fix

leanprover-community · May 8, 2024 · 1a26cb8 · 1a26cb8
1 parent fdc5e45
commit 1a26cb8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Qq/Match.lean b/Qq/Match.lean
@@ -172,7 +172,7 @@ def elabPat (pat : Term) (lctx : LocalContext) (localInsts : LocalInstances) (ty
           let (pat, patVars) ← getPatVars pat #[]
           let pat ← Lean.Elab.Term.elabTerm pat ty
           let pat ← ensureHasType ty pat
-          synthesizeSyntheticMVars false
+          synthesizeSyntheticMVars (postpone := .no)
           let pat ← instantiateMVars pat
 
           let mctx ← getMCtx