def Lean.MVarId.revertAll (mvarId : MVarId) : MetaM MVarId

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.