aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proofview.ml2
1 files changed, 1 insertions, 1 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