diff options
| -rw-r--r-- | tactics/auto.ml | 8 | ||||
| -rw-r--r-- | tactics/eauto.ml | 4 |
2 files changed, 6 insertions, 6 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 diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 90f80a737..c6d244867 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -351,8 +351,8 @@ let pr_info_nop = function let pr_dbg_header = function | Off -> () - | Debug -> Feedback.msg_debug (str "(* debug eauto : *)") - | Info -> Feedback.msg_debug (str "(* info eauto : *)") + | Debug -> Feedback.msg_debug (str "(* debug eauto: *)") + | Info -> Feedback.msg_debug (str "(* info eauto: *)") let pr_info dbg s = if dbg != Info then () |