From 353eb0dd2756f03dfa449b4876a7f0181fd17452 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 9 Sep 2022 15:17:50 -0700 Subject: [PATCH] fix: disable auto implicit feature when running tactics fixes #1569 --- src/Lean/Elab/SyntheticMVars.lean | 2 +- tests/lean/1569.lean | 2 ++ tests/lean/1569.lean.expected.out | 1 + 3 files changed, 4 insertions(+), 1 deletion(-) create mode 100644 tests/lean/1569.lean create mode 100644 tests/lean/1569.lean.expected.out diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index e39661db26..bbf5b8226f 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -325,7 +325,7 @@ mutual /-- Try to synthesize a term `val` using the tactic code `tacticCode`, and then assign `mvarId := val`. -/ - partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do + partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := withoutAutoBoundImplicit do /- Recall, `tacticCode` is the whole `by ...` expression. -/ let code := tacticCode[1] instantiateMVarDeclMVars mvarId diff --git a/tests/lean/1569.lean b/tests/lean/1569.lean new file mode 100644 index 0000000000..ea18364db8 --- /dev/null +++ b/tests/lean/1569.lean @@ -0,0 +1,2 @@ +def foo (x : Nat) (_ : x = 0) : Nat := x +example : foo 0 (by simp [typo]; done) = 0 := sorry diff --git a/tests/lean/1569.lean.expected.out b/tests/lean/1569.lean.expected.out new file mode 100644 index 0000000000..ce606f7a1f --- /dev/null +++ b/tests/lean/1569.lean.expected.out @@ -0,0 +1 @@ +1569.lean:2:26-2:30: error: unknown identifier 'typo'