Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

42 files changed, 715 insertions, 307 deletions

diff --git a/lib/bigint.ml b/lib/bigint.ml
new file mode 100644
index 00000000..5bcceb5c
--- /dev/null
+++ b/lib/bigint.ml
@@ -0,0 +1,392 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: bigint.ml 7305 2005-08-19 19:51:02Z letouzey $ *)
+
+(*i*)
+open Pp
+(*i*)
+
+(***************************************************)
+(* Basic operations on (unbounded) integer numbers *)
+(***************************************************)
+
+(* An integer is canonically represented as an array of k-digits blocs.
+
+   0 is represented by the empty array and -1 by the singleton [|-1|].
+   The first bloc is in the range ]0;10^k[ for positive numbers. 
+   The first bloc is in the range ]-10^k;-1[ for negative ones. 
+   All other blocs are numbers in the range [0;10^k[.
+
+   Negative numbers are represented using 2's complementation. For instance,
+   with 4-digits blocs, [-9655;6789] denotes -96543211
+*)
+
+(* The base is a power of 10 in order to facilitate the parsing and printing
+   of numbers in digital notation.
+
+   All functions, to the exception of to_string and of_string should work
+   with an arbitrary base, even if not a power of 10.
+
+   In practice, we set k=4 so that no overflow in ocaml machine words
+   (i.e. the interval [-2^30;2^30-1]) occur when multiplying two
+   numbers less than (10^k)
+*)
+
+(* The main parameters *)
+
+let size =
+  let rec log10 n = if n < 10 then 0 else 1 + log10 (n / 10) in
+  (log10 max_int) / 2
+
+let format_size =
+  (* How to parametrize a printf format *)
+  if size = 4 then Printf.sprintf "%04d"
+  else fun n ->
+    let rec aux j l n =
+      if j=size then l else aux (j+1) (string_of_int (n mod 10) :: l) (n/10)
+    in String.concat "" (aux 0 [] n)
+
+(* The base is 10^size *)
+let base =
+  let rec exp10 = function 0 -> 1 | n -> 10 * exp10 (n-1) in exp10 size
+
+(* Basic numbers *)
+let zero = [||]
+let neg_one = [|-1|]
+
+(* Sign of an integer *)
+let is_strictly_neg n = n<>[||] && n.(0) < 0
+let is_strictly_pos n = n<>[||] && n.(0) > 0
+let is_neg_or_zero n = n=[||] or n.(0) < 0
+let is_pos_or_zero n = n=[||] or n.(0) > 0
+
+let normalize_pos n =
+  let k = ref 0 in
+  while !k < Array.length n & n.(!k) = 0 do incr k done;
+  Array.sub n !k (Array.length n - !k)
+
+let normalize_neg n =
+  let k = ref 1 in
+  while !k < Array.length n & n.(!k) = base - 1 do incr k done;
+  let n' = Array.sub n !k (Array.length n - !k) in
+  if Array.length n' = 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n')
+
+let rec normalize n =
+  if Array.length n = 0 then n else 
+    if n.(0) = -1 then normalize_neg n else normalize_pos n
+
+let neg m =
+  if m = zero then zero else
+  let n = Array.copy m in
+  let i = ref (Array.length m - 1) in
+  while !i > 0 & n.(!i) = 0 do decr i done;
+  if !i > 0 then begin
+    n.(!i) <- base - n.(!i); decr i;
+    while !i > 0 do n.(!i) <- base - 1 - n.(!i); decr i done;
+    n.(0) <- - n.(0) - 1;
+    if n.(0) < -1 then (n.(0) <- n.(0) + base; Array.append [| -1 |] n) else
+    if n.(0) = - base then (n.(0) <- 0; Array.append [| -1 |] n)
+    else normalize n
+  end else (n.(0) <- - n.(0); n)
+
+let push_carry r j =
+  let j = ref j in
+  while !j > 0 & r.(!j) < 0 do
+    r.(!j) <- r.(!j) + base; decr j; r.(!j) <- r.(!j) - 1
+  done;
+  while !j > 0 & r.(!j) >= base do
+    r.(!j) <- r.(!j) - base; decr j; r.(!j) <- r.(!j) + 1
+  done;
+  if r.(0) >= base then (r.(0) <- r.(0) - base; Array.append [| 1 |] r)
+  else if r.(0) < -base then (r.(0) <- r.(0) + 2*base; Array.append [| -2 |] r)
+  else if r.(0) = -base then (r.(0) <- 0; Array.append [| -1 |] r)
+  else normalize r
+
+let add_to r a j =
+  if a = zero then r else begin
+  for i = Array.length r - 1 downto j+1 do
+    r.(i) <- r.(i) + a.(i-j);
+    if r.(i) >= base then (r.(i) <- r.(i) - base; r.(i-1) <- r.(i-1) + 1)
+  done;
+  r.(j) <- r.(j) + a.(0);
+  push_carry r j
+  end
+
+let add n m =
+  let d = Array.length n - Array.length m in
+  if d > 0 then add_to (Array.copy n) m d else add_to (Array.copy m) n (-d)
+
+let sub_to r a j =
+  if a = zero then r else begin
+  for i = Array.length r - 1 downto j+1 do
+    r.(i) <- r.(i) - a.(i-j);
+    if r.(i) < 0 then (r.(i) <- r.(i) + base; r.(i-1) <- r.(i-1) - 1)
+  done;
+  r.(j) <- r.(j) - a.(0);
+  push_carry r j
+  end
+
+let sub n m =
+  let d = Array.length n - Array.length m in
+  if d >= 0 then sub_to (Array.copy n) m d
+  else let r = neg m in add_to r n (Array.length r - Array.length n)
+
+let rec mult m n =
+  if m = zero or n = zero then zero else
+  let l = Array.length m + Array.length n in
+  let r = Array.create l 0 in
+  for i = Array.length m - 1 downto 0 do
+    for j = Array.length n - 1 downto 0 do
+      let p = m.(i) * n.(j) + r.(i+j+1) in
+      let (q,s) =
+        if p < 0
+        then (p + 1) / base - 1, (p + 1) mod base + base - 1
+        else p / base, p mod base in
+      r.(i+j+1) <- s;
+      if q <> 0 then r.(i+j) <- r.(i+j) + q;
+    done
+  done;
+  normalize r
+
+let rec less_than_same_size m n i j =
+  i < Array.length m &&
+  (m.(i) < n.(j) or (m.(i) = n.(j) && less_than_same_size m n (i+1) (j+1)))
+
+let less_than m n =
+  if is_strictly_neg m then
+    is_pos_or_zero n or Array.length m > Array.length n
+      or (Array.length m = Array.length n && less_than_same_size m n 0 0)
+  else
+    is_strictly_pos n && (Array.length m < Array.length n or
+    (Array.length m = Array.length n && less_than_same_size m n 0 0))
+
+let equal m n = (m = n)
+  
+let less_or_equal_than m n = equal m n or less_than m n
+
+let less_than_shift_pos k m n =
+  (Array.length m - k < Array.length n)
+  or (Array.length m - k = Array.length n && less_than_same_size m n k 0)
+
+let rec can_divide k m d i =
+  (i = Array.length d) or
+  (m.(k+i) > d.(i)) or
+  (m.(k+i) = d.(i) && can_divide k m d (i+1))
+
+(* computes m - d * q * base^(|m|-k) in-place on positive numbers *)
+let sub_mult m d q k =
+  if q <> 0 then
+  for i = Array.length d - 1 downto 0 do
+    let v = d.(i) * q in
+    m.(k+i) <- m.(k+i) - v mod base;
+    if m.(k+i) < 0 then (m.(k+i) <- m.(k+i) + base; m.(k+i-1) <- m.(k+i-1) -1);
+    if v >= base then m.(k+i-1) <- m.(k+i-1) - v / base;
+  done
+
+let euclid m d =
+  let isnegm, m =
+    if is_strictly_neg m then (-1),neg m else 1,Array.copy m in
+  let isnegd, d = if is_strictly_neg d then (-1),neg d else 1,d in
+  if d = zero then raise Division_by_zero;
+  let q,r = 
+    if less_than m d then (zero,m) else
+    let ql = Array.length m - Array.length d in
+    let q = Array.create (ql+1) 0 in
+    let i = ref 0 in
+    while not (less_than_shift_pos !i m d) do
+      if m.(!i)=0 then incr i else
+      if can_divide !i m d 0 then begin
+        let v = 
+          if Array.length d > 1 && d.(0) <> m.(!i) then
+            (m.(!i) * base + m.(!i+1)) / (d.(0) * base + d.(1) + 1)
+          else
+            m.(!i) / d.(0) in
+        q.(!i) <- q.(!i) + v;
+	sub_mult m d v !i
+      end else begin
+        let v = (m.(!i) * base + m.(!i+1)) / (d.(0) + 1) in
+        q.(!i) <- q.(!i) + v / base;
+	sub_mult m d (v / base) !i;
+        q.(!i+1) <- q.(!i+1) + v mod base;
+	if q.(!i+1) >= base then
+	  (q.(!i+1) <- q.(!i+1)-base; q.(!i) <- q.(!i)+1);
+	sub_mult m d (v mod base) (!i+1)
+      end
+    done;
+    (normalize q, normalize m) in
+  (if isnegd * isnegm = -1 then neg q else q),
+  (if isnegm = -1 then neg r else r)
+
+(* Parsing/printing ordinary 10-based numbers *)
+
+let of_string s =
+  let isneg = String.length s > 1 & s.[0] = '-' in
+  let n = if isneg then 1 else 0 in
+  let d = ref n in
+  while !d < String.length s && s.[!d] = '0' do incr d done;
+  if !d = String.length s then zero else
+  let r = (String.length s - !d) mod size in
+  let h = String.sub s (!d) r in
+  if !d = String.length s - 1 && isneg && h="1" then neg_one else
+  let e = if h<>"" then 1 else 0 in 
+  let l = (String.length s - !d) / size in
+  let a = Array.create (l + e + n) 0 in
+  if isneg then begin
+    a.(0) <- (-1); 
+    let carry = ref 0 in
+    for i=l downto 1 do
+      let v = int_of_string (String.sub s ((i-1)*size + !d +r) size)+ !carry in
+      if v <> 0 then (a.(i+e)<- base - v; carry := 1) else carry := 0
+    done;
+    if e=1 then a.(1) <- base - !carry - int_of_string h;
+  end
+  else begin
+    if e=1 then a.(0) <- int_of_string h;
+    for i=1 to l do
+      a.(i+e-1) <- int_of_string (String.sub s ((i-1)*size + !d + r) size)
+    done
+  end;
+  a
+
+let to_string_pos sgn n =
+   if Array.length n = 0 then "0" else
+     sgn ^
+     String.concat ""
+      (string_of_int n.(0) :: List.map format_size (List.tl (Array.to_list n)))
+
+let to_string n =
+  if is_strictly_neg n then to_string_pos "-" (neg n)
+  else to_string_pos "" n
+
+(******************************************************************)
+(* Optimized operations on (unbounded) integer numbers            *)
+(* integers smaller than base are represented as machine integers *)
+(******************************************************************)
+
+type bigint = Obj.t
+
+let ints_of_int n =
+  if n >= base then [| n / base; n mod base |]
+  else if n <= - base then [| n / base - 1; n mod base + base |]
+  else if n = 0 then [| |] else [| n |]
+
+let big_of_int n =
+  if n >= base then Obj.repr [| n / base; n mod base |]
+  else if n <= - base then Obj.repr [| n / base - 1; n mod base + base |]
+  else Obj.repr n
+
+let big_of_ints n =
+  let n = normalize n in
+  if n = zero then Obj.repr 0 else
+  if Array.length n = 1 then Obj.repr n.(0) else
+  Obj.repr n
+
+let coerce_to_int = (Obj.magic : Obj.t -> int)
+let coerce_to_ints = (Obj.magic : Obj.t -> int array)
+
+let ints_of_z n =
+  if Obj.is_int n then ints_of_int (coerce_to_int n)
+  else coerce_to_ints n
+
+let app_pair f (m, n) =
+  (f m, f n)
+
+let add m n =
+  if Obj.is_int m & Obj.is_int n 
+  then big_of_int (coerce_to_int m + coerce_to_int n)
+  else big_of_ints (add (ints_of_z m) (ints_of_z n))
+
+let sub m n =
+  if Obj.is_int m & Obj.is_int n
+  then big_of_int (coerce_to_int m - coerce_to_int n)
+  else big_of_ints (sub (ints_of_z m) (ints_of_z n))
+
+let mult m n =
+  if Obj.is_int m & Obj.is_int n
+  then big_of_int (coerce_to_int m * coerce_to_int n)
+  else big_of_ints (mult (ints_of_z m) (ints_of_z n))
+
+let euclid m n =
+  if Obj.is_int m & Obj.is_int n 
+  then app_pair big_of_int 
+    (coerce_to_int m / coerce_to_int n, coerce_to_int m mod coerce_to_int n)
+  else app_pair big_of_ints (euclid (ints_of_z m) (ints_of_z n))
+
+let less_than m n =
+  if Obj.is_int m & Obj.is_int n
+  then coerce_to_int m < coerce_to_int n
+  else less_than (ints_of_z m) (ints_of_z n)
+
+let neg n =
+  if Obj.is_int n then big_of_int (- (coerce_to_int n))
+  else big_of_ints (neg (ints_of_z n))
+
+let of_string m = big_of_ints (of_string m)
+let to_string m = to_string (ints_of_z m)
+
+let zero = big_of_int 0
+let one = big_of_int 1
+let sub_1 n = sub n one
+let add_1 n = add n one
+let two = big_of_int 2
+let neg_two = big_of_int (-2)
+let mult_2 n = add n n
+let is_zero n = n=zero
+
+let div2_with_rest n =
+  let (q,b) = euclid n two in
+  (q, b = one)
+
+let is_strictly_neg n = is_strictly_neg (ints_of_z n)
+let is_strictly_pos n = is_strictly_pos (ints_of_z n)
+let is_neg_or_zero n = is_neg_or_zero (ints_of_z n)
+let is_pos_or_zero n = is_pos_or_zero (ints_of_z n)
+
+let pr_bigint n = str (to_string n)
+
+(* Testing suite *)
+
+let check () =
+  let numbers = [
+  "1";"2";"99";"100";"101";"9999";"10000";"10001";
+  "999999";"1000000";"1000001";"99999999";"100000000";"100000001";
+  "1234";"5678";"12345678";"987654321";
+  "-1";"-2";"-99";"-100";"-101";"-9999";"-10000";"-10001";
+  "-999999";"-1000000";"-1000001";"-99999999";"-100000000";"-100000001";
+  "-1234";"-5678";"-12345678";"-987654321";"0"
+  ]
+  in
+  let eucl n m =
+    let n' = abs_float n and m' = abs_float m in
+    let q' = floor (n' /. m') in let r' = n' -. m' *. q' in
+    (if n *. m < 0. & q' <> 0. then -. q' else q'),
+    (if n < 0. then -. r' else r') in
+  let round f = floor (abs_float f +. 0.5) *. (if f < 0. then -1. else 1.) in
+  let i = ref 0 in
+  let compare op n n' =
+    incr i;
+    let s = Printf.sprintf "%30s" (to_string n) in
+    let s' = Printf.sprintf "% 30.0f" (round n') in
+    if s <> s' then Printf.printf "%s: %s <> %s\n" op s s' in
+List.iter (fun a -> List.iter (fun b ->  
+  let n = of_string a and m = of_string b in
+  let n' = float_of_string a and m' = float_of_string b in
+  let a = add n m and a' = n' +. m' in
+  let s = sub n m and s' = n' -. m' in
+  let p = mult n m and p' = n' *. m' in
+  let q,r = try euclid n m with Division_by_zero -> zero,zero
+  and q',r' = eucl n' m' in
+  compare "+" a a';
+  compare "-" s s';
+  compare "*" p p';
+  compare "/" q q';
+  compare "%" r r') numbers) numbers;
+  Printf.printf "%i tests done\n" !i
+
+
diff --git a/lib/bigint.mli b/lib/bigint.mli
new file mode 100644
index 00000000..7a835a49
--- /dev/null
+++ b/lib/bigint.mli
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: bigint.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
+
+(*i*)
+open Pp
+(*i*)
+
+(* Arbitrary large integer numbers *)
+
+type bigint
+
+val of_string : string -> bigint
+val to_string : bigint -> string
+
+val zero : bigint
+val one : bigint
+val two : bigint
+
+val div2_with_rest : bigint -> bigint * bool (* true=odd; false=even *)
+val add_1 : bigint -> bigint
+val sub_1 : bigint -> bigint
+val mult_2 : bigint -> bigint
+
+val add : bigint -> bigint -> bigint
+val sub : bigint -> bigint -> bigint
+val mult : bigint -> bigint -> bigint
+val euclid : bigint -> bigint -> bigint * bigint
+
+val less_than : bigint -> bigint -> bool
+val equal : bigint -> bigint -> bool
+
+val is_strictly_pos : bigint -> bool
+val is_strictly_neg : bigint -> bool
+val is_pos_or_zero : bigint -> bool
+val is_neg_or_zero : bigint -> bool
+val neg : bigint -> bigint
+
+val pr_bigint : bigint -> std_ppcmds
diff --git a/lib/bignat.ml b/lib/bignat.ml
deleted file mode 100644
index 583a027f..00000000
--- a/lib/bignat.ml
+++ /dev/null
@@ -1,116 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: bignat.ml,v 1.5.6.1 2004/07/16 19:30:29 herbelin Exp $ *)
-
-(*i*)
-open Pp
-(*i*)
-
-(* Arbitrary big natural numbers *)
-
-type bignat = int array
-
-let digits =            8
-let base =      100000000 (* let enough room for multiplication by 2 *)
-let base_div_2 = 50000000
-let base_to_string x = Printf.sprintf "%08d" x
-
-let of_string s =
-  let a = Array.create (String.length s / digits + 1) 0 in
-  let r = String.length s mod digits in
-  if r<>0 then a.(0) <- int_of_string (String.sub s 0 r);
-  for i = 1 to String.length s / digits do
-    a.(i) <- int_of_string (String.sub s ((i-1)*digits+r) digits)
-  done;
-  a
-
-let rec to_string s =
-  if s = [||] then "0" else
-    if s.(0) = 0 then to_string (Array.sub s 1 (Array.length s - 1))
-    else 
-      String.concat ""
-        ((string_of_int (s.(0)))
-        ::(List.tl (Array.to_list (Array.map base_to_string s))))
-  
-let is_nonzero a =
-  let b = ref false in Array.iter (fun x -> b := x <> 0 || !b) a; !b
-
-let zero = [|0|]
-let one = [|1|]
-
-let is_one a =
-  let rec leading_zero i = i<0 || (a.(i) = 0 && leading_zero (i-1)) in
-  (a.(Array.length a - 1) = 1) && leading_zero (Array.length a - 2)
-      
-let div2_with_rest n =
-  let len = Array.length n in
-  let q = Array.create len 0 in
-  for i = 0 to len - 2 do
-    q.(i) <- q.(i) + n.(i) / 2; q.(i + 1) <- base_div_2 * (n.(i) mod 2)
-  done;
-  q.(len - 1) <- q.(len - 1) + n.(len - 1) / 2;
-  q, (n.(len - 1) mod 2) = 1
-
-let add_1 n =
-  let m = Array.copy n
-  and i = ref (Array.length n - 1) in
-  while !i >= 0 && m.(!i) = base-1 do
-    m.(!i) <- 0; decr i; 
-  done;
-  if !i < 0 then begin
-    m.(0) <- 0; Array.concat [[| 1 |]; m] 
-  end else begin
-    m.(!i) <- m.(!i) + 1; m
-  end
-
-let sub_1 n =
-  if is_nonzero n then
-    let m = Array.copy n
-    and i = ref (Array.length n - 1) in
-    while m.(!i) = 0 && !i > 0 do
-      m.(!i) <- base-1; decr i;
-    done;
-    m.(!i) <- m.(!i) - 1;
-    m
-  else n
-
-let rec mult_2 n =
-  let m = Array.copy n in
-  m.(Array.length n - 1) <- 2 * m.(Array.length n - 1);
-  for i = Array.length n - 2 downto 0 do
-    m.(i) <- 2 * m.(i);
-    if m.(i + 1) >= base then begin
-      m.(i + 1) <- m.(i + 1) - base; m.(i) <- m.(i) + 1 
-    end
-  done;
-  if m.(0) >= base then begin
-    m.(0) <- m.(0) - base; Array.concat [[| 1 |]; m] 
-  end else 
-    m
-
-let less_than m n =
-  let lm = ref 0 in
-  while !lm < Array.length m && m.(!lm) = 0 do incr lm done;
-  let ln = ref 0 in
-  while !ln < Array.length n && n.(!ln) = 0 do incr ln done;
-  let um = Array.length m - !lm and un = Array.length n - !ln in
-  let rec lt d =
-    d < um && (m.(!lm+d) < n.(!ln+d) || (m.(!lm+d) = n.(!ln+d) && lt (d+1)))
-  in
-  (um < un) || (um = un && lt 0)
-
-type bigint = POS of bignat | NEG of bignat
-
-let pr_bigint = function
-  | POS n -> str (to_string n)
-  | NEG n -> str "-" ++ str (to_string n)
-
-let bigint_to_string = function
-  | POS n -> to_string n
-  | NEG n -> "-" ^ (to_string n);;
diff --git a/lib/bignat.mli b/lib/bignat.mli
deleted file mode 100644
index 860bcf29..00000000
--- a/lib/bignat.mli
+++ /dev/null
@@ -1,37 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: bignat.mli,v 1.4.6.3 2005/01/21 17:14:11 herbelin Exp $ i*)
-
-(*i*)
-open Pp
-(*i*)
-
-(* Arbitrary big natural numbers *)
-
-type bignat
-
-val of_string : string -> bignat
-val to_string : bignat -> string
-
-val is_nonzero : bignat -> bool
-val zero : bignat
-val one : bignat
-val is_one : bignat -> bool
-val div2_with_rest : bignat -> bignat * bool (* true=odd; false=even *)
-
-val add_1 : bignat -> bignat
-val sub_1 : bignat -> bignat (* Remark: [sub_1 0]=0 *)
-val mult_2 : bignat -> bignat
-
-val less_than : bignat -> bignat -> bool
-
-type bigint = POS of bignat | NEG of bignat
-
-val bigint_to_string : bigint -> string
-val pr_bigint : bigint -> std_ppcmds
diff --git a/lib/bstack.ml b/lib/bstack.ml
index d4b995fb..b86dccf9 100644
--- a/lib/bstack.ml
+++ b/lib/bstack.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: bstack.ml,v 1.3.2.1 2004/07/16 19:30:29 herbelin Exp $ *)
+(* $Id: bstack.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (* Queues of a given length *)
 
diff --git a/lib/bstack.mli b/lib/bstack.mli
index 617f7df1..f018d155 100644
--- a/lib/bstack.mli
+++ b/lib/bstack.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: bstack.mli,v 1.4.2.1 2004/07/16 19:30:29 herbelin Exp $ i*)
+(*i $Id: bstack.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* Bounded stacks. If the depth is [None], then there is no depth limit. *)
 
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 63f00365..94979835 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dyn.ml,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ *)
+(* $Id: dyn.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Util
 
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 7f46c7e6..86a1560a 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: dyn.mli,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ i*)
+(*i $Id: dyn.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* Dynamics. Use with extreme care. Not for kids. *)
 
diff --git a/lib/edit.ml b/lib/edit.ml
index 5020ef5c..03420992 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: edit.ml,v 1.8.2.1 2004/07/16 19:30:29 herbelin Exp $ *)
+(* $Id: edit.ml 6947 2005-04-20 16:18:41Z coq $ *)
 
 open Pp
 open Util
@@ -84,6 +84,28 @@ let undo e n =
 	  errorlabstrm "Edit.undo" (str"Undo stack exhausted");
         repeat n Bstack.pop bs
 
+(* Return the depth of the focused proof of [e] stack, this is used to
+   put informations in coq prompt (in emacs mode). *)
+let depth e =
+  match e.focus with
+    | None -> invalid_arg "Edit.depth"
+    | Some d ->
+	let (bs,_) = Hashtbl.find e.buf d in
+	Bstack.depth bs
+
+(* Undo focused proof of [e] to reach depth [n] *)
+let undo_todepth e n =
+  match e.focus with
+    | None -> 
+	if n <> 0 
+	then errorlabstrm "Edit.undo_todepth" (str"No proof in progress")
+	else () (* if there is no proof in progress, then n must be zero *)
+    | Some d ->
+	let (bs,_) = Hashtbl.find e.buf d in
+	if Bstack.depth bs < n then
+	  errorlabstrm "Edit.undo_todepth" (str"Undo stack would be exhausted");
+        repeat (Bstack.depth bs - n) Bstack.pop bs
+
 let create e (d,b,c,udepth) =
   if Hashtbl.mem e.buf d then
     errorlabstrm "Edit.create" 
diff --git a/lib/edit.mli b/lib/edit.mli
index edf0f67b..ab82c1f9 100644
--- a/lib/edit.mli
+++ b/lib/edit.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: edit.mli,v 1.5.2.1 2004/07/16 19:30:29 herbelin Exp $ i*)
+(*i $Id: edit.mli 6947 2005-04-20 16:18:41Z coq $ i*)
 
 (* The type of editors.
  * An editor is a finite map, ['a -> 'b], which knows how to apply
@@ -54,3 +54,10 @@ val delete : ('a,'b,'c) t -> 'a -> unit
 val dom : ('a,'b,'c) t -> 'a list
 
 val clear : ('a,'b,'c) t -> unit
+
+(* [depth e] Returns the depth of the focused proof stack of [e], this
+   is used to put informations in coq prompt (in emacs mode). *)
+val depth : ('a,'b,'c) t -> int
+
+(* [undo_todepth e n] Undoes focused proof of [e] to reach depth [n] *)
+val undo_todepth : ('a,'b,'c) t -> int -> unit
diff --git a/lib/explore.ml b/lib/explore.ml
index 2eaabef8..7e6de0c4 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: explore.ml,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ i*)
+(*i $Id: explore.ml 6066 2004-09-06 22:54:50Z barras $ i*)
 
 open Format
 
@@ -37,6 +37,7 @@ module Make = functor(S : SearchProblem) -> struct
     if S.success s then s else depth_first_many (S.branching s)
   and depth_first_many = function
     | [] -> raise Not_found
+    | [s] -> depth_first s
     | s :: l -> try depth_first s with Not_found -> depth_first_many l
 
   let debug_depth_first s = 
@@ -44,8 +45,8 @@ module Make = functor(S : SearchProblem) -> struct
       pp_position p; S.pp s;
       if S.success s then s else explore_many 1 p (S.branching s)
     and explore_many i p = function
-      | [] -> 
-	  raise Not_found
+      | [] -> raise Not_found
+      | [s] -> explore (i::p) s
       | s :: l -> 
 	  try explore (i::p) s with Not_found -> explore_many (succ i) p l
     in
@@ -67,10 +68,8 @@ module Make = functor(S : SearchProblem) -> struct
 
   let breadth_first s = 
     let rec explore q =
-      try 
-	let (s, q') = pop q in enqueue q' (S.branching s)
-      with Empty ->
-	raise Not_found
+      let (s, q') = try pop q with Empty -> raise Not_found in
+      enqueue q' (S.branching s)
     and enqueue q = function
       | [] -> explore q
       | s :: l -> if S.success s then s else enqueue (push s q) l
@@ -79,11 +78,8 @@ module Make = functor(S : SearchProblem) -> struct
 
   let debug_breadth_first s = 
     let rec explore q =
-      try 
-	let ((p,s), q') = pop q in 
-	enqueue 1 p q' (S.branching s)
-      with Empty ->
-	raise Not_found
+      let ((p,s), q') = try pop q with Empty -> raise Not_found in 
+      enqueue 1 p q' (S.branching s)
     and enqueue i p q = function
       | [] -> 
 	  explore q
diff --git a/lib/explore.mli b/lib/explore.mli
index 1236f06b..07f95e8a 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: explore.mli,v 1.2.16.1 2004/07/16 19:30:29 herbelin Exp $ i*)
+(*i $Id: explore.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (*s Search strategies. *)
 
diff --git a/lib/gmap.ml b/lib/gmap.ml
index e5d41034..884305d9 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.ml
@@ -5,10 +5,10 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: gmap.ml,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ *)
+(* $Id: gmap.ml 7925 2006-01-24 23:20:39Z herbelin $ *)
 
 (* Maps using the generic comparison function of ocaml. Code borrowed from
-   the ocaml standard library. *)
+   the ocaml standard library (Copyright 1996, INRIA). *)
 
     type ('a,'b) t =
         Empty
@@ -57,7 +57,7 @@
     let rec add x data = function
         Empty ->
           Node(Empty, x, data, Empty, 1)
-      | Node(l, v, d, r, h) as t ->
+      | Node(l, v, d, r, h) ->
           let c = Pervasives.compare x v in
           if c = 0 then
             Node(l, x, data, r, h)
@@ -81,17 +81,28 @@
           let c = Pervasives.compare x v in
           c = 0 || mem x (if c < 0 then l else r)
 
-    let rec merge t1 t2 =
+    let rec min_binding = function
+        Empty -> raise Not_found
+      | Node(Empty, x, d, r, _) -> (x, d)
+      | Node(l, x, d, r, _) -> min_binding l
+
+    let rec remove_min_binding = function
+        Empty -> invalid_arg "Map.remove_min_elt"
+      | Node(Empty, x, d, r, _) -> r
+      | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
+
+    let merge t1 t2 =
       match (t1, t2) with
         (Empty, t) -> t
       | (t, Empty) -> t
-      | (Node(l1, v1, d1, r1, h1), Node(l2, v2, d2, r2, h2)) ->
-          bal l1 v1 d1 (bal (merge r1 l2) v2 d2 r2)
+      | (_, _) ->
+          let (x, d) = min_binding t2 in
+          bal t1 x d (remove_min_binding t2)
 
     let rec remove x = function
         Empty ->
           Empty
-      | Node(l, v, d, r, h) as t ->
+      | Node(l, v, d, r, h) ->
           let c = Pervasives.compare x v in
           if c = 0 then
             merge l r
@@ -109,6 +120,9 @@
         Empty               -> Empty
       | Node(l, v, d, r, h) -> Node(map f l, v, f d, map f r, h)
 
+    (* Maintien de fold_right par compatibilité (changé en fold_left dans
+       ocaml-3.09.0) *)
+
     let rec fold f m accu =
       match m with
         Empty -> accu
diff --git a/lib/gmap.mli b/lib/gmap.mli
index 7415a395..79958fab 100644
--- a/lib/gmap.mli
+++ b/lib/gmap.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: gmap.mli,v 1.4.16.1 2004/07/16 19:30:29 herbelin Exp $ i*)
+(*i $Id: gmap.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* Maps using the generic comparison function of ocaml. Same interface as
    the module [Map] from the ocaml standard library. *)
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
index 5eb4e110..0974909d 100644
--- a/lib/gmapl.ml
+++ b/lib/gmapl.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: gmapl.ml,v 1.2.16.2 2006/01/03 20:31:16 herbelin Exp $ *)
+(* $Id: gmapl.ml 7780 2006-01-03 20:33:53Z herbelin $ *)
 
 open Util
 
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
index f8855ae4..db8f4358 100644
--- a/lib/gmapl.mli
+++ b/lib/gmapl.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: gmapl.mli,v 1.4.16.1 2004/07/16 19:30:30 herbelin Exp $ i*)
+(*i $Id: gmapl.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* Maps from ['a] to lists of ['b]. *)
 
diff --git a/lib/gset.ml b/lib/gset.ml
index 5ea2f82b..e90386a0 100644
--- a/lib/gset.ml
+++ b/lib/gset.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: gset.ml,v 1.2.16.1 2004/07/16 19:30:30 herbelin Exp $ *)
+(* $Id: gset.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (* Sets using the generic comparison function of ocaml. Code borrowed from
    the ocaml standard library. *)
diff --git a/lib/gset.mli b/lib/gset.mli
index 32d798cc..0f14368f 100644
--- a/lib/gset.mli
+++ b/lib/gset.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: gset.mli,v 1.3.16.1 2004/07/16 19:30:30 herbelin Exp $ i*)
+(*i $Id: gset.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* Sets using the generic comparison function of ocaml. Same interface as
    the module [Set] from the ocaml standard library. *)
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 5f083459..50be0ec4 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: hashcons.ml,v 1.3.16.1 2004/07/16 19:30:30 herbelin Exp $ *)
+(* $Id: hashcons.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (* Hash consing of datastructures *)
 
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 2e32323a..f1e55ba1 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: hashcons.mli,v 1.5.16.1 2004/07/16 19:30:30 herbelin Exp $ i*)
+(*i $Id: hashcons.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* Generic hash-consing. *)
 
diff --git a/lib/heap.ml b/lib/heap.ml
index f0db2943..92aa0070 100644
--- a/lib/heap.ml
+++ b/lib/heap.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: heap.ml,v 1.1.2.1 2004/07/16 19:30:30 herbelin Exp $ *)
+(* $Id: heap.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (*s Heaps *)
 
diff --git a/lib/heap.mli b/lib/heap.mli
index 46e72728..d351edd0 100644
--- a/lib/heap.mli
+++ b/lib/heap.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: heap.mli,v 1.1.2.2 2005/01/21 17:14:11 herbelin Exp $ i*)
+(*i $Id: heap.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
 
 (* Heaps *)
 
diff --git a/lib/options.ml b/lib/options.ml
index b5c5efda..0d934922 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: options.ml,v 1.27.2.1 2004/07/16 19:30:30 herbelin Exp $ *)
+(* $Id: options.ml 7740 2005-12-26 20:07:21Z herbelin $ *)
 
 open Util
 
@@ -23,8 +23,6 @@ let debug = ref false
 
 let print_emacs = ref false
 
-let emacs_str s = if !print_emacs then s else "" 
-
 let term_quality = ref false
 
 let xml_export = ref false
@@ -33,22 +31,11 @@ let dont_load_proofs = ref false
 
 let raw_print = ref false
 
-let v7 =
-  let transl = array_exists ((=) "-translate") Sys.argv in
-  let v7 = array_exists ((=) "-v7") Sys.argv in
-  let v8 = array_exists ((=) "-v8") Sys.argv in
-  if v8 & transl then error "Options -translate and -v8 are incompatible";
-  if v8 & v7 then error "Options -v7 and -v8 are incompatible";
-  ref (v7 or transl)
-
-let v7_only = ref false
-
 (* Translate *)
 let translate = ref false
-let make_translate f = translate := f; v7 := f; ()
+let make_translate f = translate := f
 let do_translate () = !translate
 let translate_file = ref false
-let translate_strict_impargs = ref true
 
 (* True only when interning from pp*new.ml *)
 let translate_syntax = ref false
@@ -73,6 +60,8 @@ let silently f x =
 let if_silent f x = if !silent then f x
 let if_verbose f x = if not !silent then f x
 
+let hash_cons_proofs = ref true
+
 (* The number of printed hypothesis in a goal *)
 
 let print_hyps_limit = ref (None : int option)
@@ -105,3 +94,30 @@ let dump_it () =
   end
 
 let _ = at_exit dump_it
+
+(* Options for the virtual machine *)
+
+let boxed_definitions = ref true
+let set_boxed_definitions b = boxed_definitions := b
+let boxed_definitions _ = !boxed_definitions 
+ 
+(* Options for external tools *)
+
+let browser_cmd_fmt =
+ try
+  let coq_netscape_remote_var = "COQREMOTEBROWSER" in
+  let coq_netscape_remote = Sys.getenv coq_netscape_remote_var in
+  let i = Util.string_index_from coq_netscape_remote 0 "%s" in
+  let pre = String.sub coq_netscape_remote 0 i in
+  let post = String.sub coq_netscape_remote (i + 2)
+              (String.length coq_netscape_remote - (i + 2)) in
+   if Util.string_string_contains ~where:post ~what:"%s" then
+    error ("The environment variable \"" ^
+           coq_netscape_remote_var ^
+           "\" must contain exactly one placeholder \"%s\".")
+   else pre,post
+ with
+  Not_found ->
+   if Sys.os_type = "Win32"
+   then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
+   else "netscape -remote \"OpenURL(", ")\""
diff --git a/lib/options.mli b/lib/options.mli
index 731b7da4..1a5444a4 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: options.mli,v 1.25.2.1 2004/07/16 19:30:30 herbelin Exp $ i*)
+(*i $Id: options.mli 7740 2005-12-26 20:07:21Z herbelin $ i*)
 
 (* Global options of the system. *)
 
@@ -17,7 +17,6 @@ val batch_mode : bool ref
 val debug : bool ref
 
 val print_emacs : bool ref
-val emacs_str : string -> string
 
 val term_quality : bool ref
 
@@ -27,15 +26,11 @@ val dont_load_proofs : bool ref
 
 val raw_print : bool ref
 
-val v7 : bool ref
-val v7_only : bool ref
-
 val translate : bool ref
 val make_translate : bool -> unit
 val do_translate : unit -> bool
 val translate_file : bool ref
 val translate_syntax : bool ref
-val translate_strict_impargs : bool ref
 
 val make_silent : bool -> unit
 val is_silent : unit -> bool
@@ -44,6 +39,8 @@ val silently : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
+val hash_cons_proofs : bool ref
+
 (* Temporary activate an option ('c must be an atomic type) *)
 val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 
@@ -60,3 +57,14 @@ val dump : bool ref
 val dump_into_file : string -> unit
 val dump_string : string -> unit
 
+(* Options for the virtual machine *)
+
+val set_boxed_definitions : bool -> unit
+val boxed_definitions : unit -> bool
+
+(* Options for external tools *)
+
+(* Returns head and tail of printf string format *)
+(* ocaml doesn't allow not applied formats *)
+val browser_cmd_fmt : string * string
+ 
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 25ab9ce8..e7ba9869 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pp.ml4,v 1.5.2.1 2004/07/16 19:30:30 herbelin Exp $ *)
+(* $Id: pp.ml4 7751 2005-12-28 12:58:53Z herbelin $ *)
 
 open Pp_control
 
@@ -122,17 +122,17 @@ let int n = str (string_of_int n)
 let real r = str (string_of_float r)
 let bool b = str (string_of_bool b)
 
+(* In new syntax only double quote char is escaped by repeating it *)
 let rec escape_string s =
   let rec escape_at s i =
     if i<0 then s
-    else if s.[i] == '\\' || s.[i] == '"' then
-      let s' = String.sub s 0 i^"\\"^String.sub s i (String.length s - i) in
+    else if s.[i] == '"' then
+      let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
       escape_at s' (i-1)
     else escape_at s (i-1) in
   escape_at s (String.length s - 1)
 
-
-let qstring s = str ("\""^(escape_string s)^"\"")
+let qstring s = str ("\""^escape_string s^"\"")
 let qs = qstring
 
 (* boxing commands *)
@@ -183,7 +183,6 @@ let rec pr_com ft s =
 
 (* pretty printing functions *)
 let pp_dirs ft = 
-  let maxbox = (get_gp ft).max_depth in
   let pp_open_box = function
     | Pp_hbox n   -> Format.pp_open_hbox ft ()
     | Pp_vbox n   -> Format.pp_open_vbox ft n
diff --git a/lib/pp.mli b/lib/pp.mli
index 417ea107..88deb6d2 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pp.mli,v 1.8.2.1 2004/07/16 19:30:30 herbelin Exp $ i*)
+(*i $Id: pp.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (*i*)
 open Pp_control
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 85303f74..7632d736 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pp_control.ml,v 1.8.2.1 2004/07/16 19:30:31 herbelin Exp $ *)
+(* $Id: pp_control.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (* Parameters of pretty-printing *)
 
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 3588847d..7e25e561 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pp_control.mli,v 1.7.2.1 2004/07/16 19:30:31 herbelin Exp $ i*)
+(*i $Id: pp_control.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* Parameters of pretty-printing. *)
 
diff --git a/lib/predicate.ml b/lib/predicate.ml
index 1eaa20ce..93b74463 100644
--- a/lib/predicate.ml
+++ b/lib/predicate.ml
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (************************************************************************)
 
-(* $Id: predicate.ml,v 1.1.14.1 2004/07/16 19:30:31 herbelin Exp $ *)
+(* $Id: predicate.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 (* Sets over ordered types *)
 
diff --git a/lib/predicate.mli b/lib/predicate.mli
index 2dc7d85c..85596fea 100644
--- a/lib/predicate.mli
+++ b/lib/predicate.mli
@@ -1,5 +1,5 @@
 
-(*i $Id: predicate.mli,v 1.1.14.1 2005/01/21 17:14:11 herbelin Exp $ i*)
+(*i $Id: predicate.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
 
 (* Module [Pred]: sets over infinite ordered types with complement. *)
 
diff --git a/lib/profile.ml b/lib/profile.ml
index f55388f8..dd7e977e 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: profile.ml,v 1.13.16.1 2004/07/16 19:30:31 herbelin Exp $ *)
+(* $Id: profile.ml 7538 2005-11-08 17:14:52Z herbelin $ *)
 
 open Gc
 
@@ -259,9 +259,9 @@ let time_overhead_B_C () =
   for i=1 to loops do
     try
       dummy_last_alloc := get_alloc ();
-      let r = dummy_f dummy_x in
-      let dw = dummy_spent_alloc () in
-      let dt = get_time () in
+      let _r = dummy_f dummy_x in
+      let _dw = dummy_spent_alloc () in
+      let _dt = get_time () in
       ()
     with _ -> assert false
   done;
@@ -328,7 +328,7 @@ let close_profile print =
 	outside.owntime <- outside.owntime + t;
 	ajoute_ownalloc outside dw;
 	ajoute_totalloc outside dw;
-	if List.length !prof_table <> 0 then begin
+	if !prof_table <> [] then begin
 	  let ov_bc = time_overhead_B_C () (* B+C overhead *) in
 	  let ov_ad = time_overhead_A_D () (* A+D overhead *) in
 	  let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in
diff --git a/lib/profile.mli b/lib/profile.mli
index e8ce8994..0937e9e3 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: profile.mli,v 1.7.16.2 2005/01/21 17:14:11 herbelin Exp $ i*)
+(*i $Id: profile.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
 
 (*s This program is a small time and allocation profiler for Objective Caml *)
 
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 53cc372f..ab689be1 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -6,16 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rtree.ml,v 1.2.8.1 2004/07/16 19:30:31 herbelin Exp $ i*)
+(*i $Id: rtree.ml 8648 2006-03-18 15:37:14Z herbelin $ i*)
 
 
 (* Type of regular trees:
    - Param denotes tree variables (like de Bruijn indices)
-   - Node denotes the usual tree node, labelles with 'a
+   - Node denotes the usual tree node, labelled with 'a
    - Rec(j,v1..vn) introduces infinite tree. It denotes
      v(j+1) with parameters 0..n-1 replaced by
      Rec(0,v1..vn)..Rec(n-1,v1..vn) respectively.
-     Parameters n and higher denote parameters globals to the
+     Parameters n and higher denote parameters global to the
      current Rec node (as usual in de Bruijn binding system)
  *)
 type 'a t =
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 79b57586..7be96652 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -6,10 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rtree.mli,v 1.2.8.2 2005/01/21 16:41:52 herbelin Exp $ i*)
+(*i $Id: rtree.mli 7493 2005-11-02 22:12:16Z mohring $ i*)
 
 (* Type of regular tree with nodes labelled by values of type 'a *)
-type 'a t
+
+type 'a t 
 
 (* Building trees *)
 (* build a recursive call *) 
diff --git a/lib/stamps.ml b/lib/stamps.ml
index 1697c309..0f481516 100644
--- a/lib/stamps.ml
+++ b/lib/stamps.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: stamps.ml,v 1.2.16.1 2004/07/16 19:30:31 herbelin Exp $ *)
+(* $Id: stamps.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 let new_stamp = 
   let stamp_ctr = ref 0 in
diff --git a/lib/stamps.mli b/lib/stamps.mli
index 36f238b9..6fa3077f 100644
--- a/lib/stamps.mli
+++ b/lib/stamps.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: stamps.mli,v 1.3.16.1 2004/07/16 19:30:31 herbelin Exp $ i*)
+(*i $Id: stamps.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* Time stamps. *)
 
diff --git a/lib/system.ml b/lib/system.ml
index 9bbcc308..fb3cf7b5 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: system.ml,v 1.31.8.3 2006/01/10 17:06:23 barras Exp $ *)
+(* $Id: system.ml 7603 2005-11-23 17:21:53Z barras $ *)
 
 open Pp
 open Util
@@ -34,7 +34,7 @@ let rec expand_atom s i =
   then expand_atom s (i+1)
   else i
 
-let rec expand_macros b s i =
+let rec expand_macros s i =
   let l = String.length s in
   if i=l then s else
     match s.[i] with
@@ -42,9 +42,7 @@ let rec expand_macros b s i =
 	  let n = expand_atom s (i+1) in
 	  let v = safe_getenv (String.sub s (i+1) (n-i-1)) in
 	  let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in
-	  expand_macros false s (i + String.length v)
-      | '/' ->
-	  expand_macros true s (i+1)
+	  expand_macros s (i + String.length v)
       | '~' ->
 	  let n = expand_atom s (i+1) in
 	  let v =
@@ -52,44 +50,16 @@ let rec expand_macros b s i =
 	    else (getpwnam (String.sub s (i+1) (n-i-1))).pw_dir
 	  in
 	  let s = v^(String.sub s n (l-n)) in
-	  expand_macros false s (String.length v)
-      | c -> expand_macros false s (i+1)
+	  expand_macros s (String.length v)
+      | c -> expand_macros s (i+1)
 
-let glob s = expand_macros true s 0
+let glob s = expand_macros s 0
 
 (* Files and load path. *)
 
 type physical_path = string
 type load_path = physical_path list
 
-(* Hints to partially detects if two paths refer to the same repertory *)
-let rec remove_path_dot p = 
-  let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
-  let n = String.length curdir in
-  if String.length p > n && String.sub p 0 n = curdir then
-    remove_path_dot (String.sub p n (String.length p - n))
-  else
-    p
-
-let strip_path p =
-  let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
-  let n = String.length cwd in
-  if String.length p > n && String.sub p 0 n = cwd then
-    remove_path_dot (String.sub p n (String.length p - n))
-  else
-    remove_path_dot p
-
-let canonical_path_name p =
-  let current = Sys.getcwd () in
-  try 
-    Sys.chdir p;
-    let p' = Sys.getcwd () in
-    Sys.chdir current;
-    p'
-  with Sys_error _ ->
-    (* We give up to find a canonical name and just simplify it... *)
-    strip_path p
-
 (* All subdirectories, recursively *)
 
 let exists_dir dir =
@@ -214,6 +184,61 @@ let extern_intern magic suffix =
   in 
   (extern_state,intern_state)
 
+(* Communication through files with another executable *)
+
+let connect writefun readfun com =
+  let name = Filename.basename com in
+  let tmp_to = Filename.temp_file ("coq-"^name^"-in") ".xml" in
+  let tmp_from = Filename.temp_file ("coq-"^name^"-out") ".xml" in
+  let ch_to_in,ch_to_out =
+    try open_in tmp_to, open_out tmp_to
+    with Sys_error s -> error ("Cannot set connection to "^com^"("^s^")") in
+  let ch_from_in,ch_from_out = 
+    try open_in tmp_from, open_out tmp_from
+    with Sys_error s ->
+      close_out ch_to_out; close_in ch_to_in; 
+      error ("Cannot set connection from "^com^"("^s^")") in
+  writefun ch_to_out;
+  close_out ch_to_out;
+  let pid = 
+    let ch_to' = Unix.descr_of_in_channel ch_to_in in
+    let ch_from' = Unix.descr_of_out_channel ch_from_out in
+    try Unix.create_process com [||] ch_to' ch_from' Unix.stdout
+    with Unix.Unix_error (err,_,_) ->
+      close_in ch_to_in; close_in ch_from_in; close_out ch_from_out;
+      unlink tmp_from; unlink tmp_to;
+      error ("Cannot execute "^com^"("^(Unix.error_message err)^")") in
+  close_in ch_to_in;
+  close_out ch_from_out;
+  (match snd (Unix.waitpid [] pid) with
+    | Unix.WEXITED 127 -> error (com^": cannot execute")
+    | Unix.WEXITED 0 -> ()
+    | _ -> error (com^" exited abnormally"));
+  let a = readfun ch_from_in in
+  close_in ch_from_in;
+  unlink tmp_from;
+  unlink tmp_to;
+  a
+
+let run_command converter f c =
+  let result = Buffer.create 127 in
+  let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in
+  let buff = String.make 127 ' ' in
+  let buffe = String.make 127 ' ' in
+  let n = ref 0 in
+  let ne = ref 0 in
+
+  while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; 
+    !n+ !ne <> 0
+  do 
+    let r = converter (String.sub buff 0 !n) in 
+    f r;
+    Buffer.add_string result r;
+    let r = converter (String.sub buffe 0 !ne) in 
+    f r;
+    Buffer.add_string result r 
+  done;
+  (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
 
 (* Time stamps. *)
 
diff --git a/lib/system.mli b/lib/system.mli
index dc172b70..ea463732 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: system.mli,v 1.17.16.3 2006/01/10 17:06:23 barras Exp $ i*)
+(*i $Id: system.mli 7603 2005-11-23 17:21:53Z barras $ i*)
 
 (*s Files and load paths. Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
@@ -16,8 +16,6 @@
 type physical_path = string
 type load_path = physical_path list
 
-val canonical_path_name : string -> physical_path
-
 val all_subdirs : unix_path:string -> (physical_path * string list) list
 val is_in_path : load_path -> string -> bool
 val where_in_path : load_path -> string -> physical_path * string
@@ -48,6 +46,18 @@ val raw_extern_intern : int -> string ->
 val extern_intern : 
   int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a)
 
+(*s Sending/receiving once with external executable *)
+
+val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a 
+
+(*s [run_command converter f com] launches command [com], and returns
+    the contents of stdout and stderr that have been processed with
+    [converter]; the processed contents of stdout and stderr is also
+    passed to [f] *)
+
+val run_command : (string -> string) -> (string -> unit) -> string -> 
+  Unix.process_status * string
+
 (*s Time stamps. *)
 
 type time
@@ -56,5 +66,3 @@ val process_time : unit -> float * float
 val get_time : unit -> time
 val time_difference : time -> time -> float (* in seconds *)
 val fmt_time_difference : time -> time -> Pp.std_ppcmds
-
-
diff --git a/lib/tlm.ml b/lib/tlm.ml
index 23021be4..2939e91a 100644
--- a/lib/tlm.ml
+++ b/lib/tlm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tlm.ml,v 1.3.16.1 2004/07/16 19:30:31 herbelin Exp $ *)
+(* $Id: tlm.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t
 
diff --git a/lib/tlm.mli b/lib/tlm.mli
index a3011932..982bb5ed 100644
--- a/lib/tlm.mli
+++ b/lib/tlm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tlm.mli,v 1.5.16.1 2004/07/16 19:30:31 herbelin Exp $ i*)
+(*i $Id: tlm.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* Tries. This module implements a data structure [('a,'b) t] mapping lists
    of values of type ['a] to sets (as lists) of values of type ['b]. *)
diff --git a/lib/util.ml b/lib/util.ml
index b5470e58..2e6e1279 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1,12 +1,12 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
-(* $Id: util.ml,v 1.84.2.3 2004/07/29 15:00:04 herbelin Exp $ *)
+(* $Id: util.ml 8672 2006-03-29 21:06:33Z herbelin $ *)
 
 open Pp
 
@@ -32,8 +32,9 @@ type 'a located = loc * 'a
 let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
 let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
 let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
-let join_loc (deb1,_ as loc1) (_,fin2 as loc2) = 
-  if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc else (deb1,fin2)
+let join_loc loc1 loc2 =
+  if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
+  else (fst loc1, snd loc2)
 
 (* Like Exc_located, but specifies the outermost file read, the filename
    associated to the location of the error, and the error itself. *)
@@ -98,6 +99,8 @@ let string_string_contains ~where ~what =
   with
       Not_found -> false
 
+let plural n s = if n>1 then s^"s" else s
+
 (* string parsing *)
 
 let parse_loadpath s =
@@ -118,10 +121,6 @@ module Stringset = Set.Make(struct type t = string let compare = compare end)
 
 module Stringmap = Map.Make(struct type t = string let compare = compare end)
 
-let stringmap_to_list m = Stringmap.fold (fun s y l -> (s,y)::l) m []
-
-let stringmap_dom m = Stringmap.fold (fun s _ l -> s::l) m []
-
 (* Lists *)
 
 let list_add_set x l = if List.mem x l then l else x::l
@@ -251,6 +250,13 @@ let list_for_all_i p =
 
 let list_except x l = List.filter (fun y -> not (x = y)) l
 
+let list_remove = list_except (* Alias *)
+
+let rec list_remove_first a = function
+  | b::l when a = b -> l
+  | b::l -> b::list_remove_first a l
+  | [] -> raise Not_found
+
 let list_for_all2eq f l1 l2 = try List.for_all2 f l1 l2 with Failure _ -> false
 
 let list_map_i f = 
@@ -362,12 +368,12 @@ let list_share_tails l1 l2 =
 
 let list_join_map f l = List.flatten (List.map f l)
 
-let rec list_fold_map f e = function 
+let rec list_fold_map f e = function
   |  []  -> (e,[])
-  |  h::t -> 
+  |  h::t ->
        let e',h' = f e h in
        let e'',t' = list_fold_map f e' t in
-	 e'',h'::t'
+         e'',h'::t'
 
 (* (* tail-recursive version of the above function *)
 let list_fold_map f e l = 
@@ -379,6 +385,10 @@ let list_fold_map f e l =
     (e',List.rev lrev)
 *)
 
+(* The same, based on fold_right, with the effect accumulated on the right *)
+let list_fold_map' f l e =
+  List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e)
+
 let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
 
 (* Arrays *)
@@ -596,6 +606,20 @@ let array_map_left_pair f a g b =
     r, s
   end
 
+let pure_functional = false
+
+let array_fold_map' f v e =
+if pure_functional then
+  let (l,e) =
+    Array.fold_right 
+      (fun x (l,e) -> let (y,e) = f x e in (y::l,e))
+      v ([],e) in
+  (Array.of_list l,e)
+else
+  let e' = ref e in
+  let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in
+  (v',!e')
+
 (* Matrices *)
 
 let matrix_transpose mat =
@@ -693,6 +717,8 @@ let pr_str = str
 let pr_coma () = str "," ++ spc ()
 let pr_semicolon () = str ";" ++ spc ()
 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
diff --git a/lib/util.mli b/lib/util.mli
index 19f05ea4..f77aa6b4 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -1,12 +1,12 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
-(*i $Id: util.mli,v 1.84.2.2 2004/07/16 20:43:46 herbelin Exp $ i*)
+(*i $Id: util.mli 8672 2006-03-29 21:06:33Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -68,16 +68,13 @@ val explode : string -> string list
 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 parse_loadpath : string -> string list
 
 module Stringset : Set.S with type elt = string
-
 module Stringmap : Map.S with type key = string
 
-val stringmap_to_list : 'a Stringmap.t -> (string * 'a) list 
-val stringmap_dom : 'a Stringmap.t -> string list
-
 (*s Lists. *)
 
 val list_add_set : 'a -> 'a list -> 'a list
@@ -109,6 +106,8 @@ val list_fold_right_and_left :
     ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
 val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 val list_except : 'a -> 'a list -> 'a list
+val list_remove : 'a -> 'a list -> 'a list
+val list_remove_first : 'a -> 'a list -> 'a list
 val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
 val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
@@ -130,8 +129,8 @@ val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
 val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
 (* [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
    where [(e_i,k_i)=f e_{i-1} l_i] *)
-val list_fold_map : 
-  ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list 
+val list_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+val list_fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
 val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
 
 (*s Arrays. *)
@@ -170,6 +169,7 @@ val array_map3 :
 val array_map_left : ('a -> 'b) -> 'a array -> 'b array
 val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array ->
   'b array * 'd array
+val array_fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
 
 (*s Matrices *)
 
@@ -223,6 +223,8 @@ 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 prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds