Reverts all free variables in the goal mvarId
.
Remark: Auxiliary local declarations are cleared.
The grind
tactic also clears them, but this tactic can be used independently by users.
Reverts all free variables in the goal mvarId
.
Remark: Auxiliary local declarations are cleared.
The grind
tactic also clears them, but this tactic can be used independently by users.