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.
Equations
- One or more equations did not get rendered due to their size.