From c8ec11ca4406f2824267e204904cb5172b2eca30 Mon Sep 17 00:00:00 2001
From: JovanGerb <56355248+JovanGerb@users.noreply.github.com>
Date: Thu, 21 Nov 2024 23:00:57 +0000
Subject: [PATCH] fix: `revert` creates natural metavariable goal (#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)
---
 src/Lean/Meta/Tactic/Revert.lean      |  1 +
 tests/lean/run/revertMetavarKind.lean | 10 ++++++++++
 2 files changed, 11 insertions(+)
 create mode 100644 tests/lean/run/revertMetavarKind.lean

diff --git a/src/Lean/Meta/Tactic/Revert.lean b/src/Lean/Meta/Tactic/Revert.lean
index 3f8f844a7bf4..79e62e61ac4e 100644
--- 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
new file mode 100644
index 000000000000..56137b95e570
--- /dev/null
+++ 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