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 | |
| parent | e3a3b4bb17c40b6af2ef8501c405f0600cc6d65b (diff) | |
Uniformity of style for selecting plural or not; spacing for comma.
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 |
2 files changed, 2 insertions, 2 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 diff --git a/vernac/obligations.ml b/vernac/obligations.ml index e0520216b..5233fab15 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1088,7 +1088,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit Defined cst) else ( let len = Array.length obls in - let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in + let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in progmap_add n (CEphemeron.create prg); let res = auto_solve_obligations (Some n) tactic in match res with |