diff options
| author | Maxime Dénès | 2017-05-17 09:03:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-17 09:03:09 +0200 |
| commit | 5360ec8ff56c44e96c56965be78e6f2538963a57 (patch) | |
| tree | 82361651080323e8ab33db31890c32b93f6928ea /vernac | |
| parent | 5ea95f9cd843bec4504646851bf22bf505e56ad8 (diff) | |
| parent | 9ddfdab6a4715a08a78296bf8824d086f358bdc0 (diff) | |
Merge PR#636: Miscellaneous typos, dead code, etc.
Diffstat (limited to 'vernac')
| -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 e0520216b2..5233fab151 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 |