fix: revert creates natural metavariable goal (leanprover#6145)

This PR fixes the `revert` tactic so that it creates a `syntheticOpaque` metavariable as the new goal, instead of a `natural` metavariable I reported it on [Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.60revert.60.20gives.20natural.20metavariable.20goal/near/483388096)
JovanGerb · Jan 21, 2025 · c8ec11c · c8ec11c
1 parent 42c8488
commit c8ec11c
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 0 deletions.
diff --git a/src/Lean/Meta/Tactic/Revert.lean b/src/Lean/Meta/Tactic/Revert.lean
@@ -43,6 +43,7 @@ def _root_.Lean.MVarId.revert (mvarId : MVarId) (fvarIds : Array FVarId) (preser
       finally
         mvarId.setKind .syntheticOpaque
     let mvar := e.getAppFn
+    mvar.mvarId!.setKind .syntheticOpaque
     mvar.mvarId!.setTag tag
     return (toRevert.map Expr.fvarId!, mvar.mvarId!)
 

diff --git a/tests/lean/run/revertMetavarKind.lean b/tests/lean/run/revertMetavarKind.lean
@@ -0,0 +1,10 @@
+import Lean.Meta
+
+open Lean Elab Tactic
+
+example (n : Nat) : n = n := by
+  revert n
+  run_tac do
+    guard (← getMainDecl).kind.isSyntheticOpaque
+  intro n
+  rfl