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 /tactics/eauto.ml | |
| parent | d8e87360b6413d9eb02c2c47441c8f48b816eac3 (diff) | |
Fixing English typography for colon.
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 () |