From 9abb749663682d4daf3e70f74d576bcd8402fafa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 21 Feb 2020 19:06:54 -0800
Subject: [PATCH] fix: preserve tag

---
 src/Init/Lean/Elab/Tactic/Generalize.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Elab/Tactic/Generalize.lean b/src/Init/Lean/Elab/Tactic/Generalize.lean
index 2e09997a9f..c40eb0ed74 100644
--- a/src/Init/Lean/Elab/Tactic/Generalize.lean
+++ b/src/Init/Lean/Elab/Tactic/Generalize.lean
@@ -21,9 +21,10 @@ private def getVarName (stx : Syntax) : Name :=
 (stx.getIdAt 4).eraseMacroScopes
 
 private def evalGeneralizeFinalize (mvarId : MVarId) (e : Expr) (target : Expr) : MetaM (List MVarId) := do
+tag         ← Meta.getMVarTag mvarId;
 eType       ← Meta.inferType e;
 u           ← Meta.getLevel eType;
-mvar' ← Meta.mkFreshExprSyntheticOpaqueMVar target;
+mvar' ← Meta.mkFreshExprSyntheticOpaqueMVar target tag;
 let rfl    := mkApp2 (Lean.mkConst `Eq.refl [u]) eType e;
 let val    := mkApp2 mvar' e rfl;
 Meta.assignExprMVar mvarId val;