From ee22e637cde3e3b3ab27e0f1c16d4eecbb2c429b Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 26 Aug 2022 17:22:40 -0400 Subject: [PATCH] fix: use withContext at ac_rfl --- src/Lean/Meta/Tactic/AC/Main.lean | 2 +- tests/lean/run/ac_rfl.lean | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean index 5c8cfc7b78..5de74ed8c9 100644 --- a/src/Lean/Meta/Tactic/AC/Main.lean +++ b/src/Lean/Meta/Tactic/AC/Main.lean @@ -171,7 +171,7 @@ where @[builtinTactic acRfl] def acRflTactic : Lean.Elab.Tactic.Tactic := fun _ => do let goal ← getMainGoal - rewriteUnnormalized goal + goal.withContext <| rewriteUnnormalized goal builtin_initialize registerTraceClass `Meta.AC diff --git a/tests/lean/run/ac_rfl.lean b/tests/lean/run/ac_rfl.lean index d7e2df4677..6e57a5e9cd 100644 --- a/tests/lean/run/ac_rfl.lean +++ b/tests/lean/run/ac_rfl.lean @@ -82,3 +82,6 @@ theorem ex₃ (n : Nat) : (fun x => n + x) = (fun x => x + n) := by -- Repro: the Prop universe doesn't work example (p q : Prop) : (p ∨ p ∨ q ∧ True) = (q ∨ p) := by ac_rfl + +-- Repro: missing withContext +example : ∀ x : Nat, x = x := by intro x; ac_rfl