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 /vernac/obligations.ml | |
| parent | e3a3b4bb17c40b6af2ef8501c405f0600cc6d65b (diff) | |
Uniformity of style for selecting plural or not; spacing for comma.
Diffstat (limited to 'vernac/obligations.ml')
| -rw-r--r-- | vernac/obligations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |