Nettoyage et standardisation des messages d'erreurs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9831 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 18 insertions, 5 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 8b3fb2428b..a1c011ce1b 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -101,6 +101,10 @@ let string_string_contains ~where ~what =
 
 let plural n s = if n>1 then s^"s" else s
 
+let ordinal n =
+  let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
+  string_of_int n ^ s
+
 (* string parsing *)
 
 let parse_loadpath s =
@@ -325,6 +329,12 @@ let rec list_distinct l =
     | [] -> true
   in loop l
 
+let rec list_duplicates = function
+  | [] -> []
+  | x::l ->
+      let l' = list_duplicates l in
+      if List.mem x l then list_add_set x l' else l'
+
 let rec list_filter2 f = function
   | [], [] as p -> p
   | d::dp, l::lp ->
@@ -802,9 +812,7 @@ let pr_bar () = str "|" ++ spc ()
 let pr_arg pr x = spc () ++ pr x
 let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
 
-let pr_ord n =
-  let suff = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
-  int n ++ str suff
+let nth n = str (ordinal n)
 
 let rec prlist elem l = match l with 
   | []   -> mt ()
@@ -842,6 +850,8 @@ let prvect_with_sep sep elem v =
   let n = Array.length v in
   if n = 0 then mt () else pr (n - 1)
 
+let prvect elem v = prvect_with_sep mt elem v
+
 let surround p = hov 1 (str"(" ++ p ++ str")")
 
 (*s Size of ocaml values. *)
diff --git a/lib/util.mli b/lib/util.mli
index 8a406519e8..5c59708211 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -69,6 +69,7 @@ val implode : string list -> string
 val string_index_from : string -> int -> string -> int
 val string_string_contains : where:string -> what:string -> bool
 val plural : int -> string -> string
+val ordinal : int -> string
 
 val parse_loadpath : string -> string list
 
@@ -89,6 +90,7 @@ val list_chop : int -> 'a list -> 'a list * 'a list
 val list_tabulate : (int -> 'a) -> int -> 'a list
 val list_assign : 'a list -> int -> 'a -> 'a list
 val list_distinct : 'a list -> bool
+val list_duplicates : 'a list -> 'a list
 val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
 
 (* [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
@@ -232,14 +234,15 @@ val pr_str : string -> std_ppcmds
 val pr_coma : unit -> std_ppcmds
 val pr_semicolon : unit -> std_ppcmds
 val pr_bar : unit -> std_ppcmds
-val pr_ord : int -> std_ppcmds
 val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
 val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val nth : int -> std_ppcmds
 
 val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
-val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
 val prlist_with_sep :
    (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
 val prvect_with_sep :
    (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds