From e79917d9a8d6cd68fc507c49991baa78b5c86067 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Aug 2022 01:17:54 -0700 Subject: [PATCH] fix: missing `instantiateMVars` --- src/Lean/Elab/Tactic/Conv/Delta.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Tactic/Conv/Delta.lean b/src/Lean/Elab/Tactic/Conv/Delta.lean index 2761d93828..c018b33ebb 100644 --- a/src/Lean/Elab/Tactic/Conv/Delta.lean +++ b/src/Lean/Elab/Tactic/Conv/Delta.lean @@ -11,7 +11,7 @@ open Meta @[builtinTactic Lean.Parser.Tactic.Conv.delta] def evalDelta : Tactic := fun stx => withMainContext do let declName ← resolveGlobalConstNoOverload stx[1] - let lhsNew ← deltaExpand (← getLhs) (· == declName) + let lhsNew ← deltaExpand (← instantiateMVars (← getLhs)) (· == declName) changeLhs lhsNew end Lean.Elab.Tactic.Conv