From 527c3c73b48d00929e6bdfd3f4075da5209e3af3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Dec 2019 16:54:48 -0800 Subject: [PATCH] chore: improve trace message --- src/Init/Lean/Elab/Term.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index 4a6c8a5d6e..c5643ce867 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -590,7 +590,7 @@ modify $ fun s => { syntheticMVars := [], .. s }; -- 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`. remainingSyntheticMVars ← syntheticMVars.filterRevM $ fun mvarDecl => do { - trace `Elab.postpone mvarDecl.ref $ fun _ => fmt "resuming"; + trace `Elab.postpone mvarDecl.ref $ fun _ => "resuming ?" ++ mvarDecl.mvarId; succeeded ← synthesizeSyntheticMVar mvarDecl; trace `Elab.postpone mvarDecl.ref $ fun _ => if succeeded then fmt "succeeded" else fmt "not ready yet"; pure $ !succeeded