diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-13 22:38:00 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-13 22:38:00 +0000 |
| commit | 1d436a18f2f72b57ea09a6d27709a36b63be863a (patch) | |
| tree | 0082ab298988502105c7f71baa5a240051b82fdf /tactics/tactics.ml | |
| parent | 81ca535c9888bc578d8f9274568ace0d8e7b2d35 (diff) | |
Added a CString module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 39c669f42..2a8722ea9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1215,7 +1215,7 @@ let check_number_of_constructors expctdnumopt i nconstr = begin match expctdnumopt with | Some n when n <> nconstr -> error ("Not an inductive goal with "^ - string_of_int n^plural n " constructor"^".") + string_of_int n ^ String.plural n " constructor"^".") | _ -> () end; if i > nconstr then error "Not enough constructors." @@ -1283,7 +1283,7 @@ let register_subst_one f = let error_unexpected_extra_pattern loc nb pat = let s1,s2,s3 = match pat with - | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no" + | IntroIdentifier _ -> "name", (String.plural nb " introduction pattern"), "no" | _ -> "introduction pattern", "", "none" in user_err_loc (loc,"",str "Unexpected " ++ str s1 ++ str " (" ++ (if Int.equal nb 0 then (str s3 ++ str s2) else @@ -1883,7 +1883,7 @@ let expand_hyp id = tclTHEN (tclTRY (unfold_body id)) (clear [id]) let check_unused_names names = if names <> [] & Flags.is_verbose () then msg_warning - (str"Unused introduction " ++ str (plural (List.length names) "pattern") + (str"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++ str": " ++ prlist_with_sep spc pr_intro_pattern names) let rec consume_pattern avoid id isdep gl = function |