aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-14 19:59:46 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-14 20:00:47 +0200
commita40451fbd096703d9a06795c9294d11dfd7a74dd (patch)
tree6099e425b19b3f10c80798a8098703459a42e3b9
parentd8e87360b6413d9eb02c2c47441c8f48b816eac3 (diff)
Fixing English typography for colon.
-rw-r--r--tactics/auto.ml8
-rw-r--r--tactics/eauto.ml4
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 ()