From da2e5b6fdfc9ace0852d0003ace30e99de78131f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 8 Feb 2020 18:49:33 -0800
Subject: [PATCH] fix: must set mvar as natural

---
 src/Init/Lean/Meta/Tactic/Revert.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Meta/Tactic/Revert.lean b/src/Init/Lean/Meta/Tactic/Revert.lean
index a64fac75e4..be3afc76b1 100644
--- a/src/Init/Lean/Meta/Tactic/Revert.lean
+++ b/src/Init/Lean/Meta/Tactic/Revert.lean
@@ -13,7 +13,9 @@ def revert (mvarId : MVarId) (fvars : Array FVarId) : MetaM (Array FVarId × MVa
 if fvars.isEmpty then pure (fvars, mvarId)
 else withMVarContext mvarId $ do
   checkNotAssigned mvarId `revert;
-  e ← elimMVarDeps (fvars.map mkFVar) (mkMVar mvarId);
+  -- Set metavariable kind to natural to make sure `elimMVarDeps` will assign it.
+  setMVarKind mvarId MetavarKind.natural;
+  e ← finally (elimMVarDeps (fvars.map mkFVar) (mkMVar mvarId)) (setMVarKind mvarId MetavarKind.syntheticOpaque);
   pure $ e.withApp $ fun mvar args => (args.map Expr.fvarId!, mvar.mvarId!)
 
 end Meta