diff options
| author | Hugo Herbelin | 2016-10-15 00:24:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-15 00:26:55 +0200 |
| commit | ec878d596f15ad2baa10395fffd3849df5597f78 (patch) | |
| tree | a4aae5495eaa766b3f05b4c775a275c663007ade /tactics/auto.ml | |
| parent | 58d1381316560eadbe859b53780fe8da7723ad31 (diff) | |
One more little bug in the output of "debug auto".
Header was missing in last commit.
One day, it would be nice to unify the display of "debug auto" and
"debug eauto"...
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 65294dadad..985650e49d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -272,7 +272,7 @@ let tclTRY_dbg d tac = let (level, _, _) = d in let delay f = Proofview.tclUNIT () >>= fun () -> f () in let tac = match level with - | Debug | Off -> tac + | Debug | Off -> delay (fun () -> msg_debug (pr_dbg_header d); tac) | Info -> delay (fun () -> msg_debug (pr_dbg_header d); tac) >>= fun () -> msg_debug (pr_info_trace d); Proofview.tclUNIT () in let after = match level with |