diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-14 19:59:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-14 20:00:47 +0200 |
| commit | a40451fbd096703d9a06795c9294d11dfd7a74dd (patch) | |
| tree | 6099e425b19b3f10c80798a8098703459a42e3b9 | |
| parent | d8e87360b6413d9eb02c2c47441c8f48b816eac3 (diff) | |
Fixing English typography for colon.
| -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 () |