Added multiple implicit arguments rules per name.

Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]".

This should a priori be used with care (it might be a bit disturbing
seeing the same constant used with apparently incompatible signatures).

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

2 files changed, 16 insertions, 15 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 7e62f77032..fb271ea421 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -141,7 +141,7 @@ let string_string_contains ~where ~what =
   with
       Not_found -> false
 
-let plural n s = if n>1 then s^"s" else s
+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
@@ -1292,29 +1292,28 @@ let pr_vertical_list pr = function
   | [] -> str "none" ++ fnl ()
   | l -> fnl () ++ str "  " ++ hov 0 (prlist_with_sep pr_fnl pr l) ++ fnl ()
 
-let prvecti elem v =
-  let n = Array.length v in
+(* [prvecti_with_sep sep pr [|a0 ; ... ; an|]] outputs
+   [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *)
+
+let prvecti_with_sep sep elem v =
   let rec pr i =
     if i = 0 then
       elem 0 v.(0)
     else
-      let r = pr (i-1) and e = elem i v.(i) in r ++ e
+      let r = pr (i-1) and s = sep () and e = elem i v.(i) in
+      r ++ s ++ e
   in
+  let n = Array.length v in
   if n = 0 then mt () else pr (n - 1)
 
+(* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *)
+
+let prvecti elem v = prvecti_with_sep mt elem v
+
 (* [prvect_with_sep sep pr [|a ; ... ; c|]] outputs
    [pr a ++ sep() ++ ... ++ sep() ++ pr c] *)
 
-let prvect_with_sep sep elem v =
-  let rec pr n =
-    if n = 0 then
-      elem v.(0)
-    else
-      let r = pr (n-1) and s = sep() and e = elem v.(n) in
-      r ++ s ++ e
-      in
-  let n = Array.length v in
-  if n = 0 then mt () else pr (n - 1)
+let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
 
 (* [prvect pr [|a ; ... ; c|]] outputs [pr a ++ ... ++ pr c] *)
 
diff --git a/lib/util.mli b/lib/util.mli
index 83fac5fcd1..13be5521d6 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -348,7 +348,9 @@ val prlist_with_sep :
 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
+   (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvecti_with_sep :
+   (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds