Imported Upstream version 8.3upstream/8.3

3 files changed, 20 insertions, 20 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index de70b6a6..fc793780 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: flags.ml 13358 2010-07-29 23:10:17Z herbelin $ i*)
+(*i $Id: flags.ml 13436 2010-09-19 10:18:18Z herbelin $ i*)
 
 let with_option o f x =
   let old = !o in o:=true;
@@ -114,8 +114,7 @@ let browser_cmd_fmt =
 
 let is_standard_doc_url url =
   let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in
-  let wwwprefix = "http://coq.inria.fr/" in
-  let n = String.length wwwprefix in
+  let n = String.length Coq_config.wwwcoq in
   let n' = String.length Coq_config.wwwrefman in
   url = Coq_config.localwwwrefman ||
   url = Coq_config.wwwrefman ||
diff --git a/lib/util.ml b/lib/util.ml
index 851afc60..9a8c724f 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 13357 2010-07-29 22:59:55Z herbelin $ *)
+(* $Id: util.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
 
 open Pp
 
@@ -142,7 +142,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
@@ -1290,29 +1290,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 00c73a1f..e5b5f8c6 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id: util.mli 13357 2010-07-29 22:59:55Z herbelin $ i*)
+(*i $Id: util.mli 13492 2010-10-04 21:20:01Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -330,7 +330,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