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/auto.ml | |
| parent | d8e87360b6413d9eb02c2c47441c8f48b816eac3 (diff) | |
Fixing English typography for colon.
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 8 |
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 |