From 285658cead88270a5b32fd8a128eaea75ea45a14 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Oct 2020 11:52:47 -0700 Subject: [PATCH] fix: `Elab.postpone` trace message --- src/Lean/Elab/SyntheticMVars.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 40752a541d..a339a6d193 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -135,7 +135,8 @@ modify fun s => { s with syntheticMVars := [] } -- We use `filterRevM` instead of `filterM` to make sure we process the synthetic metavariables using the order they were created. -- It would not be incorrect to use `filterM`. let remainingSyntheticMVars ← syntheticMVars.filterRevM fun mvarDecl => do - trace[Elab.postpone]! "resuming ?{mvarDecl.mvarId}" + -- We use `traceM` because we want to make sure the metavar local context is used to trace the message + traceM `Elab.postpone (withMVarContext mvarDecl.mvarId do addMessageContext msg!"resuming {mkMVar mvarDecl.mvarId}") let succeeded ← synthesizeSyntheticMVar mvarDecl postponeOnError runTactics trace[Elab.postpone]! if succeeded then fmt "succeeded" else fmt "not ready yet" pure !succeeded