fix bug in lsimp

lecopivo · Nov 29, 2024 · 13f33cd · 13f33cd
1 parent 1d70152
commit 13f33cd
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/SciLean/Tactic/LSimp/Main.lean b/SciLean/Tactic/LSimp/Main.lean
@@ -642,7 +642,11 @@ partial def processCongrHypothesis (h : Expr) : LSimpM Bool := do
       return r.proof?.isSome || (xs.size > 0 && lhs != r.expr)
 
 /-- Try to rewrite `e` children using the given congruence theorem -/
-partial def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : LSimpM (Option Result) := withNewMCtxDepth do
+partial def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : LSimpM (Option Result) :=
+  -- Looks like that `withNewMCtxDepth` does not work well with `MetaLCtxM` so we need to
+  -- add `withoutModifyingLCtx`
+  withoutModifyingLCtx (fun r? => r?.mapM (Result.bindVars ·)) do
+  withNewMCtxDepth do
   trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
   let thm ← mkConstWithFreshMVarLevels c.theoremName
   let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm)