aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
authorHugo Herbelin2014-11-02 11:51:20 +0100
committerHugo Herbelin2014-11-02 19:58:03 +0100
commiteb863af14628cd13ceb455c406937c717c8d3ee5 (patch)
tree5a2e225ac8647190d79dca03ed86b67fb406cda6 /tactics
parent81848583bdbc21564e4b2c8d308dd0b6add0bf38 (diff)
Plural and singular forms in error messages.
Diffstat (limited to 'tactics')
-rw-r--r--tactics/tacticals.ml4
1 files changed, 2 insertions, 2 deletions
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