aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r--tactics/auto.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6d1a1ae28..a6dc64b4e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -269,10 +269,10 @@ let pr_info_nop = function
let pr_dbg_header = function
| (Off,_,_) -> mt ()
- | (Debug,0,_) -> str "(* debug trivial : *)"
- | (Debug,_,_) -> str "(* debug auto : *)"
- | (Info,0,_) -> str "(* info trivial : *)"
- | (Info,_,_) -> str "(* info auto : *)"
+ | (Debug,0,_) -> str "(* debug trivial: *)"
+ | (Debug,_,_) -> str "(* debug auto: *)"
+ | (Info,0,_) -> str "(* info trivial: *)"
+ | (Info,_,_) -> str "(* info auto: *)"
let tclTRY_dbg d tac =
let (level, _, _) = d in