diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-26 14:46:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-13 12:20:52 +0200 |
| commit | e3550a0acc39e235e01a727267b12a7c06f23b2c (patch) | |
| tree | c26897adeffc2377e55517277d49a302eef46ea3 /tactics | |
| parent | e3a3b4bb17c40b6af2ef8501c405f0600cc6d65b (diff) | |
Uniformity of style for selecting plural or not; spacing for comma.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 2d6dffdd2..05eb0a976 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1202,7 +1202,7 @@ module Search = struct Feedback.msg_debug (pr_depth info.search_depth ++ str": no match for " ++ Printer.pr_econstr_env (Goal.env gl) s concl ++ - spc () ++ str ", " ++ int (List.length poss) ++ + str ", " ++ int (List.length poss) ++ str" possibilities"); match e with | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx |