diff options
| author | ppedrot | 2012-11-13 22:38:00 +0000 |
|---|---|---|
| committer | ppedrot | 2012-11-13 22:38:00 +0000 |
| commit | 1d436a18f2f72b57ea09a6d27709a36b63be863a (patch) | |
| tree | 0082ab298988502105c7f71baa5a240051b82fdf /printing | |
| 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 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | printing/prettyp.ml | 10 |
2 files changed, 6 insertions, 6 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 721d9b6c8a..41882acb4b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -734,7 +734,7 @@ let rec pr_vernac = function | VernacDeclareInstances (glob, ids) -> hov 1 (pr_non_locality (not glob) ++ - str"Existing" ++ spc () ++ str(plural (List.length ids) "Instance") ++ + str"Existing" ++ spc () ++ str(String.plural (List.length ids) "Instance") ++ spc () ++ prlist_with_sep spc pr_reference ids) | VernacDeclareClass id -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 7fbbc0a2ec..3136847b03 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -85,7 +85,7 @@ let pr_impl_name imp = pr_id (name_of_implicit imp) let print_impargs_by_name max = function | [] -> [] | impls -> - [hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++ + [hov 0 (str (String.plural (List.length impls) "Argument") ++ spc() ++ prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++ str (conjugate_verb_to_be impls) ++ str" implicit" ++ (if max then strbrk " and maximally inserted" else mt()))] @@ -111,7 +111,7 @@ let print_impargs_list prefix l = (if n1 = n2 then int_or_no n2 else if n1 = 0 then str "less than " ++ int n2 else int n1 ++ str " to " ++ int_or_no n2) ++ - str (plural n2 " argument") ++ str ":"; + str (String.plural n2 " argument") ++ str ":"; v 0 (prlist_with_sep cut (fun x -> x) (if List.exists is_status_implicit imps then print_one_impargs_list imps @@ -166,12 +166,12 @@ let print_simpl_behaviour ref = let pp_nomatch = spc() ++ if nomatch then str "avoiding to expose match constructs" else str"" in let pp_recargs = spc() ++ str "when the " ++ - pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (plural (List.length recargs) " argument") ++ - str (plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++ + pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (String.plural (List.length recargs) " argument") ++ + str (String.plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++ str " to a constructor" in let pp_nargs = spc() ++ str "when applied to " ++ int nargs ++ - str (plural nargs " argument") in + str (String.plural nargs " argument") in [hov 2 (str "The simpl tactic " ++ match recargs, nargs, never with | _,_, true -> str "never unfolds " ++ pr_global ref |