From 1a26cb8b722c1d7965fc24e348c91c1e0e58685f Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 9 May 2024 09:36:59 +1000
Subject: [PATCH] fix

---
 Qq/Match.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Qq/Match.lean b/Qq/Match.lean
index abe4cfc..442faf9 100644
--- 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