aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2014-11-02 11:51:20 +0100
committerHugo Herbelin2014-11-02 19:58:03 +0100
commiteb863af14628cd13ceb455c406937c717c8d3ee5 (patch)
tree5a2e225ac8647190d79dca03ed86b67fb406cda6
parent81848583bdbc21564e4b2c8d308dd0b6add0bf38 (diff)
Plural and singular forms in error messages.
-rw-r--r--proofs/proofview.ml2
-rw-r--r--tactics/tacticals.ml4
2 files changed, 3 insertions, 3 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 0a03965f1d..7ab7e882ce 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -368,7 +368,7 @@ let _ = Errors.register_handler begin function
let open Pp in
let errmsg =
str"Incorrect number of goals" ++ spc() ++
- str"(expected "++int i++str" tactics)."
+ str"(expected "++int i++str(String.plural i " tactic") ++ str")."
in
Errors.errorlabstrm "" errmsg
| _ -> raise Errors.Unhandled
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 2a21c53ab6..bc7e5f7cda 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -345,7 +345,7 @@ module New = struct
| SizeMismatch (i,_)->
let errmsg =
str"Incorrect number of goals" ++ spc() ++
- str"(expected "++int i++str" tactics)"
+ str"(expected "++int i++str(String.plural i " tactic") ++ str")"
in
tclFAIL 0 errmsg
| reraise -> tclZERO reraise
@@ -368,7 +368,7 @@ module New = struct
| SizeMismatch (i,_)->
let errmsg =
str"Incorrect number of goals" ++ spc() ++
- str"(expected "++int i++str" tactics)"
+ str"(expected "++int i++str(String.plural i " tactic") ++ str")"
in
tclFAIL 0 errmsg
| reraise -> tclZERO reraise