Merge branch 'experimental/upstream' into upstream

66 files changed, 2628 insertions, 1389 deletions

diff --git a/lib/bigint.ml b/lib/bigint.ml
index f3808f14..9185ba64 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -1,41 +1,38 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: bigint.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-(*i*)
-open Pp
-(*i*)
-
 (***************************************************)
 (* Basic operations on (unbounded) integer numbers *)
 (***************************************************)
 
-(* An integer is canonically represented as an array of k-digits blocs.
+(* An integer is canonically represented as an array of k-digits blocs,
+   i.e. in base 10^k.
 
    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[.
+   The first bloc is in the range ]0;base[ for positive numbers.
+   The first bloc is in the range [-base;-1[ for numbers < -1.
+   All other blocs are numbers in the range [0;base[.
 
-   Negative numbers are represented using 2's complementation. For instance,
-   with 4-digits blocs, [-9655;6789] denotes -96543211
-*)
+   Negative numbers are represented using 2's complementation :
+   one unit is "borrowed" from the top block for complementing
+   the other blocs. For instance, with 4-digits blocs,
+   [|-5;6789|] denotes -43211
+   since -5.10^4+6789=-((4.10^4)+(10000-6789)) = -43211
 
-(* The base is a power of 10 in order to facilitate the parsing and printing
+   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)
+   In practice, we set k=4 on 32-bits machines, 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). On 64-bits machines, k=9.
 *)
 
 (* The main parameters *)
@@ -47,6 +44,7 @@ let size =
 let format_size =
   (* How to parametrize a printf format *)
   if size = 4 then Printf.sprintf "%04d"
+  else if size = 9 then Printf.sprintf "%09d"
   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)
@@ -56,44 +54,81 @@ let format_size =
 let base =
   let rec exp10 = function 0 -> 1 | n -> 10 * exp10 (n-1) in exp10 size
 
+(******************************************************************)
+(* First, we represent all numbers by int arrays.
+   Later, we will optimize the particular case of small integers  *)
+(******************************************************************)
+
+module ArrayInt = struct
+
 (* 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
+(* An array is canonical when
+   - it is empty
+   - it is [|-1|]
+   - its first bloc is in [-base;-1[U]0;base[
+     and the other blocs are in [0;base[. *)
+
+let canonical n =
+  let ok x = (0 <= x && x < base) in
+  let rec ok_tail k = (k = 0) || (ok n.(k) && ok_tail (k-1)) in
+  let ok_init x = (-base <= x && x < base && x <> -1 && x <> 0)
+  in
+  (n = [||]) || (n = [|-1|]) ||
+    (ok_init n.(0) && ok_tail (Array.length n - 1))
+
+(* [normalize_pos] : removing initial blocks of 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)
 
+(* [normalize_neg] : avoid (-1) as first bloc.
+   input: an array with -1 as first bloc and other blocs in [0;base[
+   output: a canonical array *)
+
 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')
 
+(* [normalize] : avoid 0 and (-1) as first bloc.
+   input: an array with first bloc in [-base;base[ and others in [0;base[
+   output: a canonical array *)
+
 let rec normalize n =
-  if Array.length n = 0 then n else
-    if n.(0) = -1 then normalize_neg n else normalize_pos n
+  if Array.length n = 0 then n
+  else if n.(0) = -1 then normalize_neg n
+  else if n.(0) = 0 then normalize_pos n
+  else n
+
+(* Opposite (expects and returns canonical arrays) *)
 
 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
+  if !i = 0 then begin
+    n.(0) <- - n.(0);
+    (* n.(0) cannot be 0 since m is canonical *)
+    if n.(0) = -1 then normalize_neg n
+    else if n.(0) = base then (n.(0) <- 0; Array.append [| 1 |] n)
+    else n
+  end else begin
+    (* here n.(!i) <> 0, hence 0 < base - n.(!i) < base for n canonical *)
     n.(!i) <- base - n.(!i); decr i;
     while !i > 0 do n.(!i) <- base - 1 - n.(!i); decr i done;
+    (* since -base <= n.(0) <= base-1, hence -base <= -n.(0)-1 <= base-1 *)
     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)
+    (* since m is canonical, m.(0)<>0 hence n.(0)<>-1,
+       and m=-1 is already handled above, so here m.(0)<>-1 hence n.(0)<>0 *)
+    n
+  end
 
 let push_carry r j =
   let j = ref j in
@@ -103,10 +138,10 @@ let push_carry r j =
   while !j > 0 & r.(!j) >= base do
     r.(!j) <- r.(!j) - base; decr j; r.(!j) <- r.(!j) + 1
   done;
+  (* here r.(0) could be in [-2*base;2*base-1] *)
   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
+  else normalize r (* in case r.(0) is 0 or -1 *)
 
 let add_to r a j =
   if a = zero then r else begin
@@ -154,6 +189,13 @@ let rec mult m n =
   done;
   normalize r
 
+(* Comparisons *)
+
+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 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)))
@@ -166,6 +208,8 @@ let less_than m n =
     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))
 
+(* For this equality test it is critical that n and m are canonical *)
+
 let equal m n = (m = n)
 
 let less_than_shift_pos k m n =
@@ -177,16 +221,30 @@ let rec can_divide k m d i =
   (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 *)
+(* For two big nums m and d and a small number q,
+   computes m - d * q * base^(|m|-|d|-k) in-place (in m).
+   Both m d and q are positive. *)
+
 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;
+    if v >= base then begin
+      m.(k+i-1) <- m.(k+i-1) - v / base;
+      let j = ref (i-1) in
+      while m.(k + !j) < 0 do (* result is positive, hence !j remains >= 0 *)
+        m.(k + !j) <- m.(k + !j) + base; decr j; m.(k + !j) <- m.(k + !j) -1
+      done
+    end
   done
 
+(** Euclid division m/d = (q,r)
+    This is the "Floor" variant, as with ocaml's /
+    (but not as ocaml's Big_int.quomod_big_int).
+    We have sign r = sign m *)
+
 let euclid m d =
   let isnegm, m =
     if is_strictly_neg m then (-1),neg m else 1,Array.copy m in
@@ -224,33 +282,21 @@ let euclid m d =
 (* 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 len = String.length s in
+  let isneg = len > 1 & s.[0] = '-' in
+  let d = ref (if isneg then 1 else 0) in
+  while !d < len && s.[!d] = '0' do incr d done;
+  if !d = len then zero else
+  let r = (len - !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 l = (len - !d) / size in
+  let a = Array.create (l + e) 0 in
+  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;
+  if isneg then neg a else a
 
 let to_string_pos sgn n =
    if Array.length n = 0 then "0" else
@@ -262,25 +308,44 @@ let to_string n =
   if is_strictly_neg n then to_string_pos "-" (neg n)
   else to_string_pos "" n
 
+end
+
 (******************************************************************)
 (* Optimized operations on (unbounded) integer numbers            *)
 (* integers smaller than base are represented as machine integers *)
 (******************************************************************)
 
+open ArrayInt
+
 type bigint = Obj.t
 
+(* Since base is the largest power of 10 such that base*base <= max_int,
+   we have max_int < 100*base*base : any int can be represented
+   by at most three blocs *)
+
+let small n = (-base <= n) && (n < base)
+
+let mkarray n =
+  (* n isn't small, this case is handled separately below *)
+  let lo = n mod base
+  and hi = n / base in
+  let t = if small hi then [|hi;lo|] else [|hi/base;hi mod base;lo|]
+  in
+  for i = Array.length t -1 downto 1 do
+    if t.(i) < 0 then (t.(i) <- t.(i) + base; t.(i-1) <- t.(i-1) -1)
+  done;
+  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 |]
+  if n = 0 then [| |]
+  else if small n then [| n |]
+  else mkarray 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 of_int n =
+  if small n then Obj.repr n else Obj.repr (mkarray n)
 
-let big_of_ints n =
-  let n = normalize n in
+let of_ints n =
+  let n = normalize n in (* TODO: using normalize here seems redundant now *)
   if n = zero then Obj.repr 0 else
   if Array.length n = 1 then Obj.repr n.(0) else
   Obj.repr n
@@ -288,63 +353,81 @@ let big_of_ints 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 =
+let to_ints n =
   if Obj.is_int n then ints_of_int (coerce_to_int n)
   else coerce_to_ints n
 
+let int_of_ints =
+  let maxi = mkarray max_int and mini = mkarray min_int in
+  fun t ->
+    let l = Array.length t in
+    if (l > 3) || (l = 3 && (less_than maxi t || less_than t mini))
+    then failwith "Bigint.to_int: too large";
+    let sum = ref 0 in
+    let pow = ref 1 in
+    for i = l-1 downto 0 do
+      sum := !sum + t.(i) * !pow;
+      pow := !pow*base;
+    done;
+    !sum
+
+let to_int n =
+  if Obj.is_int n then coerce_to_int n
+  else int_of_ints (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))
+  then of_int (coerce_to_int m + coerce_to_int n)
+  else of_ints (add (to_ints m) (to_ints 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))
+  then of_int (coerce_to_int m - coerce_to_int n)
+  else of_ints (sub (to_ints m) (to_ints 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))
+  then of_int (coerce_to_int m * coerce_to_int n)
+  else of_ints (mult (to_ints m) (to_ints n))
 
 let euclid m n =
   if Obj.is_int m & Obj.is_int n
-  then app_pair big_of_int
+  then app_pair 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))
+  else app_pair of_ints (euclid (to_ints m) (to_ints 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)
+  else less_than (to_ints m) (to_ints 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))
+  if Obj.is_int n then of_int (- (coerce_to_int n))
+  else of_ints (neg (to_ints n))
 
-let of_string m = big_of_ints (of_string m)
-let to_string m = to_string (ints_of_z m)
+let of_string m = of_ints (of_string m)
+let to_string m = to_string (to_ints m)
 
-let zero = big_of_int 0
-let one = big_of_int 1
+let zero = of_int 0
+let one = of_int 1
+let two = of_int 2
 let sub_1 n = sub n one
 let add_1 n = add n one
-let two = big_of_int 2
 let mult_2 n = add n n
 
 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 is_strictly_neg n = is_strictly_neg (to_ints n)
+let is_strictly_pos n = is_strictly_pos (to_ints n)
+let is_neg_or_zero n = is_neg_or_zero (to_ints n)
+let is_pos_or_zero n = is_pos_or_zero (to_ints n)
 
-let pr_bigint n = str (to_string n)
+let equal m n = (m = n)
 
 (* spiwack: computes n^m *)
 (* The basic idea of the algorithm is that n^(2m) = (n^2)^m *)
@@ -354,58 +437,68 @@ let pr_bigint n = str (to_string n)
     k*n^(2m+1) = (n*k)*(n*n)^m *)
 let pow  =
   let rec pow_aux odd_rest n m = (* odd_rest is the k from above *)
-    if is_neg_or_zero m then
+    if m<=0 then
       odd_rest
     else
-      let (quo,rem) = div2_with_rest m in
+      let quo = m lsr 1 (* i.e. m/2 *)
+      and odd = (m land 1) <> 0 in
       pow_aux
-	((* [if m mod 2 = 1]*)
-         if rem then
-          mult n odd_rest
-	 else
-          odd_rest )
-	(* quo = [m/2] *)
-	(mult n n) quo
+	(if odd then mult n odd_rest else odd_rest)
+	(mult n n)
+	quo
   in
   pow_aux one
 
-(* Testing suite *)
+(** Testing suite w.r.t. OCaml's Big_int *)
+
+(*
+module B = struct
+  open Big_int
+  let zero = zero_big_int
+  let to_string = string_of_big_int
+  let of_string = big_int_of_string
+  let add = add_big_int
+  let opp = minus_big_int
+  let sub = sub_big_int
+  let mul = mult_big_int
+  let abs = abs_big_int
+  let sign = sign_big_int
+  let euclid n m =
+    let n' = abs n and m' = abs m in
+    let q',r' = quomod_big_int n' m' in
+    (if sign (mul n m) < 0 && sign q' <> 0 then opp q' else q'),
+    (if sign n < 0 then opp r' else r')
+end
 
 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"
-  ]
+  let roots = [ 1; 100; base; 100*base; base*base ] in
+  let rands = [ 1234; 5678; 12345678; 987654321 ] in
+  let nums = (List.flatten (List.map (fun x -> [x-1;x;x+1]) roots)) @ rands in
+  let numbers =
+    List.map string_of_int nums @
+    List.map (fun n -> string_of_int (-n)) nums
   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' =
+  let compare op x y 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;
+    let s' = Printf.sprintf "%30s" (B.to_string n') in
+    if s <> s' then Printf.printf "%s%s%s: %s <> %s\n" x op y s s' in
+  let test x y =
+    let n = of_string x and m = of_string y in
+    let n' = B.of_string x and m' = B.of_string y in
+    let a = add n m and a' = B.add n' m' in
+    let s = sub n m and s' = B.sub n' m' in
+    let p = mult n m and p' = B.mul n' m' in
+    let q,r = try euclid n m with Division_by_zero -> zero,zero
+    and q',r' = try B.euclid n' m' with Division_by_zero -> B.zero, B.zero
+    in
+    compare "+" x y a a';
+    compare "-" x y s s';
+    compare "*" x y p p';
+    compare "/" x y q q';
+    compare "%" x y r r'
+  in
+  List.iter (fun a -> List.iter (test a) numbers) numbers;
   Printf.printf "%i tests done\n" !i
-
-
+*)
diff --git a/lib/bigint.mli b/lib/bigint.mli
index 9a890570..754f10d6 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -1,29 +1,26 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: bigint.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
-open Pp
-(*i*)
-
-(* Arbitrary large integer numbers *)
+(** Arbitrary large integer numbers *)
 
 type bigint
 
 val of_string : string -> bigint
 val to_string : bigint -> string
 
+val of_int : int -> bigint
+val to_int : bigint -> int (** May raise a Failure on oversized numbers *)
+
 val zero : bigint
 val one : bigint
 val two : bigint
 
-val div2_with_rest : bigint -> bigint * bool (* true=odd; false=even *)
+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
@@ -42,6 +39,4 @@ val is_pos_or_zero : bigint -> bool
 val is_neg_or_zero : bigint -> bool
 val neg : bigint -> bigint
 
-val pow : bigint -> bigint -> bigint
-
-val pr_bigint : bigint -> std_ppcmds
+val pow : bigint -> int -> bigint
diff --git a/lib/bstack.ml b/lib/bstack.ml
deleted file mode 100644
index 3d549427..00000000
--- a/lib/bstack.ml
+++ /dev/null
@@ -1,75 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: bstack.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-(* Queues of a given length *)
-
-open Util
-
-(* - size  is the count of elements actually in the queue
-   - depth is the the amount of elements pushed in the queue (and not popped)
-   in particular, depth >= size always and depth > size if the queue overflowed
-   (and forgot older elements)
- *)
-
-type 'a t = {mutable pos : int;
-             mutable size : int;
-             mutable depth : int;
-             stack : 'a array}
-
-let create depth e =
-  {pos = 0;
-   size = 1;
-   depth = 1;
-   stack = Array.create depth e}
-
-(*
-let set_depth bs n = bs.depth <- n
-*)
-
-let incr_pos bs =
-  bs.pos <- if bs.pos = Array.length bs.stack - 1 then 0 else bs.pos + 1
-
-let incr_size bs =
-  if bs.size < Array.length bs.stack then bs.size <- bs.size + 1
-
-let decr_pos bs =
-  bs.pos <- if bs.pos = 0 then Array.length bs.stack - 1 else bs.pos - 1
-
-let push bs e =
-  incr_pos bs;
-  incr_size bs;
-  bs.depth <- bs.depth + 1;
-  bs.stack.(bs.pos) <- e
-
-let pop bs =
-  if bs.size > 1 then begin
-    bs.size <- bs.size - 1;
-    bs.depth <- bs.depth - 1;
-    let oldpos = bs.pos in
-    decr_pos bs;
-    (* Release the memory at oldpos, by copying what is at new pos *)
-    bs.stack.(oldpos) <- bs.stack.(bs.pos)
-  end
-
-let top bs =
-  if bs.size >= 1 then bs.stack.(bs.pos)
-  else error "Nothing on the stack"
-
-let app_push bs f =
-  if bs.size = 0 then error "Nothing on the stack"
-  else push bs (f (bs.stack.(bs.pos)))
-
-let app_repl bs f =
-  if bs.size = 0 then error "Nothing on the stack"
-  else bs.stack.(bs.pos) <- f (bs.stack.(bs.pos))
-
-let depth bs = bs.depth
-
-let size bs = bs.size
diff --git a/lib/bstack.mli b/lib/bstack.mli
deleted file mode 100644
index 39a5202a..00000000
--- a/lib/bstack.mli
+++ /dev/null
@@ -1,22 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: bstack.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Bounded stacks. If the depth is [None], then there is no depth limit. *)
-
-type 'a t
-
-val create : int -> 'a -> 'a t
-val push : 'a t -> 'a -> unit
-val app_push : 'a t -> ('a -> 'a) -> unit
-val app_repl : 'a t -> ('a -> 'a) -> unit
-val pop : 'a t -> unit
-val top : 'a t -> 'a
-val depth : 'a t -> int
-val size : 'a t -> int
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index a0264dc7..a428ec10 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -1,83 +1,242 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_macro.cmo" i*)
+(** Compatibility file depending on ocaml/camlp4 version *)
 
-(* Compatibility file depending on ocaml version *)
+(** Locations *)
 
-IFDEF OCAML309 THEN DEFINE OCAML308 END
+IFDEF CAMLP5 THEN
+
+module Loc = struct
+  include Ploc
+  exception Exc_located = Exc
+  let ghost = dummy
+  let merge = encl
+end
+
+let make_loc = Loc.make_unlined
+let unloc loc = (Loc.first_pos loc, Loc.last_pos loc)
+
+ELSE
+
+module Loc = Camlp4.PreCast.Loc
+
+let make_loc (start,stop) =
+  Loc.of_tuple ("", 0, 0, start, 0, 0, stop, false)
+let unloc loc = (Loc.start_off loc, Loc.stop_off loc)
+
+END
+
+(** Misc module emulation *)
+
+IFDEF CAMLP5 THEN
+
+module PcamlSig = struct end
+
+ELSE
+
+module PcamlSig = Camlp4.Sig
+module Ast = Camlp4.PreCast.Ast
+module Pcaml = Camlp4.PreCast.Syntax
+module MLast = Ast
+module Token = struct exception Error of string end
+
+END
+
+
+(** Grammar auxiliary types *)
+
+IFDEF CAMLP5 THEN
+type gram_assoc = Gramext.g_assoc = NonA | RightA | LeftA
+type gram_position = Gramext.position =
+  | First
+  | Last
+  | Before of string
+  | After of string
+  | Like of string (** dont use it, not in camlp4 *)
+  | Level of string
+ELSE
+type gram_assoc = PcamlSig.Grammar.assoc = NonA | RightA | LeftA
+type gram_position = PcamlSig.Grammar.position =
+  | First
+  | Last
+  | Before of string
+  | After of string
+  | Level of string
+END
+
+
+(** Signature of Lexer *)
+
+IFDEF CAMLP5 THEN
+
+module type LexerSig = sig
+  include Grammar.GLexerType with type te = Tok.t
+  module Error : sig
+    type t
+    exception E of t
+    val to_string : t -> string
+  end
+end
+
+ELSE
+
+module type LexerSig =
+  Camlp4.Sig.Lexer with module Loc = Loc and type Token.t = Tok.t
+
+END
+
+(** Signature and implementation of grammars *)
 
 IFDEF CAMLP5 THEN
-module M = struct
-type loc = Stdpp.location
-exception Exc_located = Ploc.Exc
-let dummy_loc = Stdpp.dummy_loc
-let make_loc = Stdpp.make_loc
-let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc
-let join_loc loc1 loc2 =
- if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
- else Stdpp.encl_loc loc1 loc2
-type token = string*string
-type lexer = token Token.glexer
+
+module type GrammarSig = sig
+  include Grammar.S with type te = Tok.t
+  type 'a entry = 'a Entry.e
+  type internal_entry = Tok.t Gramext.g_entry
+  type symbol = Tok.t Gramext.g_symbol
+  type action = Gramext.g_action
+  type production_rule = symbol list * action
+  type single_extend_statment =
+      string option * gram_assoc option * production_rule list
+  type extend_statment =
+      gram_position option * single_extend_statment list
+  val action : 'a -> action
+  val entry_create : string -> 'a entry
+  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_print : 'a entry -> unit
+  val srules' : production_rule list -> symbol
+  val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
 end
-ELSE IFDEF OCAML308 THEN
-module M = struct
-exception Exc_located = Stdpp.Exc_located
-type loc = Token.flocation
-let dummy_loc = Token.dummy_loc
-let make_loc loc = Token.make_loc loc
-let unloc (b,e) =
-  let loc = (b.Lexing.pos_cnum,e.Lexing.pos_cnum) in
-  (* Ensure that we unpack a char location that was encoded as a line-col
-     location by make_loc *)
-(* Gram.Entry.parse may send bad loc in 3.08, see caml-bugs #2954
-  assert (dummy_loc = (b,e) or make_loc loc = (b,e));
-*)
-  loc
-let join_loc loc1 loc2 =
- if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
- else (fst loc1, snd loc2)
-type token = Token.t
-type lexer = Token.lexer
+
+module GrammarMake (L:LexerSig) : GrammarSig = struct
+  include Grammar.GMake (L)
+  type 'a entry = 'a Entry.e
+  type internal_entry = Tok.t Gramext.g_entry
+  type symbol = Tok.t Gramext.g_symbol
+  type action = Gramext.g_action
+  type production_rule = symbol list * action
+  type single_extend_statment =
+      string option * gram_assoc option * production_rule list
+  type extend_statment =
+      gram_position option * single_extend_statment list
+  let action = Gramext.action
+  let entry_create = Entry.create
+  let entry_parse = Entry.parse
+IFDEF CAMLP5_6_02_1 THEN
+  let entry_print x = Entry.print !Pp_control.std_ft x
+ELSE
+  let entry_print = Entry.print
+END
+  let srules' = Gramext.srules
+  let parse_tokens_after_filter = Entry.parse_token
 end
+
 ELSE
-module M = struct
-exception Exc_located = Stdpp.Exc_located
-type loc = int * int
-let dummy_loc = (0,0)
-let make_loc x = x
-let unloc x = x
-let join_loc loc1 loc2 =
- if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
- else (fst loc1, snd loc2)
-type token = Token.t
-type lexer = Token.lexer
+
+module type GrammarSig = sig
+  include Camlp4.Sig.Grammar.Static
+    with module Loc = Loc and type Token.t = Tok.t
+  type 'a entry = 'a Entry.t
+  type action = Action.t
+  type parsable
+  val parsable : char Stream.t -> parsable
+  val action : 'a -> action
+  val entry_create : string -> 'a entry
+  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_print : 'a entry -> unit
+  val srules' : production_rule list -> symbol
+end
+
+module GrammarMake (L:LexerSig) : GrammarSig = struct
+  include Camlp4.Struct.Grammar.Static.Make (L)
+  type 'a entry = 'a Entry.t
+  type action = Action.t
+  type parsable = char Stream.t
+  let parsable s = s
+  let action = Action.mk
+  let entry_create = Entry.mk
+  let entry_parse e s = parse e (*FIXME*)Loc.ghost s
+  let entry_print x = Entry.print !Pp_control.std_ft x
+  let srules' = srules (entry_create "dummy")
 end
+
 END
+
+
+(** Misc functional adjustments *)
+
+(** - The lexer produces streams made of pairs in camlp4 *)
+
+let get_tok = IFDEF CAMLP5 THEN fun x -> x ELSE fst END
+
+(** - Gram.extend is more currified in camlp5 than in camlp4 *)
+
+IFDEF CAMLP5 THEN
+let maybe_curry f x y = f (x,y)
+let maybe_uncurry f (x,y) = f x y
+ELSE
+let maybe_curry f = f
+let maybe_uncurry f = f
+END
+
+(** Compatibility with camlp5 strict mode *)
+IFDEF CAMLP5 THEN
+  IFDEF STRICT THEN
+    let vala x = Ploc.VaVal x
+  ELSE
+    let vala x = x
+  END
+ELSE
+  let vala x = x
 END
 
-type loc = M.loc
-exception Exc_located = M.Exc_located
-let dummy_loc = M.dummy_loc
-let make_loc = M.make_loc
-let unloc = M.unloc
-let join_loc = M.join_loc
-type token = M.token
-type lexer = M.lexer
+(** Fix a quotation difference in [str_item] *)
+
+let declare_str_items loc l =
+IFDEF CAMLP5 THEN
+  MLast.StDcl (loc, vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)
+ELSE
+  Ast.stSem_of_list l
+END
 
-IFDEF CAMLP5_6_00 THEN
+(** Quotation difference for match clauses *)
 
-let slist0sep x y = Gramext.Slist0sep (x, y, false)
-let slist1sep x y = Gramext.Slist1sep (x, y, false)
+let default_patt loc =
+  (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>)
+
+IFDEF CAMLP5 THEN
+
+let make_fun loc cl =
+  let l = cl @ [default_patt loc] in
+  MLast.ExFun (loc, vala l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)
 
 ELSE
 
-let slist0sep x y = Gramext.Slist0sep (x, y)
-let slist1sep x y = Gramext.Slist1sep (x, y)
+let make_fun loc cl =
+  let mk_when = function
+    | Some w -> w
+    | None -> Ast.ExNil loc
+  in
+  let mk_clause (patt,optwhen,expr) =
+    (* correspond to <:match_case< ... when ... -> ... >> *)
+    Ast.McArr (loc, patt, mk_when optwhen, expr) in
+  let init = mk_clause (default_patt loc) in
+  let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in
+  let l = List.fold_right add_clause cl init in
+  Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *)
+
+END
+
+(** Explicit antiquotation $anti:... $ *)
 
+IFDEF CAMLP5 THEN
+let expl_anti loc e = <:expr< $anti:e$ >>
+ELSE
+let expl_anti _loc e = e (* FIXME: understand someday if we can do better *)
 END
diff --git a/lib/dnet.ml b/lib/dnet.ml
index fe20ecac..0562cc40 100644
--- a/lib/dnet.ml
+++ b/lib/dnet.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
-
 (* Generic dnet implementation over non-recursive types *)
 
 module type Datatype =
diff --git a/lib/dnet.mli b/lib/dnet.mli
index eba2220b..7ce43bd5 100644
--- a/lib/dnet.mli
+++ b/lib/dnet.mli
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id:$ *)
-
-(* Generic discrimination net implementation over recursive
+(** Generic discrimination net implementation over recursive
    types. This module implements a association data structure similar
    to tries but working on any types (not just lists). It is a term
    indexing datastructure, a generalization of the discrimination nets
@@ -43,27 +41,27 @@
 
 *)
 
-(* datatype you want to build a dnet on *)
+(** datatype you want to build a dnet on *)
 module type Datatype =
 sig
-  (* parametric datatype. ['a] is morally the recursive argument *)
+  (** parametric datatype. ['a] is morally the recursive argument *)
   type 'a t
 
-  (* non-recursive mapping of subterms *)
+  (** non-recursive mapping of subterms *)
   val map : ('a -> 'b) -> 'a t -> 'b t
   val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
 
-  (* non-recursive folding of subterms *)
+  (** non-recursive folding of subterms *)
   val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
   val fold2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a
 
-  (* comparison of constructors *)
+  (** comparison of constructors *)
   val compare : unit t -> unit t -> int
 
-  (* for each constructor, is it not-parametric on 'a? *)
+  (** for each constructor, is it not-parametric on 'a? *)
   val terminal : 'a t -> bool
 
-  (* [choose f w] applies f on ONE of the subterms of w *)
+  (** [choose f w] applies f on ONE of the subterms of w *)
   val choose : ('a -> 'b) -> 'a t -> 'b
 end
 
@@ -71,19 +69,19 @@ module type S =
 sig
   type t
 
-  (* provided identifier type *)
+  (** provided identifier type *)
   type ident
 
-  (* provided metavariable type *)
+  (** provided metavariable type *)
   type meta
 
-  (* provided parametrized datastructure *)
+  (** provided parametrized datastructure *)
   type 'a structure
 
-  (* returned sets of solutions *)
+  (** returned sets of solutions *)
   module Idset : Set.S with type elt=ident
 
-  (* a pattern is a term where each node can be a unification
+  (** a pattern is a term where each node can be a unification
      variable *)
   type 'a pattern =
     | Term of 'a
@@ -93,13 +91,13 @@ sig
 
   val empty : t
 
-  (* [add t w i] adds a new association (w,i) in t. *)
+  (** [add t w i] adds a new association (w,i) in t. *)
   val add : t -> term_pattern -> ident -> t
 
-  (* [find_all t] returns all identifiers contained in t. *)
+  (** [find_all t] returns all identifiers contained in t. *)
   val find_all : t -> Idset.t
 
-  (* [fold_pattern f acc p dn] folds f on each meta of p, passing the
+  (** [fold_pattern f acc p dn] folds f on each meta of p, passing the
      meta and the sub-dnet under it. The result includes:
      - Some set if identifiers were gathered on the leafs of the term
      - None if the pattern contains no leaf (only Metas at the leafs).
@@ -107,15 +105,15 @@ sig
   val fold_pattern :
     ('a -> (Idset.t * meta * t) -> 'a) -> 'a -> term_pattern -> t -> Idset.t option * 'a
 
-  (* [find_match p t] returns identifiers of all terms matching p in
+  (** [find_match p t] returns identifiers of all terms matching p in
      t. *)
   val find_match : term_pattern -> t -> Idset.t
 
-  (* set operations on dnets *)
+  (** set operations on dnets *)
   val inter : t -> t -> t
   val union : t -> t -> t
 
-  (* apply a function on each identifier and node of terms in a dnet *)
+  (** apply a function on each identifier and node of terms in a dnet *)
   val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
 end
 
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 2748422a..b795a4b4 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dyn.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 
 (* Dynamics, programmed with DANGER !!! *)
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 0d36dbef..9173e810 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: dyn.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Dynamics. Use with extreme care. Not for kids. *)
+(** Dynamics. Use with extreme care. Not for kids. *)
 
 type t
 
diff --git a/lib/edit.ml b/lib/edit.ml
deleted file mode 100644
index 882303a6..00000000
--- a/lib/edit.ml
+++ /dev/null
@@ -1,134 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: edit.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-open Pp
-open Util
-
-type ('a,'b,'c) t = {
-  mutable focus : 'a option;
-  mutable last_focused_stk : 'a list;
-  buf : ('a, 'b Bstack.t * 'c) Hashtbl.t }
-
-let empty () = {
-  focus = None;
-  last_focused_stk = [];
-  buf = Hashtbl.create 17 }
-
-let focus e nd =
-  if not (Hashtbl.mem e.buf nd) then invalid_arg "Edit.focus";
-  begin match e.focus with
-    | Some foc when foc <> nd ->
-        e.last_focused_stk <- foc::(list_except foc e.last_focused_stk);
-    | _ -> ()
-  end;
-  e.focus <- Some nd
-
-let unfocus e =
-  match e.focus with
-    | None -> invalid_arg "Edit.unfocus"
-    | Some foc ->
-	begin
-	  e.last_focused_stk <- foc::(list_except foc e.last_focused_stk);
-	  e.focus <- None
-	end
-
-let last_focused e =
-  match e.last_focused_stk with
-    | [] -> None
-    | f::_ -> Some f
-
-let restore_last_focus e =
-  match e.last_focused_stk with
-    | [] -> ()
-    | f::_ -> focus e f
-
-let focusedp e =
-  match e.focus with
-    | None -> false
-    | _    -> true
-
-let read e =
-  match e.focus with
-    | None -> None
-    | Some d ->
-	let (bs,c) = Hashtbl.find e.buf d in
-	Some(d,Bstack.top bs,c)
-
-let mutate e f =
-  match e.focus with
-    | None -> invalid_arg "Edit.mutate"
-    | Some d ->
-	let (bs,c) = Hashtbl.find e.buf d in
-	Bstack.app_push bs (f c)
-
-let rev_mutate e f =
-  match e.focus with
-    | None -> invalid_arg "Edit.rev_mutate"
-    | Some d ->
-	let (bs,c) = Hashtbl.find e.buf d in
-	Bstack.app_repl bs (f c)
-
-let undo e n =
-  match e.focus with
-    | None -> invalid_arg "Edit.undo"
-    | Some d ->
-	let (bs,_) = Hashtbl.find e.buf d in
-	if n >= Bstack.size bs then
-	  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
-	let ucnt = Bstack.depth bs - n in
-	if  ucnt >= Bstack.size bs then
-	  errorlabstrm "Edit.undo_todepth" (str"Undo stack would be exhausted");
-        repeat ucnt Bstack.pop bs
-
-let create e (d,b,c,usize) =
-  if Hashtbl.mem e.buf d then
-    errorlabstrm "Edit.create"
-      (str"Already editing something of that name");
-  let bs = Bstack.create usize b in
-  Hashtbl.add e.buf d (bs,c)
-
-let delete e d =
-  if not(Hashtbl.mem e.buf d) then
-    errorlabstrm "Edit.delete" (str"No such editor");
-  Hashtbl.remove e.buf d;
-  e.last_focused_stk <- (list_except d e.last_focused_stk);
-  match e.focus with
-    | Some d' -> if d = d' then (e.focus <- None ; (restore_last_focus e))
-    | None -> ()
-
-let dom e =
-  let l = ref [] in
-  Hashtbl.iter (fun x _ -> l := x :: !l) e.buf;
-  !l
-
-let clear e =
-  e.focus <- None;
-  e.last_focused_stk <- [];
-  Hashtbl.clear e.buf
diff --git a/lib/edit.mli b/lib/edit.mli
deleted file mode 100644
index d3558716..00000000
--- a/lib/edit.mli
+++ /dev/null
@@ -1,63 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: edit.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* The type of editors.
- * An editor is a finite map, ['a -> 'b], which knows how to apply
- * modification functions to the value in the range, and how to
- * focus on a member of the range.
- * It also supports the notion of a limited-depth undo, and that certain
- * modification actions do not push onto the undo stack, since they are
- * reversible. *)
-
-type ('a,'b,'c) t
-
-val empty : unit -> ('a,'b,'c) t
-
-(* sets the focus to the specified domain element *)
-val focus : ('a,'b,'c) t -> 'a -> unit
-
-(* unsets the focus which must not already be unfocused *)
-val unfocus : ('a,'b,'c) t -> unit
-
-(* gives the last focused element or [None] if none *)
-val last_focused : ('a,'b,'c) t -> 'a option
-
-(* are we focused ? *)
-val focusedp : ('a,'b,'c) t -> bool
-
-(* If we are focused, then return the current domain,range pair. *)
-val read : ('a,'b,'c) t -> ('a * 'b * 'c) option
-
-(* mutates the currently-focused range element, pushing its
- * old value onto the undo stack
- *)
-val mutate : ('a,'b,'c) t -> ('c -> 'b -> 'b) -> unit
-
-(* mutates the currently-focused range element, in place. *)
-val rev_mutate : ('a,'b,'c) t -> ('c -> 'b -> 'b) -> unit
-
-(* Pops the specified number of elements off of the undo stack, *
-  reinstating the last popped element. The undo stack is independently
-  managed for each range element. *)
-val undo : ('a,'b,'c) t -> int -> unit
-
-val create : ('a,'b,'c) t -> 'a * 'b * 'c * int -> unit
-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/envars.ml b/lib/envars.ml
index f764576d..c672d30c 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,39 +9,77 @@
 (* This file gathers environment variables needed by Coq to run (such
    as coqlib) *)
 
-let coqbin () =
-  if !Flags.boot || Coq_config.local
-  then Filename.concat Coq_config.coqsrc "bin"
-  else System.canonical_path_name (Filename.dirname Sys.executable_name)
+let coqbin =
+  System.canonical_path_name (Filename.dirname Sys.executable_name)
+
+(* The following only makes sense when executables are running from
+   source tree (e.g. during build or in local mode). *)
+let coqroot = Filename.dirname coqbin
 
 (* On win32, we add coqbin to the PATH at launch-time (this used to be
    done in a .bat script). *)
 
 let _ =
   if Coq_config.arch = "win32" then
-    Unix.putenv "PATH" (coqbin() ^ ";" ^ System.getenv_else "PATH" "")
+    Unix.putenv "PATH" (coqbin ^ ";" ^ System.getenv_else "PATH" "")
+
+let exe s = s ^ Coq_config.exec_extension
+
+let reldir instdir testfile oth =
+  let rpath = if Coq_config.local then [] else instdir in
+  let out = List.fold_left Filename.concat coqroot rpath in
+  if Sys.file_exists (Filename.concat out testfile) then out else oth ()
 
 let guess_coqlib () =
   let file = "states/initial.coq" in
-    if Sys.file_exists (Filename.concat Coq_config.coqlib file)
-    then Coq_config.coqlib
-    else
-      let coqbin = System.canonical_path_name (Filename.dirname Sys.executable_name) in
-      let prefix = Filename.dirname coqbin in
-      let rpath = if Coq_config.local then [] else
-	  (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
-      let coqlib = List.fold_left Filename.concat prefix rpath in
-	if Sys.file_exists (Filename.concat coqlib file) then coqlib else
-	  Util.error "cannot guess a path for Coq libraries; please use -coqlib option"
+    reldir (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) file
+      (fun () ->
+        let coqlib = match Coq_config.coqlib with
+          | Some coqlib -> coqlib
+          | None -> coqroot
+        in
+        if Sys.file_exists (Filename.concat coqlib file)
+        then coqlib
+        else Util.error "cannot guess a path for Coq libraries; please use -coqlib option")
 
 let coqlib () =
   if !Flags.coqlib_spec then !Flags.coqlib else
-    (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ())
+    (if !Flags.boot then coqroot else guess_coqlib ())
+
+let docdir () =
+  reldir (if Coq_config.arch = "win32" then ["doc"] else ["share";"doc";"coq"]) "html" (fun () -> Coq_config.docdir)
 
 let path_to_list p =
   let sep = if Sys.os_type = "Win32" then ';' else ':' in
     Util.split_string_at sep p
 
+let xdg_data_home =
+  Filename.concat
+    (System.getenv_else "XDG_DATA_HOME" (Filename.concat System.home ".local/share"))
+    "coq"
+
+let xdg_config_home =
+  Filename.concat
+    (System.getenv_else "XDG_CONFIG_HOME" (Filename.concat System.home ".config"))
+    "coq"
+
+let xdg_data_dirs =
+  (try
+    List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
+  with Not_found -> ["/usr/local/share/coq";"/usr/share/coq"])
+    @ (match Coq_config.datadir with |None -> [] |Some datadir -> [datadir])
+
+let xdg_dirs =
+  let dirs = xdg_data_home :: xdg_data_dirs
+  in
+  List.rev (List.filter Sys.file_exists dirs)
+
+let coqpath =
+  try
+    let path = Sys.getenv "COQPATH" in
+      List.rev (List.filter Sys.file_exists (path_to_list path))
+  with Not_found -> []
+
 let rec which l f =
   match l with
     | [] -> raise Not_found
@@ -51,19 +89,19 @@ let rec which l f =
 	else which tl f
 
 let guess_camlbin () =
-  let path = try Sys.getenv "PATH" with _ -> raise Not_found in
+  let path = Sys.getenv "PATH" in (* may raise Not_found *)
   let lpath = path_to_list path in
-    which lpath "ocamlc"
+    which lpath (exe "ocamlc")
 
 let guess_camlp4bin () =
-  let path = try Sys.getenv "PATH" with _ -> raise Not_found in
+  let path = Sys.getenv "PATH" in (* may raise Not_found *)
   let lpath = path_to_list path in
-    which lpath Coq_config.camlp4
+    which lpath (exe Coq_config.camlp4)
 
 let camlbin () =
   if !Flags.camlbin_spec then !Flags.camlbin else
     if !Flags.boot then Coq_config.camlbin else
-      try guess_camlbin () with _ -> Coq_config.camlbin
+      try guess_camlbin () with e when e <> Sys.Break -> Coq_config.camlbin
 
 let camllib () =
   if !Flags.boot
@@ -74,11 +112,13 @@ let camllib () =
     let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in
     Util.strip res
 
-(* TODO : essayer aussi camlbin *)
 let camlp4bin () =
   if !Flags.camlp4bin_spec then !Flags.camlp4bin else
     if !Flags.boot then Coq_config.camlp4bin else
-      try guess_camlp4bin () with _ -> Coq_config.camlp4bin
+      try guess_camlp4bin () with e when e <> Sys.Break ->
+        let cb = camlbin () in
+	if Sys.file_exists (Filename.concat cb (exe Coq_config.camlp4)) then cb
+	else Coq_config.camlp4bin
 
 let camlp4lib () =
   if !Flags.boot
@@ -86,7 +126,7 @@ let camlp4lib () =
   else
     let camlp4bin = camlp4bin () in
     let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in
-    let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in
-    Util.strip res
-
-
+    let ex,res = System.run_command (fun x -> x) (fun _ -> ()) com in
+    match ex with
+      |Unix.WEXITED 0 -> Util.strip res
+      |_ -> "/dev/null"
diff --git a/lib/envars.mli b/lib/envars.mli
index 05357b32..9ec170db 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -1,13 +1,23 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** This file gathers environment variables needed by Coq to run (such
+   as coqlib) *)
+
 val coqlib : unit -> string
-val coqbin : unit -> string
+val docdir : unit -> string
+val coqbin : string
+val coqroot : string
+(* coqpath is stored in reverse order, since that is the order it
+ * gets added to the searc path *)
+val xdg_config_home : string
+val xdg_dirs : string list
+val coqpath : string list
 
 val camlbin : unit -> string
 val camlp4bin : unit -> string
diff --git a/lib/errors.ml b/lib/errors.ml
new file mode 100644
index 00000000..6affea23
--- /dev/null
+++ b/lib/errors.ml
@@ -0,0 +1,79 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+open Pp
+
+(* spiwack: it might be reasonable to decide and move the declarations
+   of Anomaly and so on to this module so as not to depend on Util. *)
+
+let handle_stack = ref []
+
+exception Unhandled
+
+let register_handler h = handle_stack := h::!handle_stack
+
+(** [print_gen] is a general exception printer which tries successively
+    all the handlers of a list, and finally a [bottom] handler if all
+    others have failed *)
+
+let rec print_gen bottom stk e =
+  match stk with
+  | [] -> bottom e
+  | h::stk' ->
+    try h e
+    with
+    | Unhandled -> print_gen bottom stk' e
+    | any -> print_gen bottom stk' any
+
+(** Only anomalies should reach the bottom of the handler stack.
+    In usual situation, the [handle_stack] is treated as it if was always
+    non-empty with [print_anomaly] as its bottom handler. *)
+
+let where s =
+  if !Flags.debug then str ("in "^s^":") ++ spc () else mt ()
+
+let raw_anomaly e = match e with
+  | Util.Anomaly (s,pps) -> where s ++ pps ++ str "."
+  | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".")
+  | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".")
+
+let print_anomaly askreport e =
+  if askreport then
+    hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.")
+  else
+    hov 0 (raw_anomaly e)
+
+(** The standard exception printer *)
+let print e = print_gen (print_anomaly true) !handle_stack e
+
+(** Same as [print], except that the "Please report" part of an anomaly
+    isn't printed (used in Ltac debugging). *)
+let print_no_report e = print_gen (print_anomaly false) !handle_stack e
+
+(** Same as [print], except that anomalies are not printed but re-raised
+    (used for the Fail command) *)
+let print_no_anomaly e = print_gen (fun e -> raise e) !handle_stack e
+
+(** Predefined handlers **)
+
+let _ = register_handler begin function
+  | Util.UserError(s,pps) -> hov 0 (str "Error: " ++ where s ++ pps)
+  | _ -> raise Unhandled
+end
+
+(** Critical exceptions shouldn't be catched and ignored by mistake
+    by inner functions during a [vernacinterp]. They should be handled
+    only at the very end of interp, to be displayed to the user. *)
+
+(** NB: in the 8.4 branch, for maximal compatibility, anomalies
+    are considered non-critical *)
+
+let noncritical = function
+  | Sys.Break | Out_of_memory | Stack_overflow -> false
+  | _ -> true
+
diff --git a/lib/errors.mli b/lib/errors.mli
new file mode 100644
index 00000000..ae4d0b85
--- /dev/null
+++ b/lib/errors.mli
@@ -0,0 +1,49 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(** This modules implements basic manipulations of errors for use
+    throughout Coq's code. *)
+
+(** [register_handler h] registers [h] as a handler.
+    When an expression is printed with [print e], it
+    goes through all registered handles (the most
+    recent first) until a handle deals with it.
+
+    Handles signal that they don't deal with some exception
+    by raising [Unhandled].
+
+    Handles can raise exceptions themselves, in which
+    case, the exception is passed to the handles which
+    were registered before.
+
+    The exception that are considered anomalies should not be
+    handled by registered handlers.
+*)
+
+exception Unhandled
+
+val register_handler : (exn -> Pp.std_ppcmds) -> unit
+
+(** The standard exception printer *)
+val print : exn -> Pp.std_ppcmds
+
+(** Same as [print], except that the "Please report" part of an anomaly
+    isn't printed (used in Ltac debugging). *)
+val print_no_report : exn -> Pp.std_ppcmds
+
+(** Same as [print], except that anomalies are not printed but re-raised
+    (used for the Fail command) *)
+val print_no_anomaly : exn -> Pp.std_ppcmds
+
+(** Critical exceptions shouldn't be catched and ignored by mistake
+    by inner functions during a [vernacinterp]. They should be handled
+    only in [Toplevel.do_vernac] (or Ideslave), to be displayed to the user.
+    Typical example: [Sys.Break]. In the 8.4 branch, for maximal
+    compatibility, anomalies are not considered as critical...
+*)
+val noncritical : exn -> bool
diff --git a/lib/explore.ml b/lib/explore.ml
index c40362c8..1c8776a4 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: explore.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-open Format
+open Pp
 
 (*s Definition of a search problem. *)
 
@@ -16,20 +14,20 @@ module type SearchProblem = sig
   type state
   val branching : state -> state list
   val success : state -> bool
-  val pp : state -> unit
+  val pp : state -> std_ppcmds
 end
 
 module Make = functor(S : SearchProblem) -> struct
 
   type position = int list
 
-  let pp_position p =
+  let msg_with_position p pp =
     let rec pp_rec = function
-      | [] -> ()
-      | [i] -> printf "%d" i
-      | i :: l -> pp_rec l; printf ".%d" i
+      | [] -> mt ()
+      | [i] -> int i
+      | i :: l -> pp_rec l ++ str "." ++ int i
     in
-    open_hbox (); pp_rec p; close_box ()
+    msg_debug (h 0 (pp_rec p) ++ pp)
 
   (*s Depth first search. *)
 
@@ -42,7 +40,7 @@ module Make = functor(S : SearchProblem) -> struct
 
   let debug_depth_first s =
     let rec explore p s =
-      pp_position p; S.pp s;
+      msg_with_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
@@ -85,7 +83,7 @@ module Make = functor(S : SearchProblem) -> struct
 	  explore q
       | s :: l ->
 	  let ps = i::p in
-	  pp_position ps; S.pp s;
+	  msg_with_position ps (S.pp s);
 	  if S.success s then s else enqueue (succ i) p (push (ps,s) q) l
     in
     enqueue 1 [] empty [s]
diff --git a/lib/explore.mli b/lib/explore.mli
index e01f851c..7190d5e3 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -1,16 +1,15 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: explore.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** {6 Search strategies. } *)
 
-(*s Search strategies. *)
-
-(*s A search problem implements the following signature [SearchProblem].
+(** {6 ... } *)
+(** A search problem implements the following signature [SearchProblem].
     [state] is the type of states of the search tree.
     [branching] is the branching function; if [branching s] returns an
     empty list, then search from [s] is aborted; successors of [s] are
@@ -28,11 +27,12 @@ module type SearchProblem = sig
 
   val success : state -> bool
 
-  val pp : state -> unit
+  val pp : state -> Pp.std_ppcmds
 
 end
 
-(*s Functor [Make] returns some search functions given a search problem.
+(** {6 ... } *)
+(** Functor [Make] returns some search functions given a search problem.
     Search functions raise [Not_found] if no success is found.
     States are always visited in the order they appear in the
     output of [branching] (whatever the search method is).
diff --git a/lib/flags.ml b/lib/flags.ml
index 6b68a8f2..32c68b25 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -1,22 +1,20 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: flags.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 let with_option o f x =
   let old = !o in o:=true;
   try let r = f x in o := old; r
-  with e -> o := old; raise e
+  with reraise -> o := old; raise reraise
 
 let without_option o f x =
   let old = !o in o:=false;
   try let r = f x in o := old; r
-  with e -> o := old; raise e
+  with reraise -> o := old; raise reraise
 
 let boot = ref false
 
@@ -25,24 +23,34 @@ let batch_mode = ref false
 let debug = ref false
 
 let print_emacs = ref false
-let print_emacs_safechar = ref false
 
 let term_quality = ref false
 
 let xml_export = ref false
 
-let dont_load_proofs = ref false
+type load_proofs = Force | Lazy | Dont
+
+let load_proofs = ref Lazy
 
 let raw_print = ref false
 
+let record_print = ref true
+
 (* Compatibility mode *)
 
-type compat_version = V8_2
-let compat_version = ref None
-let version_strictly_greater v =
-  match !compat_version with None -> true | Some v' -> v'>v
+(* Current means no particular compatibility consideration.
+   For correct comparisons, this constructor should remain the last one. *)
+
+type compat_version = V8_2 | V8_3 | Current
+let compat_version = ref Current
+let version_strictly_greater v = !compat_version > v
 let version_less_or_equal v = not (version_strictly_greater v)
 
+let pr_version = function
+  | V8_2 -> "8.2"
+  | V8_3 -> "8.3"
+  | Current -> "current"
+
 (* Translate *)
 let beautify = ref false
 let make_beautify f = beautify := f
@@ -86,12 +94,6 @@ let unsafe_set = ref Stringset.empty
 let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
 let is_unsafe s = Stringset.mem s !unsafe_set
 
-(* Flags for the virtual machine *)
-
-let boxed_definitions = ref true
-let set_boxed_definitions b = boxed_definitions := b
-let boxed_definitions _ = !boxed_definitions
-
 (* Flags for external tools *)
 
 let subst_command_placeholder s t =
@@ -120,9 +122,21 @@ let is_standard_doc_url url =
   url = Coq_config.wwwrefman ||
   url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
 
+(* same as in System, but copied here because of dependencies *)
+let canonical_path_name p =
+  let current = Sys.getcwd () in
+  Sys.chdir p;
+  let result = Sys.getcwd () in
+  Sys.chdir current;
+  result
+
 (* Options for changing coqlib *)
 let coqlib_spec = ref false
-let coqlib = ref Coq_config.coqlib
+let coqlib = ref (
+  (* same as Envars.coqroot, but copied here because of dependencies *)
+  Filename.dirname
+    (canonical_path_name (Filename.dirname Sys.executable_name))
+)
 
 (* Options for changing camlbin (used by coqmktop) *)
 let camlbin_spec = ref false
@@ -132,3 +146,9 @@ let camlbin = ref Coq_config.camlbin
 let camlp4bin_spec = ref false
 let camlp4bin = ref Coq_config.camlp4bin
 
+(* Level of inlining during a functor application *)
+
+let default_inline_level = 100
+let inline_level = ref default_inline_level
+let set_inline_level = (:=) inline_level
+let get_inline_level () = !inline_level
diff --git a/lib/flags.mli b/lib/flags.mli
index f4325ce2..eb53f1a2 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: flags.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Global options of the system. *)
+(** Global options of the system. *)
 
 val boot : bool ref
 
@@ -17,20 +15,22 @@ val batch_mode : bool ref
 val debug : bool ref
 
 val print_emacs : bool ref
-val print_emacs_safechar : bool ref
 
 val term_quality : bool ref
 
 val xml_export : bool ref
 
-val dont_load_proofs : bool ref
+type load_proofs = Force | Lazy | Dont
+val load_proofs : load_proofs ref
 
 val raw_print : bool ref
+val record_print : bool ref
 
-type compat_version = V8_2
-val compat_version : compat_version option ref
+type compat_version = V8_2 | V8_3 | Current
+val compat_version : compat_version ref
 val version_strictly_greater : compat_version -> bool
 val version_less_or_equal : compat_version -> bool
+val pr_version : compat_version -> string
 
 val beautify : bool ref
 val make_beautify : bool -> unit
@@ -53,41 +53,41 @@ val if_warn : ('a -> unit) -> 'a -> unit
 
 val hash_cons_proofs : bool ref
 
-(* Temporary activate an option (to activate option [o] on [f x y z],
+(** Temporary activate an option (to activate option [o] on [f x y z],
    use [with_option o (f x y) z]) *)
 val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 
-(* Temporary deactivate an option *)
+(** Temporary deactivate an option *)
 val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 
-(* If [None], no limit *)
+(** If [None], no limit *)
 val set_print_hyps_limit : int option -> unit
 val print_hyps_limit : unit -> int option
 
 val add_unsafe : string -> unit
 val is_unsafe : string -> bool
 
-(* Options for the virtual machine *)
-
-val set_boxed_definitions : bool -> unit
-val boxed_definitions : unit -> bool
+(** Options for external tools *)
 
-(* Options for external tools *)
-
-(* Returns string format for default browser to use from Coq or CoqIDE *)
+(** Returns string format for default browser to use from Coq or CoqIDE *)
 val browser_cmd_fmt : string
 
 val is_standard_doc_url : string -> bool
 
-(* Substitute %s in the first chain by the second chain *)
+(** Substitute %s in the first chain by the second chain *)
 val subst_command_placeholder : string -> string -> string
 
-(* Options for specifying where coq librairies reside *)
+(** Options for specifying where coq librairies reside *)
 val coqlib_spec : bool ref
 val coqlib : string ref
 
-(* Options for specifying where OCaml binaries reside *)
+(** Options for specifying where OCaml binaries reside *)
 val camlbin_spec : bool ref
 val camlbin : string ref
 val camlp4bin_spec : bool ref
 val camlp4bin : string ref
+
+(** Level of inlining during a functor application *)
+val set_inline_level : int -> unit
+val get_inline_level : unit -> int
+val default_inline_level : int
diff --git a/lib/fmap.mli b/lib/fmap.mli
index c323b055..2c8dedd7 100644
--- a/lib/fmap.mli
+++ b/lib/fmap.mli
@@ -14,7 +14,7 @@ val iter : (key -> 'a -> unit) -> 'a t -> unit
 val map : ('a -> 'b) -> 'a t -> 'b t
 val fold : (key -> 'a -> 'c -> 'c) -> 'a t -> 'c -> 'c
 
-(* Additions with respect to ocaml standard library. *)
+(** Additions with respect to ocaml standard library. *)
 
 val dom : 'a t -> key list
 val rng : 'a t -> 'a list
diff --git a/lib/gmap.ml b/lib/gmap.ml
index 3f979074..08c99daf 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.ml
@@ -1,11 +1,10 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: gmap.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (* Maps using the generic comparison function of ocaml. Code borrowed from
    the ocaml standard library (Copyright 1996, INRIA). *)
diff --git a/lib/gmap.mli b/lib/gmap.mli
index 6da223d5..06fbd638 100644
--- a/lib/gmap.mli
+++ b/lib/gmap.mli
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: gmap.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Maps using the generic comparison function of ocaml. Same interface as
+(** Maps using the generic comparison function of ocaml. Same interface as
    the module [Map] from the ocaml standard library. *)
 
 type ('a,'b) t
@@ -23,7 +21,7 @@ val iter : ('a -> 'b -> unit) -> ('a,'b) t -> unit
 val map : ('b -> 'c) -> ('a,'b) t -> ('a,'c) t
 val fold : ('a -> 'b -> 'c -> 'c) -> ('a,'b) t -> 'c -> 'c
 
-(* Additions with respect to ocaml standard library. *)
+(** Additions with respect to ocaml standard library. *)
 
 val dom : ('a,'b) t -> 'a list
 val rng : ('a,'b) t -> 'b list
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
index e8dc6295..8c61d6eb 100644
--- a/lib/gmapl.ml
+++ b/lib/gmapl.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: gmapl.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 
 type ('a,'b) t = ('a,'b list) Gmap.t
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
index f60aed5d..5e772088 100644
--- a/lib/gmapl.mli
+++ b/lib/gmapl.mli
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: gmapl.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Maps from ['a] to lists of ['b]. *)
+(** Maps from ['a] to lists of ['b]. *)
 
 type ('a,'b) t
 
diff --git a/lib/gset.ml b/lib/gset.ml
deleted file mode 100644
index 28b769af..00000000
--- a/lib/gset.ml
+++ /dev/null
@@ -1,242 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: gset.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-(* Sets using the generic comparison function of ocaml. Code borrowed from
-   the ocaml standard library. *)
-
-    type 'a t = Empty | Node of 'a t * 'a * 'a t * int
-
-    (* Sets are represented by balanced binary trees (the heights of the
-       children differ by at most 2 *)
-
-    let height = function
-        Empty -> 0
-      | Node(_, _, _, h) -> h
-
-    (* Creates a new node with left son l, value x and right son r.
-       l and r must be balanced and | height l - height r | <= 2.
-       Inline expansion of height for better speed. *)
-
-    let create l x r =
-      let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
-      let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
-      Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1))
-
-    (* Same as create, but performs one step of rebalancing if necessary.
-       Assumes l and r balanced.
-       Inline expansion of create for better speed in the most frequent case
-       where no rebalancing is required. *)
-
-    let bal l x r =
-      let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
-      let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
-      if hl > hr + 2 then begin
-        match l with
-          Empty -> invalid_arg "Set.bal"
-        | Node(ll, lv, lr, _) ->
-            if height ll >= height lr then
-              create ll lv (create lr x r)
-            else begin
-              match lr with
-                Empty -> invalid_arg "Set.bal"
-              | Node(lrl, lrv, lrr, _)->
-                  create (create ll lv lrl) lrv (create lrr x r)
-            end
-      end else if hr > hl + 2 then begin
-        match r with
-          Empty -> invalid_arg "Set.bal"
-        | Node(rl, rv, rr, _) ->
-            if height rr >= height rl then
-              create (create l x rl) rv rr
-            else begin
-              match rl with
-                Empty -> invalid_arg "Set.bal"
-              | Node(rll, rlv, rlr, _) ->
-                  create (create l x rll) rlv (create rlr rv rr)
-            end
-      end else
-        Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1))
-
-    (* Same as bal, but repeat rebalancing until the final result
-       is balanced. *)
-
-    let rec join l x r =
-      match bal l x r with
-        Empty -> invalid_arg "Set.join"
-      | Node(l', x', r', _) as t' ->
-          let d = height l' - height r' in
-          if d < -2 or d > 2 then join l' x' r' else t'
-
-    (* Merge two trees l and r into one.
-       All elements of l must precede the elements of r.
-       Assumes | height l - height r | <= 2. *)
-
-    let rec merge t1 t2 =
-      match (t1, t2) with
-        (Empty, t) -> t
-      | (t, Empty) -> t
-      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
-          bal l1 v1 (bal (merge r1 l2) v2 r2)
-
-    (* Same as merge, but does not assume anything about l and r. *)
-
-    let rec concat t1 t2 =
-      match (t1, t2) with
-        (Empty, t) -> t
-      | (t, Empty) -> t
-      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
-          join l1 v1 (join (concat r1 l2) v2 r2)
-
-    (* Splitting *)
-
-    let rec split x = function
-        Empty ->
-          (Empty, None, Empty)
-      | Node(l, v, r, _) ->
-          let c = Pervasives.compare x v in
-          if c = 0 then (l, Some v, r)
-          else if c < 0 then
-            let (ll, vl, rl) = split x l in (ll, vl, join rl v r)
-          else
-            let (lr, vr, rr) = split x r in (join l v lr, vr, rr)
-
-    (* Implementation of the set operations *)
-
-    let empty = Empty
-
-    let is_empty = function Empty -> true | _ -> false
-
-    let rec mem x = function
-        Empty -> false
-      | Node(l, v, r, _) ->
-          let c = Pervasives.compare x v in
-          c = 0 || mem x (if c < 0 then l else r)
-
-    let rec add x = function
-        Empty -> Node(Empty, x, Empty, 1)
-      | Node(l, v, r, _) as t ->
-          let c = Pervasives.compare x v in
-          if c = 0 then t else
-          if c < 0 then bal (add x l) v r else bal l v (add x r)
-
-    let singleton x = Node(Empty, x, Empty, 1)
-
-    let rec remove x = function
-        Empty -> Empty
-      | Node(l, v, r, _) ->
-          let c = Pervasives.compare x v in
-          if c = 0 then merge l r else
-          if c < 0 then bal (remove x l) v r else bal l v (remove x r)
-
-    let rec union s1 s2 =
-      match (s1, s2) with
-        (Empty, t2) -> t2
-      | (t1, Empty) -> t1
-      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
-          if h1 >= h2 then
-            if h2 = 1 then add v2 s1 else begin
-              let (l2, _, r2) = split v1 s2 in
-              join (union l1 l2) v1 (union r1 r2)
-            end
-          else
-            if h1 = 1 then add v1 s2 else begin
-              let (l1, _, r1) = split v2 s1 in
-              join (union l1 l2) v2 (union r1 r2)
-            end
-
-    let rec inter s1 s2 =
-      match (s1, s2) with
-        (Empty, t2) -> Empty
-      | (t1, Empty) -> Empty
-      | (Node(l1, v1, r1, _), t2) ->
-          match split v1 t2 with
-            (l2, None, r2) ->
-              concat (inter l1 l2) (inter r1 r2)
-          | (l2, Some _, r2) ->
-              join (inter l1 l2) v1 (inter r1 r2)
-
-    let rec diff s1 s2 =
-      match (s1, s2) with
-        (Empty, t2) -> Empty
-      | (t1, Empty) -> t1
-      | (Node(l1, v1, r1, _), t2) ->
-          match split v1 t2 with
-            (l2, None, r2) ->
-              join (diff l1 l2) v1 (diff r1 r2)
-          | (l2, Some _, r2) ->
-              concat (diff l1 l2) (diff r1 r2)
-
-    let rec compare_aux l1 l2 =
-        match (l1, l2) with
-        ([], []) -> 0
-      | ([], _)  -> -1
-      | (_, []) -> 1
-      | (Empty :: t1, Empty :: t2) ->
-          compare_aux t1 t2
-      | (Node(Empty, v1, r1, _) :: t1, Node(Empty, v2, r2, _) :: t2) ->
-          let c = compare v1 v2 in
-          if c <> 0 then c else compare_aux (r1::t1) (r2::t2)
-      | (Node(l1, v1, r1, _) :: t1, t2) ->
-          compare_aux (l1 :: Node(Empty, v1, r1, 0) :: t1) t2
-      | (t1, Node(l2, v2, r2, _) :: t2) ->
-          compare_aux t1 (l2 :: Node(Empty, v2, r2, 0) :: t2)
-
-    let compare s1 s2 =
-      compare_aux [s1] [s2]
-
-    let equal s1 s2 =
-      compare s1 s2 = 0
-
-    let rec subset s1 s2 =
-      match (s1, s2) with
-        Empty, _ ->
-          true
-      | _, Empty ->
-          false
-      | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) ->
-          let c = Pervasives.compare v1 v2 in
-          if c = 0 then
-            subset l1 l2 && subset r1 r2
-          else if c < 0 then
-            subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2
-          else
-            subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2
-
-    let rec iter f = function
-        Empty -> ()
-      | Node(l, v, r, _) -> iter f l; f v; iter f r
-
-    let rec fold f s accu =
-      match s with
-        Empty -> accu
-      | Node(l, v, r, _) -> fold f l (f v (fold f r accu))
-
-    let rec cardinal = function
-        Empty -> 0
-      | Node(l, v, r, _) -> cardinal l + 1 + cardinal r
-
-    let rec elements_aux accu = function
-        Empty -> accu
-      | Node(l, v, r, _) -> elements_aux (v :: elements_aux accu r) l
-
-    let elements s =
-      elements_aux [] s
-
-    let rec min_elt = function
-        Empty -> raise Not_found
-      | Node(Empty, v, r, _) -> v
-      | Node(l, v, r, _) -> min_elt l
-
-    let rec max_elt = function
-        Empty -> raise Not_found
-      | Node(l, v, Empty, _) -> v
-      | Node(l, v, r, _) -> max_elt r
-
-    let choose = min_elt
diff --git a/lib/gset.mli b/lib/gset.mli
deleted file mode 100644
index 25e607f7..00000000
--- a/lib/gset.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: gset.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Sets using the generic comparison function of ocaml. Same interface as
-   the module [Set] from the ocaml standard library. *)
-
-type 'a t
-
-val empty : 'a t
-val is_empty : 'a t -> bool
-val mem : 'a -> 'a t -> bool
-val add : 'a -> 'a t -> 'a t
-val singleton : 'a -> 'a t
-val remove : 'a -> 'a t -> 'a t
-val union : 'a t -> 'a t -> 'a t
-val inter : 'a t -> 'a t -> 'a t
-val diff : 'a t -> 'a t -> 'a t
-val compare : 'a t -> 'a t -> int
-val equal : 'a t -> 'a t -> bool
-val subset : 'a t -> 'a t -> bool
-val iter : ('a -> unit) -> 'a t -> unit
-val fold : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-val cardinal : 'a t -> int
-val elements : 'a t -> 'a list
-val min_elt : 'a t -> 'a
-val max_elt : 'a t -> 'a
-val choose : 'a t -> 'a
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 542ecde9..5f4738dc 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: hashcons.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* Hash consing of datastructures *)
 
 (* The generic hash-consing functions (does not use Obj) *)
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 81c74aef..b4a9da2f 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: hashcons.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Generic hash-consing. *)
+(** Generic hash-consing. *)
 
 module type Comp =
   sig
@@ -37,7 +35,7 @@ val recursive2_hcons :
     (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u2 -> 't2 -> 't2) ->
       'u1 -> 'u2 -> ('t1 -> 't1) * ('t2 -> 't2)
 
-(* Declaring and reinitializing global hash-consing functions *)
+(** Declaring and reinitializing global hash-consing functions *)
 
 val init : unit -> unit
 val register_hcons : ('u -> 't -> 't) -> ('u -> 't -> 't)
diff --git a/lib/hashtbl_alt.ml b/lib/hashtbl_alt.ml
new file mode 100644
index 00000000..bb2252da
--- /dev/null
+++ b/lib/hashtbl_alt.ml
@@ -0,0 +1,109 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* The following module is a specialized version of [Hashtbl] that is
+   a better space saver. Actually, [Hashcons] instanciates [Hashtbl.t]
+   with [constr] used both as a key and as an image.  Thus, in each
+   cell of the internal bucketlist, there are two representations of
+   the same value. In this implementation, there is only one.
+
+   Besides, the responsibility of computing the hash function is now
+   given to the caller, which makes possible the interleaving of the
+   hash key computation and the hash-consing. *)
+
+module type Hashtype = sig
+  type t
+  val equals : t -> t -> bool
+end
+
+module type S = sig
+  type elt
+  (* [may_add_and_get key constr] uses [key] to look for [constr]
+     in the hash table [H]. If [constr] is in [H], returns the
+     specific representation that is stored in [H]. Otherwise,
+     [constr] is stored in [H] and will be used as the canonical
+     representation of this value in the future. *)
+  val may_add_and_get : int -> elt -> elt
+end
+
+module Make (E : Hashtype) =
+  struct
+
+    type elt = E.t
+
+    type bucketlist = Empty | Cons of elt * int * bucketlist
+
+    let initial_size = 19991
+    let table_data = ref (Array.make initial_size Empty)
+    let table_size = ref 0
+
+    let resize () =
+      let odata = !table_data in
+      let osize = Array.length odata in
+    let nsize = min (2 * osize + 1) Sys.max_array_length in
+    if nsize <> osize then begin
+      let ndata = Array.create nsize Empty in
+      let rec insert_bucket = function
+	| Empty -> ()
+	| Cons (key, hash, rest) ->
+          let nidx = hash mod nsize in
+          ndata.(nidx) <- Cons (key, hash, ndata.(nidx));
+          insert_bucket rest
+      in
+      for i = 0 to osize - 1 do insert_bucket odata.(i) done;
+      table_data := ndata
+    end
+
+  let add hash key =
+    let odata = !table_data in
+    let osize = Array.length odata in
+    let i = hash mod osize in
+    odata.(i) <- Cons (key, hash, odata.(i));
+    incr table_size;
+    if !table_size > osize lsl 1 then resize ()
+
+  let find_rec hash key bucket =
+    let rec aux = function
+      | Empty ->
+	add hash key; key
+      | Cons (k, h, rest) ->
+	if hash == h && E.equals key k then k else aux rest
+    in
+    aux bucket
+
+  let may_add_and_get hash key =
+    let odata = !table_data in
+    match odata.(hash mod (Array.length odata)) with
+      |	Empty -> add hash key; key
+      | Cons (k1, h1, rest1) ->
+	if hash == h1 && E.equals key k1 then k1 else
+	  match rest1 with
+            | Empty -> add hash key; key
+	    | Cons (k2, h2, rest2) ->
+              if hash == h2 && E.equals key k2 then k2 else
+		match rest2 with
+		  | Empty -> add hash key; key
+		  | Cons (k3, h3, rest3) ->
+		    if hash == h3 && E.equals key k3 then k3
+		    else find_rec hash key rest3
+
+end
+
+module Combine = struct
+    (* These are helper functions to combine the hash keys in a similar
+       way as [Hashtbl.hash] does. The constants [alpha] and [beta] must
+       be prime numbers. There were chosen empirically. Notice that the
+       problem of hashing trees is hard and there are plenty of study on
+       this topic. Therefore, there must be room for improvement here. *)
+    let alpha = 65599
+    let beta  = 7
+    let combine x y     = x * alpha + y
+    let combine3 x y z   = combine x (combine y z)
+    let combine4 x y z t = combine x (combine3 y z t)
+    let combinesmall x y = beta * x + y
+end
diff --git a/lib/hashtbl_alt.mli b/lib/hashtbl_alt.mli
new file mode 100644
index 00000000..7a1dcd57
--- /dev/null
+++ b/lib/hashtbl_alt.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* The following module is a specialized version of [Hashtbl] that is
+   a better space saver. Actually, [Hashcons] instanciates [Hashtbl.t]
+   with [constr] used both as a key and as an image.  Thus, in each
+   cell of the internal bucketlist, there are two representations of
+   the same value. In this implementation, there is only one.
+
+   Besides, the responsibility of computing the hash function is now
+   given to the caller, which makes possible the interleaving of the
+   hash key computation and the hash-consing. *)
+
+module type Hashtype = sig
+  type t
+  val equals : t -> t -> bool
+end
+
+module type S = sig
+  type elt
+  (* [may_add_and_get key constr] uses [key] to look for [constr]
+     in the hash table [H]. If [constr] is in [H], returns the
+     specific representation that is stored in [H]. Otherwise,
+     [constr] is stored in [H] and will be used as the canonical
+     representation of this value in the future. *)
+  val may_add_and_get : int -> elt -> elt
+end
+
+module Make (E : Hashtype) : S with type elt = E.t
+
+module Combine : sig
+  val combine : int -> int -> int
+  val combinesmall : int -> int -> int
+  val combine3 : int -> int -> int -> int
+  val combine4 : int -> int -> int -> int -> int
+end
diff --git a/lib/heap.ml b/lib/heap.ml
index c61bccb9..4f0a65a6 100644
--- a/lib/heap.ml
+++ b/lib/heap.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: heap.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (*s Heaps *)
 
 module type Ordered = sig
diff --git a/lib/heap.mli b/lib/heap.mli
index 3183e0ec..c2bd95ae 100644
--- a/lib/heap.mli
+++ b/lib/heap.mli
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: heap.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Heaps *)
+(** Heaps *)
 
 module type Ordered = sig
   type t
@@ -17,29 +15,29 @@ end
 
 module type S =sig
 
-  (* Type of functional heaps *)
+  (** Type of functional heaps *)
   type t
 
-  (* Type of elements *)
+  (** Type of elements *)
   type elt
 
-  (* The empty heap *)
+  (** The empty heap *)
   val empty : t
 
-  (* [add x h] returns a new heap containing the elements of [h], plus [x];
-     complexity $O(log(n))$ *)
+  (** [add x h] returns a new heap containing the elements of [h], plus [x];
+     complexity {% $ %}O(log(n)){% $ %} *)
   val add : elt -> t -> t
 
-  (* [maximum h] returns the maximum element of [h]; raises [EmptyHeap]
-     when [h] is empty; complexity $O(1)$ *)
+  (** [maximum h] returns the maximum element of [h]; raises [EmptyHeap]
+     when [h] is empty; complexity {% $ %}O(1){% $ %} *)
   val maximum : t -> elt
 
-  (* [remove h] returns a new heap containing the elements of [h], except
+  (** [remove h] returns a new heap containing the elements of [h], except
      the maximum of [h]; raises [EmptyHeap] when [h] is empty;
-     complexity $O(log(n))$ *)
+     complexity {% $ %}O(log(n)){% $ %} *)
   val remove : t -> t
 
-  (* usual iterators and combinators; elements are presented in
+  (** usual iterators and combinators; elements are presented in
      arbitrary order *)
   val iter : (elt -> unit) -> t -> unit
 
@@ -49,6 +47,6 @@ end
 
 exception EmptyHeap
 
-(*S Functional implementation. *)
+(** {6 Functional implementation. } *)
 
 module Functional(X: Ordered) : S with type elt=X.t
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 1743ce26..db79b5c2 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,3 +1,6 @@
+Xml_lexer
+Xml_parser
+Xml_utils
 Pp_control
 Pp
 Compat
@@ -5,19 +8,16 @@ Flags
 Segmenttree
 Unicodetable
 Util
+Errors
 Bigint
 Hashcons
 Dyn
 System
 Envars
-Bstack
-Edit
-Gset
 Gmap
 Fset
 Fmap
-Tlm
-tries
+Tries
 Gmapl
 Profile
 Explore
@@ -26,4 +26,6 @@ Rtree
 Heap
 Option
 Dnet
-
+Store
+Unionfind
+Hashtbl_alt
diff --git a/lib/option.ml b/lib/option.ml
index f4b1604f..0500becc 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: option.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Module implementing basic combinators for OCaml option type.
    It tries follow closely the style of OCaml standard library.
 
diff --git a/lib/option.mli b/lib/option.mli
index 1dc721fe..f8aeecc5 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: option.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (** Module implementing basic combinators for OCaml option type.
    It tries follow closely the style of OCaml standard library.
 
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index d02b5c4d..569a028f 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pp.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Pp_control
 
 (* This should not be used outside of this file. Use
@@ -160,6 +158,17 @@ let tclose () = [< 'Ppcmd_close_tbox >]
 
 let (++) = Stream.iapp
 
+let rec eval_ppcmds l =
+  let rec aux l =
+    try
+      let a = match Stream.next l with
+      | Ppcmd_box (b,s) -> Ppcmd_box (b,eval_ppcmds s)
+      | a -> a in
+      let rest = aux l in
+      a :: rest
+    with Stream.Failure -> [] in
+  Stream.of_list (aux l)
+
 (* In new syntax only double quote char is escaped by repeating it *)
 let rec escape_string s =
   let rec escape_at s i =
@@ -270,28 +279,21 @@ let pp_dirs ft =
     try
       Stream.iter pp_dir dirstream; com_brk ft
     with
-      | e -> Format.pp_print_flush ft () ; raise e
+      | reraise -> Format.pp_print_flush ft () ; raise reraise
 
 
 (* pretty print on stdout and stderr *)
 
-let pp_std_dirs = pp_dirs !std_ft
-let pp_err_dirs = pp_dirs !err_ft
-
-let ppcmds x = Ppdir_ppcmds x
-
 (* Special chars for emacs, to detect warnings inside goal output *)
-let emacs_warning_start_string = String.make 1 (Char.chr 254)
-let emacs_warning_end_string = String.make 1 (Char.chr 255)
-
-let warnstart() =
-  if not !print_emacs then mt() else str emacs_warning_start_string
+let emacs_quote_start = String.make 1 (Char.chr 254)
+let emacs_quote_end = String.make 1 (Char.chr 255)
 
-let warnend() =
-  if not !print_emacs then mt() else str emacs_warning_end_string
+let emacs_quote strm =
+  if !print_emacs then
+    [< str emacs_quote_start; hov 0 strm; str emacs_quote_end >]
+  else hov 0 strm
 
-let warnbody strm =
-  [< warnstart() ; hov 0 (str "Warning: " ++ strm) ; warnend() >]
+let warnbody strm = emacs_quote (str "Warning: " ++ strm)
 
 (* pretty printing functions WITHOUT FLUSH *)
 let pp_with ft strm =
@@ -339,3 +341,10 @@ let msgnl x = msgnl_with !std_ft x
 let msgerr x = msg_with !err_ft x
 let msgerrnl x = msgnl_with !err_ft x
 let msg_warning x = msg_warning_with !err_ft x
+
+(* Same specific display in emacs as warning, but without the "Warning:" *)
+let msg_debug x = msgnl (emacs_quote x)
+
+let string_of_ppcmds c =
+  msg_with Format.str_formatter c;
+  Format.flush_str_formatter ()
diff --git a/lib/pp.mli b/lib/pp.mli
index 61b544e3..7917ba15 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -1,30 +1,26 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Pp_control
-(*i*)
 
-(* Modify pretty printing functions behavior for emacs ouput (special
+(** Modify pretty printing functions behavior for emacs ouput (special
    chars inserted at some places). This function should called once in
    module [Options], that's all. *)
 val make_pp_emacs:unit -> unit
 val make_pp_nonemacs:unit -> unit
 
-(* Pretty-printers. *)
+(** Pretty-printers. *)
 
 type ppcmd
 
 type std_ppcmds = ppcmd Stream.t
 
-(*s Formatting commands. *)
+(** {6 Formatting commands. } *)
 
 val str  : string -> std_ppcmds
 val stras : int * string -> std_ppcmds
@@ -40,11 +36,15 @@ val ismt : std_ppcmds -> bool
 val comment : int -> std_ppcmds
 val comments : ((int * int) * string) list ref
 
-(*s Concatenation. *)
+(** {6 Concatenation. } *)
 
 val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
 
-(*s Derived commands. *)
+(** {6 Evaluation. } *)
+
+val eval_ppcmds : std_ppcmds -> std_ppcmds
+
+(** {6 Derived commands. } *)
 
 val spc : unit -> std_ppcmds
 val cut : unit -> std_ppcmds
@@ -59,7 +59,7 @@ val strbrk : string -> std_ppcmds
 
 val xmlescape : ppcmd -> ppcmd
 
-(*s Boxing commands. *)
+(** {6 Boxing commands. } *)
 
 val h : int -> std_ppcmds -> std_ppcmds
 val v : int -> std_ppcmds -> std_ppcmds
@@ -67,7 +67,7 @@ val hv : int -> std_ppcmds -> std_ppcmds
 val hov : int -> std_ppcmds -> std_ppcmds
 val t : std_ppcmds -> std_ppcmds
 
-(*s Opening and closing of boxes. *)
+(** {6 Opening and closing of boxes. } *)
 
 val hb : int -> std_ppcmds
 val vb : int -> std_ppcmds
@@ -77,7 +77,7 @@ val tb : unit -> std_ppcmds
 val close : unit -> std_ppcmds
 val tclose : unit -> std_ppcmds
 
-(*s Pretty-printing functions \emph{without flush}. *)
+(** {6 Pretty-printing functions {% \emph{%}without flush{% }%}. } *)
 
 val pp_with : Format.formatter -> std_ppcmds -> unit
 val ppnl_with : Format.formatter -> std_ppcmds -> unit
@@ -87,31 +87,37 @@ val pp_flush_with : Format.formatter -> unit -> unit
 
 val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit
 
-(*s Pretty-printing functions \emph{with flush}. *)
+(** {6 Pretty-printing functions {% \emph{%}with flush{% }%}. } *)
 
 val msg_with : Format.formatter -> std_ppcmds -> unit
 val msgnl_with : Format.formatter -> std_ppcmds -> unit
 
 
-(*s The following functions are instances of the previous ones on
+(** {6 ... } *)
+(** The following functions are instances of the previous ones on
   [std_ft] and [err_ft]. *)
 
-(*s Pretty-printing functions \emph{without flush} on [stdout] and [stderr]. *)
+(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
 
 val pp : std_ppcmds -> unit
 val ppnl : std_ppcmds -> unit
 val pperr : std_ppcmds -> unit
 val pperrnl : std_ppcmds -> unit
-val message : string -> unit       (* = pPNL *)
+val message : string -> unit       (** = pPNL *)
 val warning : string -> unit
 val warn : std_ppcmds -> unit
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
-(*s Pretty-printing functions \emph{with flush} on [stdout] and [stderr]. *)
+(** {6 Pretty-printing functions {% \emph{%}with flush{% }%} on [stdout] and [stderr]. } *)
 
 val msg : std_ppcmds -> unit
 val msgnl : std_ppcmds -> unit
 val msgerr : std_ppcmds -> unit
 val msgerrnl : std_ppcmds -> unit
 val msg_warning : std_ppcmds -> unit
+
+(** Same specific display in emacs as warning, but without the "Warning:" **)
+val msg_debug : std_ppcmds -> unit
+
+val string_of_ppcmds : std_ppcmds -> string
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index a7ad553b..dce42e29 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pp_control.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* Parameters of pretty-printing *)
 
 type pp_global_params = {
@@ -49,40 +47,18 @@ let get_gp ft =
     max_depth = Format.pp_get_max_boxes ft ();
     ellipsis = Format.pp_get_ellipsis_text ft () }
 
-
-(* Output functions of pretty-printing *)
-
-type 'a pp_formatter_params = {
-  fp_output : out_channel ;
-  fp_output_function : string -> int -> int -> unit ;
-  fp_flush_function : unit -> unit }
-
-(* Output functions for stdout and stderr *)
-
-let std_fp = {
-  fp_output = stdout ;
-  fp_output_function = output stdout;
-  fp_flush_function = (fun () -> flush stdout) }
-
-let err_fp = {
-  fp_output = stderr ;
-  fp_output_function = output stderr;
-  fp_flush_function = (fun () -> flush stderr) }
-
 (* with_fp : 'a pp_formatter_params -> Format.formatter
  * returns of formatter for given formatter functions *)
 
-let with_fp fp =
-  let ft = Format.make_formatter fp.fp_output_function fp.fp_flush_function in
-  Format.pp_set_formatter_out_channel ft fp.fp_output;
+let with_fp chan out_function flush_function =
+  let ft = Format.make_formatter out_function flush_function in
+  Format.pp_set_formatter_out_channel ft chan;
   ft
 
 (* Output on a channel ch *)
 
 let with_output_to ch =
-  let ft = with_fp { fp_output = ch ;
-      	             fp_output_function = (output ch) ;
-	             fp_flush_function = (fun () -> flush ch) } in
+  let ft = with_fp ch (output ch) (fun () -> flush ch) in
   set_gp ft deep_gp;
   ft
 
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index bbc771d5..f887e9ec 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -1,14 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pp_control.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Parameters of pretty-printing. *)
+(** Parameters of pretty-printing. *)
 
 type pp_global_params = {
   margin : int;
@@ -23,24 +21,15 @@ val set_dflt_gp : Format.formatter -> unit
 val get_gp : Format.formatter -> pp_global_params
 
 
-(*s Output functions of pretty-printing. *)
-
-type 'a pp_formatter_params = {
-  fp_output : out_channel;
-  fp_output_function : string -> int -> int -> unit;
-  fp_flush_function : unit -> unit }
-
-val std_fp : (int*string) pp_formatter_params
-val err_fp : (int*string) pp_formatter_params
+(** {6 Output functions of pretty-printing. } *)
 
-val with_fp : 'a pp_formatter_params -> Format.formatter
 val with_output_to : out_channel -> Format.formatter
 
 val std_ft : Format.formatter ref
 val err_ft : Format.formatter ref
 val deep_ft : Format.formatter ref
 
-(*s For parametrization through vernacular. *)
+(** {6 For parametrization through vernacular. } *)
 
 val set_depth_boxes : int option -> unit
 val get_depth_boxes : unit -> int option
diff --git a/lib/predicate.ml b/lib/predicate.ml
index 506a87c9..e419aa6e 100644
--- a/lib/predicate.ml
+++ b/lib/predicate.ml
@@ -10,8 +10,6 @@
 (*                                                                     *)
 (************************************************************************)
 
-(* $Id: predicate.ml 12337 2009-09-17 15:58:14Z glondu $ *)
-
 (* Sets over ordered types *)
 
 module type OrderedType =
diff --git a/lib/predicate.mli b/lib/predicate.mli
index 85596fea..bcc89e72 100644
--- a/lib/predicate.mli
+++ b/lib/predicate.mli
@@ -1,9 +1,7 @@
 
-(*i $Id: predicate.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
+(** Module [Pred]: sets over infinite ordered types with complement. *)
 
-(* Module [Pred]: sets over infinite ordered types with complement. *)
-
-(* This module implements the set data structure, given a total ordering
+(** This module implements the set data structure, given a total ordering
    function over the set elements. All operations over sets
    are purely applicative (no side-effects).
    The implementation uses the Set library. *)
@@ -13,7 +11,7 @@ module type OrderedType =
     type t
     val compare: t -> t -> int
   end
-          (* The input signature of the functor [Pred.Make].
+          (** The input signature of the functor [Pred.Make].
              [t] is the type of the set elements.
              [compare] is a total ordering function over the set elements.
              This is a two-argument function [f] such that
@@ -26,44 +24,44 @@ module type OrderedType =
 module type S =
   sig
     type elt
-          (* The type of the set elements. *)
+          (** The type of the set elements. *)
     type t
-          (* The type of sets. *)
+          (** The type of sets. *)
     val empty: t
-          (* The empty set. *)
+          (** The empty set. *)
     val full: t
-          (* The whole type. *)
+          (** The whole type. *)
     val is_empty: t -> bool
-        (* Test whether a set is empty or not. *)
+        (** Test whether a set is empty or not. *)
     val is_full: t -> bool
-        (* Test whether a set contains the whole type or not. *)
+        (** Test whether a set contains the whole type or not. *)
     val mem: elt -> t -> bool
-        (* [mem x s] tests whether [x] belongs to the set [s]. *)
+        (** [mem x s] tests whether [x] belongs to the set [s]. *)
     val singleton: elt -> t
-        (* [singleton x] returns the one-element set containing only [x]. *)
+        (** [singleton x] returns the one-element set containing only [x]. *)
     val add: elt -> t -> t
-        (* [add x s] returns a set containing all elements of [s],
+        (** [add x s] returns a set containing all elements of [s],
            plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
     val remove: elt -> t -> t
-        (* [remove x s] returns a set containing all elements of [s],
+        (** [remove x s] returns a set containing all elements of [s],
            except [x]. If [x] was not in [s], [s] is returned unchanged. *)
     val union: t -> t -> t
     val inter: t -> t -> t
     val diff: t -> t -> t
     val complement: t -> t
-        (* Union, intersection, difference and set complement. *)
+        (** Union, intersection, difference and set complement. *)
     val equal: t -> t -> bool
-        (* [equal s1 s2] tests whether the sets [s1] and [s2] are
+        (** [equal s1 s2] tests whether the sets [s1] and [s2] are
            equal, that is, contain equal elements. *)
     val subset: t -> t -> bool
-        (* [subset s1 s2] tests whether the set [s1] is a subset of
+        (** [subset s1 s2] tests whether the set [s1] is a subset of
            the set [s2]. *)
     val elements: t -> bool * elt list
-        (* Gives a finite representation of the predicate: if the
+        (** Gives a finite representation of the predicate: if the
            boolean is false, then the predicate is given in extension.
            if it is true, then the complement is given *)
   end
 
 module Make(Ord: OrderedType): (S with type elt = Ord.t)
-        (* Functor building an implementation of the set structure
+        (** Functor building an implementation of the set structure
            given a totally ordered type. *)
diff --git a/lib/profile.ml b/lib/profile.ml
index 95163a27..39e08721 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -1,17 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: profile.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-open Gc
-
 let word_length = Sys.word_size / 8
-let int_size = Sys.word_size - 1
 
 let float_of_time t = float_of_int t /. 100.
 let time_of_float f = int_of_float (f *. 100.)
@@ -265,7 +260,7 @@ let time_overhead_B_C () =
       let _dw = dummy_spent_alloc () in
       let _dt = get_time () in
       ()
-    with _ -> assert false
+    with e when e <> Sys.Break -> assert false
   done;
   let after = get_time () in
   let beforeloop =  get_time () in
@@ -354,7 +349,6 @@ let close_profile print =
 	end
     | _ -> failwith "Inconsistency"
 
-let append_profile () = close_profile false
 let print_profile () = close_profile true
 
 let declare_profile name =
@@ -396,7 +390,7 @@ let profile1 e f a =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -409,7 +403,7 @@ let profile1 e f a =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile2 e f a b =
   let dw = spent_alloc () in
@@ -438,7 +432,7 @@ let profile2 e f a b =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -451,7 +445,7 @@ let profile2 e f a b =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile3 e f a b c =
   let dw = spent_alloc () in
@@ -480,7 +474,7 @@ let profile3 e f a b c =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -493,7 +487,7 @@ let profile3 e f a b c =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile4 e f a b c d =
   let dw = spent_alloc () in
@@ -522,7 +516,7 @@ let profile4 e f a b c d =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -535,7 +529,7 @@ let profile4 e f a b c d =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile5 e f a b c d g =
   let dw = spent_alloc () in
@@ -564,7 +558,7 @@ let profile5 e f a b c d g =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -577,7 +571,7 @@ let profile5 e f a b c d g =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile6 e f a b c d g h =
   let dw = spent_alloc () in
@@ -606,7 +600,7 @@ let profile6 e f a b c d g h =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -619,7 +613,7 @@ let profile6 e f a b c d g h =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile7 e f a b c d g h i =
   let dw = spent_alloc () in
@@ -648,7 +642,7 @@ let profile7 e f a b c d g h i =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -661,7 +655,7 @@ let profile7 e f a b c d g h i =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 (* Some utilities to compute the logical and physical sizes and depth
    of ML objects *)
diff --git a/lib/profile.mli b/lib/profile.mli
index 208238e7..a67622fd 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -1,20 +1,16 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: profile.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** {6 This program is a small time and allocation profiler for Objective Caml } *)
 
-(*s This program is a small time and allocation profiler for Objective Caml *)
+(** Adapted from Christophe Raffalli *)
 
-(*i It requires the UNIX library *)
-
-(* Adapted from Christophe Raffalli *)
-
-(* To use it, link it with the program you want to profile.
+(** To use it, link it with the program you want to profile.
 
 To trace a function "f" you first need to get a key for it by using :
 
@@ -106,23 +102,23 @@ val profile7 :
     -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h
 
 
-(* Some utilities to compute the logical and physical sizes and depth
+(** Some utilities to compute the logical and physical sizes and depth
    of ML objects *)
 
-(* Print logical size (in words) and depth of its argument *)
-(* This function does not disturb the heap *)
+(** Print logical size (in words) and depth of its argument 
+   This function does not disturb the heap *)
 val print_logical_stats : 'a -> unit
 
-(* Print physical size, logical size (in words) and depth of its argument *)
-(* This function allocates itself a lot (the same order of magnitude
+(** Print physical size, logical size (in words) and depth of its argument 
+   This function allocates itself a lot (the same order of magnitude
    as the physical size of its argument) *)
 val print_stats : 'a -> unit
 
-(* Return logical size (first for strings, then for not strings),
-   (in words) and depth of its argument *)
-(* This function allocates itself a lot *)
+(** Return logical size (first for strings, then for not strings),
+   (in words) and depth of its argument 
+   This function allocates itself a lot *)
 val obj_stats : 'a -> int * int * int
 
-(* Return physical size of its argument (string part and rest) *)
-(* This function allocates itself a lot *)
+(** Return physical size of its argument (string part and rest) 
+   This function allocates itself a lot *)
 val obj_shared_size : 'a -> int * int
diff --git a/lib/refutpat.ml4 b/lib/refutpat.ml4
deleted file mode 100644
index db25ce73..00000000
--- a/lib/refutpat.ml4
+++ /dev/null
@@ -1,33 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
-
-open Pcaml
-
-(** * Non-irrefutable patterns
-
-    This small camlp4 extension creates a "let*" variant of the "let"
-    syntax that allow the use of a non-exhaustive pattern. The typical
-    usage is:
-
-      let* x::l = foo in ...
-
-    when foo is already known to be non-empty. This way, no warnings by ocamlc.
-    A Failure is raised if the pattern doesn't match the expression.
-*)
-
-
-EXTEND
- expr:
-   [[ "let"; "*"; p = patt; "="; e1 = expr; "in"; e2 = expr ->
-       <:expr< match $e1$ with
-	        [ $p$ -> $e2$
-                | _ -> failwith "Refutable pattern failed"
-                ] >> ]];
-END
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 991ed25c..9ef7f313 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rtree.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Util
 
 
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 01fff68a..7bfac2d4 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -1,24 +1,22 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rtree.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Type of regular tree with nodes labelled by values of type 'a *)
-(* The implementation uses de Bruijn indices, so binding capture
+(** Type of regular tree with nodes labelled by values of type 'a 
+   The implementation uses de Bruijn indices, so binding capture
    is avoided by the lift operator (see example below) *)
 type 'a t
 
-(* Building trees *)
+(** Building trees *)
 
-(* build a node given a label and the vector of sons *)
+(** build a node given a label and the vector of sons *)
 val mk_node  : 'a -> 'a t array -> 'a t
 
-(* Build mutually recursive trees:
+(** Build mutually recursive trees:
     X_1 = f_1(X_1,..,X_n) ... X_n = f_n(X_1,..,X_n)
    is obtained by the following pseudo-code
    let vx = mk_rec_calls n in
@@ -32,27 +30,29 @@ val mk_node  : 'a -> 'a t array -> 'a t
   Another example: nested recursive trees rec Y = b(rec X = a(X,Y),Y,Y)
   let [|vy|] = mk_rec_calls 1 in
   let [|vx|] = mk_rec_calls 1 in
-  let [|x|] = mk_rec[|mk_node a [|vx;lift 1 vy|]
-  let [|y|] = mk_rec[|mk_node b [|x;vy;vy|]|]
+  let [|x|] = mk_rec[|mk_node a vx;lift 1 vy|]
+  let [|y|] = mk_rec[|mk_node b x;vy;vy|]
   (note the lift to avoid
  *)
 val mk_rec_calls : int -> 'a t array
 val mk_rec   : 'a t array -> 'a t array
 
-(* [lift k t] increases of [k] the free parameters of [t]. Needed
+(** [lift k t] increases of [k] the free parameters of [t]. Needed
    to avoid captures when a tree appears under [mk_rec] *)
 val lift : int -> 'a t -> 'a t
 
 val is_node : 'a t -> bool
-(* Destructors (recursive calls are expanded) *)
+
+(** Destructors (recursive calls are expanded) *)
 val dest_node  : 'a t -> 'a * 'a t array
-(* dest_param is not needed for closed trees (i.e. with no free variable) *)
+
+(** dest_param is not needed for closed trees (i.e. with no free variable) *)
 val dest_param : 'a t -> int * int
 
-(* Tells if a tree has an infinite branch *)
+(** Tells if a tree has an infinite branch *)
 val is_infinite : 'a t -> bool
 
-(* [compare_rtree f t1 t2] compares t1 t2 (top-down).
+(** [compare_rtree f t1 t2] compares t1 t2 (top-down).
    f is called on each node: if the result is negative then the
    traversal ends on false, it is is positive then deeper nodes are
    not examined, and the traversal continues on respective siblings,
@@ -66,14 +66,15 @@ val compare_rtree : ('a t -> 'b t -> int) -> 'a t -> 'b t -> bool
 
 val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
 
-(* Iterators *)
+(** Iterators *)
 
 val map : ('a -> 'b) -> 'a t -> 'b t
-(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
+
+(** [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
 val smartmap : ('a -> 'a) -> 'a t -> 'a t
 val fold : (bool -> 'a t -> ('a t -> 'b) -> 'b) -> 'a t -> 'b
 val fold2 :
   (bool -> 'a t -> 'b -> ('a t -> 'b -> 'c) -> 'c) -> 'a t -> 'b -> 'c
 
-(* A rather simple minded pretty-printer *)
+(** A rather simple minded pretty-printer *)
 val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
diff --git a/lib/segmenttree.ml b/lib/segmenttree.ml
index 2a7f9df0..9ce348a0 100644
--- a/lib/segmenttree.ml
+++ b/lib/segmenttree.ml
@@ -40,7 +40,6 @@ type domain =
 type 'a t = (domain * 'a option) array
 
 (** The root is the first item of the array. *)
-let is_root i = (i = 0)
 
 (** Standard layout for left child. *)
 let left_child i = 2 * i + 1
diff --git a/lib/segmenttree.mli b/lib/segmenttree.mli
index 4aea13e9..3258537b 100644
--- a/lib/segmenttree.mli
+++ b/lib/segmenttree.mli
@@ -7,7 +7,7 @@
 (** A mapping from a union of disjoint segments to some values of type ['a]. *)
 type 'a t
 
-(** [make [(i1, j1), v1; (i2, j2), v2; ...] creates a mapping that
+(** [make [(i1, j1), v1; (i2, j2), v2; ...]] creates a mapping that
     associates to every integer [x] the value [v1] if [i1 <= x <= j1],
     [v2] if [i2 <= x <= j2], and so one. 
     Precondition: the segments must be sorted. *)
diff --git a/lib/store.ml b/lib/store.ml
new file mode 100644
index 00000000..28eb65c8
--- /dev/null
+++ b/lib/store.ml
@@ -0,0 +1,61 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(*** This module implements an "untyped store", in this particular case we
+        see it as an extensible record whose fields are left unspecified. ***)
+
+(* We give a short implementation of a universal type. This is mostly equivalent
+    to what is proposed by module Dyn.ml, except that it requires no explicit tag. *)
+module type Universal = sig
+  type t
+  
+  type 'a etype = {
+     put : 'a -> t ;
+     get : t -> 'a option
+  }
+
+  val embed : unit -> 'a etype
+end
+
+(* We use a dynamic "name" allocator. But if we needed to serialise stores, we
+might want something static to avoid troubles with plugins order. *)
+
+let next =
+  let count = ref 0 in fun () ->
+  let n = !count in
+  incr count;
+  n
+
+type t = Obj.t Util.Intmap.t
+
+module Field = struct
+  type 'a field = {
+    set : 'a -> t -> t ;
+    get : t -> 'a option ;
+    remove : t -> t 
+  }
+  type 'a t = 'a field
+end
+
+open Field
+
+let empty = Util.Intmap.empty
+
+let field () =
+  let fid = next () in
+  let set a s =
+    Util.Intmap.add fid (Obj.repr a) s
+  in
+  let get s =
+    try Some (Obj.obj (Util.Intmap.find fid s))
+    with Not_found -> None
+  in
+  let remove s =
+    Util.Intmap.remove fid s
+  in
+  { set = set ; get = get ; remove = remove }
diff --git a/lib/store.mli b/lib/store.mli
new file mode 100644
index 00000000..5df0c99a
--- /dev/null
+++ b/lib/store.mli
@@ -0,0 +1,25 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(*** This module implements an "untyped store", in this particular case we
+        see it as an extensible record whose fields are left unspecified. ***)
+
+type t
+
+module Field : sig
+  type 'a field = {
+    set : 'a -> t -> t ;
+    get : t -> 'a option ;
+    remove : t -> t 
+  }
+  type 'a t = 'a field
+end
+
+val empty : t
+
+val field : unit -> 'a Field.field
diff --git a/lib/system.ml b/lib/system.ml
index 94a57792..ae637708 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: system.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id$ *)
 
 open Pp
 open Util
@@ -33,7 +33,7 @@ let home =
       try Sys.getenv "USERPROFILE" with Not_found ->
 	warning ("Cannot determine user home directory, using '.' .");
 	flush_all ();
-	"."
+	Filename.current_dir_name
 
 let safe_getenv n = safe_getenv_def n ("$"^n)
 
@@ -72,20 +72,49 @@ type load_path = physical_path list
 let physical_path_of_string s = s
 let string_of_physical_path p = p
 
+(* 
+ * Split a path into a list of directories. A one-liner with Str, but Coq
+ * doesn't seem to use this library at all, so here is a slighly longer version.
+ *)
+
+let lpath_from_path path path_separator =
+  let n = String.length path in
+  let rec aux i l =
+    if i < n then
+      let j =
+        try String.index_from path i path_separator
+        with Not_found -> n
+      in
+      let dir = String.sub path i (j-i) in
+      aux (j+1) (dir::l)
+    else
+      l
+  in List.rev (aux 0 [])
+
 (* 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))
+  let l = String.length p in
+  if l > n && String.sub p 0 n = curdir then
+    let n' =
+      let sl = String.length Filename.dir_sep in
+      let i = ref n in
+	while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in
+    remove_path_dot (String.sub p n' (l - 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))
+  let l = String.length p in
+  if l > n && String.sub p 0 n = cwd then
+    let n' =
+      let sl = String.length Filename.dir_sep in
+      let i = ref n in
+	while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in
+    remove_path_dot (String.sub p n' (l - n'))
   else
     remove_path_dot p
 
@@ -111,7 +140,8 @@ let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
 
 let ok_dirname f =
   f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) &&
-  try ignore (check_ident f); true with _ -> false
+  try ignore (check_ident f); true
+  with e when e <> Sys.Break -> false
 
 let all_subdirs ~unix_path:root =
   let l = ref [] in
@@ -179,6 +209,14 @@ let is_in_path lpath filename =
   try ignore (where_in_path ~warn:false lpath filename); true
   with Not_found -> false
 
+let path_separator = if Sys.os_type = "Unix" then ':' else ';'
+
+let is_in_system_path filename =
+  let path = try Sys.getenv "PATH" 
+             with Not_found -> error "system variable PATH not found" in
+  let lpath = lpath_from_path path path_separator in
+  is_in_path lpath filename
+
 let make_suffix name suffix =
   if Filename.check_suffix name suffix then name else (name ^ suffix)
 
@@ -186,17 +224,22 @@ let file_readable_p name =
   try access name [R_OK];true with Unix_error (_, _, _) -> false
 
 let open_trapping_failure name =
-  try open_out_bin name with _ -> error ("Can't open " ^ name)
+  try open_out_bin name
+  with e when e <> Sys.Break -> error ("Can't open " ^ name)
 
 let try_remove filename =
   try Sys.remove filename
-  with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++
-                   str filename ++ str" which is corrupted!" )
+  with e when e <> Sys.Break ->
+    msgnl (str"Warning: " ++ str"Could not remove file " ++
+             str filename ++ str" which is corrupted!" )
 
 let marshal_out ch v = Marshal.to_channel ch v []
-let marshal_in ch =
+let marshal_in filename ch =
   try Marshal.from_channel ch
-  with End_of_file -> error "corrupted file: reached end of file"
+  with
+    | End_of_file -> error "corrupted file: reached end of file"
+    | Failure _ (* e.g. "truncated object" *) ->
+        error (filename ^ " is corrupted, try to rebuild it.")
 
 exception Bad_magic_number of string
 
@@ -222,14 +265,14 @@ let extern_intern ?(warn=true) magic suffix =
       try
         marshal_out channel val_0;
         close_out channel
-      with e ->
-	begin try_remove filename; raise e end
+      with reraise ->
+	begin try_remove filename; raise reraise end
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name =
     try
       let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in
       let channel = raw_intern filename in
-      let v = marshal_in channel in
+      let v = marshal_in filename channel in
       close_in channel;
       v
     with Sys_error s ->
@@ -300,34 +343,10 @@ let run_command converter f c =
   done;
   (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
 
-let path_separator = if Sys.os_type = "Unix" then ':' else ';'
-
-let search_exe_in_path exe =
-  try
-    let path = Sys.getenv "PATH" in
-    let n = String.length path in
-    let rec aux i =
-      if i < n then
-        let j =
-          try String.index_from path i path_separator
-          with Not_found -> n
-        in
-        let dir = String.sub path i (j-i) in
-        let exe = Filename.concat dir exe in
-        if Sys.file_exists exe then Some exe else aux (i+1)
-      else
-        None
-    in aux 0
-  with Not_found -> None
-
 (* Time stamps. *)
 
 type time = float * float * float
 
-let process_time () =
-  let t = times ()  in
-  (t.tms_utime, t.tms_stime)
-
 let get_time () =
   let t = times ()  in
   (time(), t.tms_utime, t.tms_stime)
diff --git a/lib/system.mli b/lib/system.mli
index 6998085c..d8420e7d 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -1,18 +1,19 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: system.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** System utilities *)
 
-(*s Files and load paths. Load path entries remember the original root
+(** {6 Files and load paths} *)
+
+(** Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
     [directory]), the root path and the path relative to the root. *)
 
-
 type physical_path = string
 type load_path = physical_path list
 
@@ -22,6 +23,7 @@ val exclude_search_in_dirname : string -> unit
 
 val all_subdirs : unix_path:string -> (physical_path * string list) list
 val is_in_path : load_path -> string -> bool
+val is_in_system_path : string -> bool
 val where_in_path : ?warn:bool -> load_path -> string -> physical_path * string
 
 val physical_path_of_string : string -> physical_path
@@ -39,12 +41,13 @@ val exists_dir : string -> bool
 val find_file_in_path :
   ?warn:bool -> load_path -> string -> physical_path * string
 
-(*s Generic input and output functions, parameterized by a magic number
+(** {6 I/O functions } *)
+(** Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
   when the check fails, with the full file name. *)
 
 val marshal_out : out_channel -> 'a -> unit
-val marshal_in : in_channel -> 'a
+val marshal_in : string -> in_channel -> 'a
 
 exception Bad_magic_number of string
 
@@ -56,11 +59,12 @@ val extern_intern : ?warn:bool -> int -> string ->
 
 val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
 
-(*s Sending/receiving once with external executable *)
+(** {6 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
+(** {6 Executing commands } *)
+(** [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] *)
@@ -68,13 +72,10 @@ val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a
 val run_command : (string -> string) -> (string -> unit) -> string ->
   Unix.process_status * string
 
-val search_exe_in_path : string -> string option
-
-(*s Time stamps. *)
+(** {6 Time stamps.} *)
 
 type time
 
-val process_time : unit -> float * float
 val get_time : unit -> time
-val time_difference : time -> time -> float (* in seconds *)
+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
deleted file mode 100644
index 17d337c8..00000000
--- a/lib/tlm.ml
+++ /dev/null
@@ -1,63 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: tlm.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t
-
-let empty = Node (Gset.empty, Gmap.empty)
-
-let map (Node (_,m)) lbl = Gmap.find lbl m
-
-let xtract (Node (hereset,_)) = Gset.elements hereset
-
-let dom (Node (_,m)) = Gmap.dom m
-
-let in_dom (Node (_,m)) lbl = Gmap.mem lbl m
-
-let is_empty_node (Node(a,b)) = (Gset.elements a = []) & (Gmap.to_list b = [])
-
-let assure_arc m lbl =
-  if Gmap.mem lbl m then
-    m
-  else
-    Gmap.add lbl (Node (Gset.empty,Gmap.empty)) m
-
-let cleanse_arcs (Node (hereset,m)) =
-  let l = Gmap.rng m in
-  Node(hereset, if List.for_all is_empty_node l then Gmap.empty else m)
-
-let rec at_path f (Node (hereset,m)) = function
-  | [] ->
-      cleanse_arcs (Node(f hereset,m))
-  | h::t ->
-      let m = assure_arc m h in
-      cleanse_arcs (Node(hereset,
-                         Gmap.add h (at_path f (Gmap.find h m) t) m))
-
-let add tm (path,v) =
-  at_path (fun hereset -> Gset.add v hereset) tm path
-
-let rmv tm (path,v) =
-  at_path (fun hereset -> Gset.remove v hereset) tm path
-
-let app f tlm =
-  let rec apprec pfx (Node(hereset,m)) =
-    let path = List.rev pfx in
-    Gset.iter (fun v -> f(path,v)) hereset;
-    Gmap.iter (fun l tm -> apprec (l::pfx) tm) m
-  in
-  apprec [] tlm
-
-let to_list tlm =
-  let rec torec pfx (Node(hereset,m)) =
-    let path = List.rev pfx in
-    List.flatten((List.map (fun v -> (path,v)) (Gset.elements hereset))::
-		 (List.map (fun (l,tm) -> torec (l::pfx) tm) (Gmap.to_list m)))
-  in
-  torec [] tlm
diff --git a/lib/tlm.mli b/lib/tlm.mli
deleted file mode 100644
index 9042281f..00000000
--- a/lib/tlm.mli
+++ /dev/null
@@ -1,32 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: tlm.mli 14641 2011-11-06 11:59:10Z 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]. *)
-
-type ('a,'b) t
-
-val empty : ('a,'b) t
-
-(* Work on labels, not on paths. *)
-
-val map : ('a,'b) t -> 'a -> ('a,'b) t
-val xtract : ('a,'b) t -> 'b list
-val dom : ('a,'b) t -> 'a list
-val in_dom : ('a,'b) t -> 'a -> bool
-
-(* Work on paths, not on labels. *)
-
-val add : ('a,'b) t -> 'a list * 'b -> ('a,'b) t
-val rmv : ('a,'b) t -> ('a list * 'b) -> ('a,'b) t
-
-val app : (('a list * 'b) -> unit) -> ('a,'b) t -> unit
-val to_list : ('a,'b) t -> ('a list * 'b) list
-
diff --git a/lib/tries.ml b/lib/tries.ml
index 2540bd1e..90d23bf1 100644
--- a/lib/tries.ml
+++ b/lib/tries.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/lib/tries.mli b/lib/tries.mli
index 342c81ec..8e837677 100644
--- a/lib/tries.mli
+++ b/lib/tries.mli
@@ -12,7 +12,7 @@ sig
     
   val empty : t
       
-  (* Work on labels, not on paths. *)
+  (** Work on labels, not on paths. *)
 
   val map : t -> Y.t -> t
 
@@ -22,7 +22,7 @@ sig
 
   val in_dom : t -> Y.t -> bool
 
-  (* Work on paths, not on labels. *)
+  (** Work on paths, not on labels. *)
 
   val add : t -> Y.t list * X.t -> t
   
diff --git a/lib/unionfind.ml b/lib/unionfind.ml
new file mode 100644
index 00000000..38ab0ffa
--- /dev/null
+++ b/lib/unionfind.ml
@@ -0,0 +1,115 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** An imperative implementation of partitions via Union-Find *)
+
+(** Paths are compressed imperatively at each lookup of a
+    canonical representative. Each union also modifies in-place
+    the partition structure.
+
+    Nota: For the moment we use Pervasive's comparison for
+    choosing the smallest object as representative. This could
+    be made more generic.
+*)
+
+
+
+module type PartitionSig = sig
+
+  (** The type of elements in the partition *)
+  type elt
+
+  (** A set structure over elements *)
+  type set
+
+  (** The type of partitions *)
+  type t
+
+  (** Initialise an empty partition *)
+  val create : unit -> t
+
+  (** Add (in place) an element in the partition, or do nothing
+      if the element is already in the partition. *)
+  val add : elt -> t -> unit
+
+  (** Find the canonical representative of an element.
+      Raise [not_found] if the element isn't known yet. *)
+  val find : elt -> t -> elt
+
+  (** Merge (in place) the equivalence classes of two elements.
+      This will add the elements in the partition if necessary. *)
+  val union : elt -> elt -> t -> unit
+
+  (** Merge (in place) the equivalence classes of many elements. *)
+  val union_set : set -> t -> unit
+
+  (** Listing the different components of the partition *)
+  val partition : t -> set list
+
+end
+
+module Make (S:Set.S)(M:Map.S with type key = S.elt) = struct
+
+  type elt = S.elt
+  type set = S.t
+
+  type node =
+    | Canon of set
+    | Equiv of elt
+
+  type t = node ref M.t ref
+
+  let create () = ref (M.empty : node ref M.t)
+
+  let fresh x p =
+    let node = ref (Canon (S.singleton x)) in
+    p := M.add x node !p;
+    x, node
+
+  let rec lookup x p =
+    let node = M.find x !p in
+    match !node with
+      | Canon _ -> x, node
+      | Equiv y ->
+	let ((z,_) as res) = lookup y p in
+	if not (z == y) then node := Equiv z;
+	res
+
+  let add x p = if not (M.mem x !p) then ignore (fresh x p)
+
+  let find x p = fst (lookup x p)
+
+  let canonical x p = try lookup x p with Not_found -> fresh x p
+
+  let union x y p =
+    let ((x,_) as xcan) = canonical x p in
+    let ((y,_) as ycan) = canonical y p in
+    if x = y then ()
+    else
+      let xcan, ycan = if x < y then xcan, ycan else ycan, xcan in
+      let x,xnode = xcan and y,ynode = ycan in
+      match !xnode, !ynode with
+	| Canon lx, Canon ly ->
+	  xnode := Canon (S.union lx ly);
+	  ynode := Equiv x;
+	| _ -> assert false
+
+  let union_set s p =
+    try
+      let x = S.min_elt s in
+      S.iter (fun y -> union x y p) s
+    with Not_found -> ()
+
+  let partition p =
+    List.rev (M.fold
+		(fun x node acc -> match !node with
+		  | Equiv _ -> acc
+		  | Canon lx -> lx::acc)
+		!p [])
+
+end
diff --git a/lib/unionfind.mli b/lib/unionfind.mli
new file mode 100644
index 00000000..18468661
--- /dev/null
+++ b/lib/unionfind.mli
@@ -0,0 +1,57 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** An imperative implementation of partitions via Union-Find *)
+
+(** Paths are compressed imperatively at each lookup of a
+    canonical representative. Each union also modifies in-place
+    the partition structure.
+
+    Nota: for the moment we use Pervasive's comparison for
+    choosing the smallest object as representative. This could
+    be made more generic.
+*)
+
+module type PartitionSig = sig
+
+  (** The type of elements in the partition *)
+  type elt
+
+  (** A set structure over elements *)
+  type set
+
+  (** The type of partitions *)
+  type t
+
+  (** Initialise an empty partition *)
+  val create : unit -> t
+
+  (** Add (in place) an element in the partition, or do nothing
+      if the element is already in the partition. *)
+  val add : elt -> t -> unit
+
+  (** Find the canonical representative of an element.
+      Raise [not_found] if the element isn't known yet. *)
+  val find : elt -> t -> elt
+
+  (** Merge (in place) the equivalence classes of two elements.
+      This will add the elements in the partition if necessary. *)
+  val union : elt -> elt -> t -> unit
+
+  (** Merge (in place) the equivalence classes of many elements. *)
+  val union_set : set -> t -> unit
+
+  (** Listing the different components of the partition *)
+  val partition : t -> set list
+
+end
+
+module Make :
+  functor (S:Set.S) ->
+    functor (M:Map.S with type key = S.elt) ->
+      PartitionSig with type elt = S.elt and type set = S.t
diff --git a/lib/util.ml b/lib/util.ml
index 9a8c724f..4f14b83a 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,9 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
-
 open Pp
+open Compat
 
 (* Errors *)
 
@@ -17,11 +16,9 @@ let anomaly string = raise (Anomaly(string, str string))
 let anomalylabstrm string pps = raise (Anomaly(string,pps))
 
 exception UserError of string * std_ppcmds (* User errors *)
-let error string = raise (UserError(string, str string))
+let error string = raise (UserError("_", str string))
 let errorlabstrm l pps = raise (UserError(l,pps))
 
-exception AnomalyOnError of string * exn
-
 exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *)
 let alreadydeclared pps = raise (AlreadyDeclared(pps))
 
@@ -29,17 +26,17 @@ let todo s = prerr_string ("TODO: "^s^"\n")
 
 exception Timeout
 
-type loc = Compat.loc
-let dummy_loc = Compat.dummy_loc
-let unloc = Compat.unloc
-let make_loc = Compat.make_loc
-let join_loc = Compat.join_loc
+type loc = Loc.t
+let dummy_loc = Loc.ghost
+let join_loc = Loc.merge
+let make_loc = make_loc
+let unloc = unloc
 
 (* raising located exceptions *)
 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 anomaly_loc (loc,s,strm) = Loc.raise loc (Anomaly (s,strm))
+let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm))
+let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
 
 let located_fold_left f x (_,a) = f x a
 let located_iter2 f (_,a) (_,b) = f a b
@@ -54,6 +51,7 @@ exception Error_in_file of string * (bool * string * loc) * exn
 
 let on_fst f (a,b) = (f a,b)
 let on_snd f (a,b) = (a,f b)
+let map_pair f (a,b) = (f a,f b)
 
 (* Mapping under pairs *)
 
@@ -402,6 +400,13 @@ let rec list_compare cmp l1 l2 =
 	   | 0 -> list_compare cmp l1 l2
 	   | c -> c)
 
+let rec list_equal cmp l1 l2 =
+  match l1, l2 with
+    | [], [] -> true
+    | x1 :: l1, x2 :: l2 ->
+      cmp x1 x2 && list_equal cmp l1 l2
+    | _ -> false
+
 let list_intersect l1 l2 =
   List.filter (fun x -> List.mem x l2) l1
 
@@ -425,24 +430,21 @@ let list_subtract l1 l2 =
 let list_subtractq l1 l2 =
   if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1
 
-let list_chop n l =
-  let rec chop_aux acc = function
-    | (0, l2) -> (List.rev acc, l2)
-    | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
-    | (_, []) -> failwith "list_chop"
-  in
-  chop_aux [] (n,l)
-
 let list_tabulate f len =
   let rec tabrec n =
     if n = len then [] else (f n)::(tabrec (n+1))
   in
   tabrec 0
 
-let rec list_make n v =
-  if n = 0 then []
-  else if n < 0 then invalid_arg "list_make"
-  else v::list_make (n-1) v
+let list_addn n v =
+  let rec aux n l =
+    if n = 0 then l
+    else aux (pred n) (v::l)
+  in
+    if n < 0 then invalid_arg "list_addn"
+    else aux n
+
+let list_make n v = list_addn n v []
 
 let list_assign l n e =
   let rec assrec stk = function
@@ -497,6 +499,27 @@ let list_map4 f l1 l2 l3 l4 =
   in
   map (l1,l2,l3,l4)
 
+let list_map_to_array f l =
+  Array.of_list (List.map f l)
+
+let rec list_smartfilter f l = match l with
+    [] -> l
+  | h::tl ->
+      let tl' = list_smartfilter f tl in
+	if f h then
+	  if tl' == tl then l
+	  else h :: tl'
+	else tl'
+	  
+let list_index_f f x =
+  let rec index_x n = function
+    | y::l -> if f x y then n else index_x (succ n) l
+    | [] -> raise Not_found
+  in
+  index_x 1
+
+let list_index0_f f x l = list_index_f f x l - 1
+
 let list_index x =
   let rec index_x n = function
     | y::l -> if x = y then n else index_x (succ n) l
@@ -584,6 +607,10 @@ let rec list_remove_assoc_in_triple x = function
   | [] -> []
   | (y,_,_ as z)::l -> if x = y then l else z::list_remove_assoc_in_triple x l
 
+let rec list_assoc_snd_in_triple x = function
+    [] -> raise Not_found
+  | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_snd_in_triple x l
+
 let list_add_set x l = if List.mem x l then l else x::l
 
 let list_eq_set l1 l2 =
@@ -676,6 +703,20 @@ let rec list_map_filter f = function
       let l' = list_map_filter f l in
       match f x with None -> l' | Some y -> y::l'
 
+let list_map_filter_i f =
+  let rec aux i = function
+    | [] -> []
+    | x::l ->
+      let l' = aux (succ i) l in
+	match f i x with None -> l' | Some y -> y::l'
+  in aux 0
+
+let list_filter_along f filter l =
+  snd (list_filter2 (fun b c -> f b) (filter,l))
+
+let list_filter_with filter l =
+  list_filter_along (fun x -> x) filter l
+
 let list_subset l1 l2 =
   let t2 = Hashtbl.create 151 in
   List.iter (fun x -> Hashtbl.add t2 x ()) l2;
@@ -685,15 +726,17 @@ let list_subset l1 l2 =
   in
   look l1
 
-(* [list_split_at i l] splits [l] into two lists [(l1,l2)] such that [l1++l2=l]
-    and [l1] has length [i].
-    It raises [Failure] when [i] is negative or greater than the length of [l]  *)
-let list_split_at index l =
-  let rec aux i acc = function
-      tl when i = index -> (List.rev acc), tl
-    | hd :: tl -> aux (succ i) (hd :: acc) tl
-    | [] -> failwith "list_split_at: Invalid argument"
-  in aux 0 [] l
+(* [list_chop i l] splits [l] into two lists [(l1,l2)] such that
+   [l1++l2=l] and [l1] has length [i].
+   It raises [Failure] when [i] is negative or greater than the length of [l]  *)
+
+let list_chop n l =
+  let rec chop_aux i acc = function
+    | tl when i=0 -> (List.rev acc, tl)
+    | h::t -> chop_aux (pred i) (h::acc) t
+    | [] -> failwith "list_chop"
+  in
+  chop_aux n [] l
 
 (* [list_split_when p l] splits [l] into two lists [(l1,a::l2)] such that
     [l1++(a::l2)=l], [p a=true] and [p b = false] for every element [b] of [l1].
@@ -707,7 +750,7 @@ let list_split_when p =
   split_when_loop []
 
 (* [list_split_by p l] splits [l] into two lists [(l1,l2)] such that elements of
-   [l1] satisfy [p] and elements of [l2] do not *)
+   [l1] satisfy [p] and elements of [l2] do not; order is preserved *)
 let list_split_by p =
   let rec split_by_loop = function
   | []   -> ([],[])
@@ -757,9 +800,6 @@ let rec list_skipn n l = match n,l with
 let rec list_skipn_at_least n l =
   try list_skipn n l with Failure _ -> []
 
-let rec list_addn n x l =
-  if n = 0 then l else x :: (list_addn (pred n) x l)
-
 let list_prefix_of prefl l =
   let rec prefrec = function
     | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)
@@ -815,6 +855,10 @@ let list_fold_map' f l e =
 
 let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
 
+let rec list_assoc_f f a = function
+  | (x, e) :: xs -> if f a x then e else list_assoc_f f a xs
+  | [] -> raise Not_found
+
 (* Specification:
    - =p= is set equality (double inclusion)
    - f such that \forall l acc, (f l acc) =p= append (f l []) acc
@@ -865,6 +909,14 @@ let rec list_cartesians_filter op init ll =
 
 let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: list_drop_last tl
 
+(* Factorize lists of pairs according to the left argument *)
+let rec list_factorize_left = function
+  | (a,b)::l ->
+      let al,l' = list_split_by (fun (a',b) -> a=a') l in
+      (a,(b::List.map snd al)) :: list_factorize_left l'
+  | [] ->
+      []
+
 (* Arrays *)
 
 let array_compare item_cmp v1 v2 =
@@ -878,6 +930,12 @@ let array_compare item_cmp v1 v2 =
 	  else cmp (i-1) in
     cmp (Array.length v1 - 1)
 
+let array_equal cmp t1 t2 =
+  Array.length t1 = Array.length t2 &&
+  let rec aux i =
+    (i = Array.length t1) || (cmp t1.(i) t2.(i) && aux (i + 1))
+  in aux 0
+
 let array_exists f v =
   let rec exrec = function
     | -1 -> false
@@ -998,6 +1056,15 @@ let array_fold_left2_i f a v1 v2 =
   if Array.length v2 <> lv1 then invalid_arg "array_fold_left2";
   fold a 0
 
+let array_fold_left3 f a v1 v2 v3 =
+  let lv1 = Array.length v1 in
+  let rec fold a n =
+    if n >= lv1 then a else fold (f a v1.(n) v2.(n) v3.(n)) (succ n)
+  in
+  if Array.length v2 <> lv1 || Array.length v3 <> lv1 then
+    invalid_arg "array_fold_left2";
+  fold a 0
+
 let array_fold_left_from n f a v =
   let rec fold a n =
     if n >= Array.length v then a else fold (f a v.(n)) (succ n)
@@ -1167,6 +1234,21 @@ let array_rev_to_list a =
     if i >= Array.length a then res else tolist (i+1) (a.(i) :: res) in
   tolist 0 []
 
+let array_filter_along f filter v =
+  Array.of_list (list_filter_along f filter (Array.to_list v))
+
+let array_filter_with filter v =
+  Array.of_list (list_filter_with filter (Array.to_list v))
+
+(* Stream *)
+
+let stream_nth n st =
+  try List.nth (Stream.npeek (n+1) st) n
+  with Failure _ -> raise Stream.Failure
+
+let stream_njunk n st =
+  for i = 1 to n do Stream.junk st done
+
 (* Matrices *)
 
 let matrix_transpose mat =
diff --git a/lib/util.mli b/lib/util.mli
index e5b5f8c6..05d499cb 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -1,21 +1,19 @@
-(***********************************************************************)
-(*  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       *)
-(***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
-(*i $Id: util.mli 13492 2010-10-04 21:20:01Z herbelin $ i*)
-
-(*i*)
 open Pp
-(*i*)
+open Compat
 
-(* This module contains numerous utility functions on strings, lists,
+(** This module contains numerous utility functions on strings, lists,
    arrays, etc. *)
 
-(*s Errors. [Anomaly] is used for system errors and [UserError] for the
+(** {6 ... } *)
+(** Errors. [Anomaly] is used for system errors and [UserError] for the
    user's ones. *)
 
 exception Anomaly of string * std_ppcmds
@@ -29,9 +27,7 @@ val errorlabstrm : string -> std_ppcmds -> 'a
 exception AlreadyDeclared of std_ppcmds
 val alreadydeclared : std_ppcmds -> 'a
 
-exception AnomalyOnError of string * exn
-
-(* [todo] is for running of an incomplete code its implementation is
+(** [todo] is for running of an incomplete code its implementation is
    "do nothing" (or print a message), but this function should not be
    used in a released code *)
 
@@ -39,57 +35,59 @@ val todo : string -> unit
 
 exception Timeout
 
-type loc = Compat.loc
+type loc = Loc.t
 
 type 'a located = loc * 'a
 
 val unloc : loc -> int * int
 val make_loc : int * int -> loc
 val dummy_loc : loc
+val join_loc : loc -> loc -> loc
+
 val anomaly_loc : loc * string * std_ppcmds -> 'a
 val user_err_loc : loc * string * std_ppcmds -> 'a
 val invalid_arg_loc : loc * string -> 'a
-val join_loc : loc -> loc -> loc
 val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
 val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
 val down_located : ('a -> 'b) -> 'a located -> 'b
 
-(* Like [Exc_located], but specifies the outermost file read, the
+(** Like [Exc_located], but specifies the outermost file read, the
    input buffer associated to the location of the error (or the module name
    if boolean is true), and the error itself. *)
 
 exception Error_in_file of string * (bool * string * loc) * exn
 
-(* Mapping under pairs *)
+(** Mapping under pairs *)
 
 val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
 val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
+val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b
 
-(* Going down pairs *)
+(** Going down pairs *)
 
 val down_fst : ('a -> 'b) -> 'a * 'c -> 'b
 val down_snd : ('a -> 'b) -> 'c * 'a -> 'b
 
-(* Mapping under triple *)
+(** Mapping under triple *)
 
 val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
 val on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'd
 val on_pi3 : ('a -> 'b) -> 'c * 'd * 'a -> 'c * 'd * 'b
 
-(*s Projections from triplets *)
+(** {6 Projections from triplets } *)
 
 val pi1 : 'a * 'b * 'c -> 'a
 val pi2 : 'a * 'b * 'c -> 'b
 val pi3 : 'a * 'b * 'c -> 'c
 
-(*s Chars. *)
+(** {6 Chars. } *)
 
 val is_letter : char -> bool
 val is_digit : char -> bool
 val is_ident_tail : char -> bool
 val is_blank : char -> bool
 
-(*s Strings. *)
+(** {6 Strings. } *)
 
 val explode : string -> string list
 val implode : string list -> string
@@ -116,9 +114,10 @@ val check_ident_soft : string -> unit
 val lowercase_first_char_utf8 : string -> string
 val ascii_of_ident : string -> string
 
-(*s Lists. *)
+(** {6 Lists. } *)
 
 val list_compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
+val list_equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
 val list_add_set : 'a -> 'a list -> 'a list
 val list_eq_set : 'a list -> 'a list -> bool
 val list_intersect : 'a list -> 'a list -> 'a list
@@ -126,8 +125,8 @@ val list_union : 'a list -> 'a list -> 'a list
 val list_unionq : 'a list -> 'a list -> 'a list
 val list_subtract : 'a list -> 'a list -> 'a list
 val list_subtractq : 'a list -> 'a list -> 'a list
-val list_chop : int -> 'a list -> 'a list * 'a list
-(* [list_tabulate f n] builds [[f 0; ...; f (n-1)]] *)
+
+(** [list_tabulate f n] builds [[f 0; ...; f (n-1)]] *)
 val list_tabulate : (int -> 'a) -> int -> 'a list
 val list_make : int -> 'a -> 'a list
 val list_assign : 'a list -> int -> 'a -> 'a list
@@ -135,7 +134,11 @@ 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
 val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list
-(* [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
+val list_map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
+val list_filter_with : bool list -> 'a list -> 'a list
+val list_filter_along : ('a -> bool) -> 'a list -> 'b list -> 'b list
+
+(** [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
    [ f ai == ai], then [list_smartmap f l==l] *)
 val list_smartmap : ('a -> 'a) -> 'a list -> 'a list
 val list_map_left : ('a -> 'b) -> 'a list -> 'b list
@@ -146,14 +149,24 @@ val list_map3 :
   ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
 val list_map4 :
   ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
+val list_map_to_array : ('a -> 'b) -> 'a list -> 'b array
 val list_filter_i :
   (int -> 'a -> bool) -> 'a list -> 'a list
-(* [list_index] returns the 1st index of an element in a list (counting from 1) *)
+
+(** [list_smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
+   [f ai = true], then [list_smartfilter f l==l] *)
+val list_smartfilter : ('a -> bool) -> 'a list -> 'a list
+
+(** [list_index] returns the 1st index of an element in a list (counting from 1) *)
 val list_index : 'a -> 'a list -> int
-(* [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
+val list_index_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
+
+(** [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
 val list_unique_index : 'a -> 'a list -> int
-(* [list_index0] behaves as [list_index] except that it starts counting at 0 *)
+
+(** [list_index0] behaves as [list_index] except that it starts counting at 0 *)
 val list_index0 : 'a -> 'a list -> int
+val list_index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
 val list_iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
 val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
 val list_fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
@@ -166,15 +179,18 @@ 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_remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list
+val list_assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b
 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
 val list_try_find : ('a -> 'b) -> 'a list -> 'b
 val list_uniquize : 'a list -> 'a list
-(* merges two sorted lists and preserves the uniqueness property: *)
+
+(** merges two sorted lists and preserves the uniqueness property: *)
 val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
 val list_subset : 'a list -> 'a list -> bool
-val list_split_at : int -> 'a list -> 'a list*'a list
+val list_chop : int -> 'a list -> 'a list * 'a list
+(* former [list_split_at] was a duplicate of [list_chop] *)
 val list_split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
 val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
 val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
@@ -186,28 +202,36 @@ val list_skipn : int -> 'a list -> 'a list
 val list_skipn_at_least : int -> 'a list -> 'a list
 val list_addn : int -> 'a -> 'a list -> 'a list
 val list_prefix_of : 'a list -> 'a list -> bool
-(* [list_drop_prefix p l] returns [t] if [l=p++t] else return [l] *)
+
+(** [list_drop_prefix p l] returns [t] if [l=p++t] else return [l] *)
 val list_drop_prefix : 'a list -> 'a list -> 'a list
 val list_drop_last : 'a list -> 'a list
-(* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
+
+(** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
 val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
 val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
-(* raises [Invalid_argument] if the two lists don't have the same length *)
+
+(** raises [Invalid_argument] if the two lists don't have the same length *)
 val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
 val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
-(* [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
+
+(** [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' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
 val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
-(* A generic cartesian product: for any operator (**),
+val list_assoc_f : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b
+
+(** A generic cartesian product: for any operator (**),
    [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
    and so on if there are more elements in the lists. *)
 val list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
-(* [list_cartesians] is an n-ary cartesian product: it iterates
+
+(** [list_cartesians] is an n-ary cartesian product: it iterates
    [list_cartesian] over a list of lists.  *)
 val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
-(* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
+
+(** list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
 val list_combinations : 'a list list -> 'a list list
 val list_combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
 
@@ -218,10 +242,12 @@ val list_cartesians_filter :
   ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
 
 val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+val list_factorize_left : ('a * 'b) list -> ('a * 'b list) list
 
-(*s Arrays. *)
+(** {6 Arrays. } *)
 
 val array_compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int
+val array_equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
 val array_exists : ('a -> bool) -> 'a array -> bool
 val array_for_all : ('a -> bool) -> 'a array -> bool
 val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
@@ -243,6 +269,8 @@ val array_fold_right2 :
   ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
 val array_fold_left2 :
   ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
+val array_fold_left3 :
+  ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a
 val array_fold_left2_i :
   (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
 val array_fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
@@ -267,12 +295,19 @@ val array_fold_map2' :
 val array_distinct : 'a array -> bool
 val array_union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
 val array_rev_to_list : 'a array -> 'a list
+val array_filter_along : ('a -> bool) -> 'a list -> 'b array -> 'b array
+val array_filter_with : bool list -> 'a array -> 'a array
+
+(** {6 Streams. } *)
 
-(*s Matrices *)
+val stream_nth : int -> 'a Stream.t -> 'a
+val stream_njunk : int -> 'a Stream.t -> unit
+
+(** {6 Matrices. } *)
 
 val matrix_transpose : 'a list list -> 'a list list
 
-(*s Functions. *)
+(** {6 Functions. } *)
 
 val identity : 'a -> 'a
 val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
@@ -302,12 +337,12 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list
 val interval : int -> int -> int list
 
 
-(* In [map_succeed f l] an element [a] is removed if [f a] raises *)
-(* [Failure _] otherwise behaves as [List.map f l] *)
+(** In [map_succeed f l] an element [a] is removed if [f a] raises 
+   [Failure _] otherwise behaves as [List.map f l] *)
 
 val map_succeed : ('a -> 'b) -> 'a list -> 'b list
 
-(*s Pretty-printing. *)
+(** {6 Pretty-printing. } *)
 
 val pr_spc : unit -> std_ppcmds
 val pr_fnl : unit -> std_ppcmds
@@ -322,7 +357,8 @@ val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
 val nth : int -> std_ppcmds
 
 val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
-(* unlike all other functions below, [prlist] works lazily.
+
+(** unlike all other functions below, [prlist] works lazily.
    if a strict behavior is needed, use [prlist_strict] instead. *)
 val prlist_strict :  ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val prlist_with_sep :
@@ -339,34 +375,36 @@ val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
 val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val surround : std_ppcmds -> std_ppcmds
 
-(*s Memoization. *)
+(** {6 Memoization. } *)
 
-(* General comments on memoization:
+(** General comments on memoization:
    - cache is created whenever the function is supplied (because of
       ML's polymorphic value restriction).
    - cache is never flushed (unless the memoized fun is GC'd)
- *)
-(* One cell memory: memorizes only the last call *)
+ 
+   One cell memory: memorizes only the last call *)
 val memo1_1 : ('a -> 'b) -> ('a -> 'b)
 val memo1_2 : ('a -> 'b -> 'c) -> ('a -> 'b -> 'c)
-(* with custom equality (used to deal with various arities) *)
+
+(** with custom equality (used to deal with various arities) *)
 val memo1_eq : ('a -> 'a -> bool) -> ('a -> 'b) -> ('a -> 'b)
 
-(* Memorizes the last [n] distinct calls. Efficient only for small [n]. *)
+(** Memorizes the last [n] distinct calls. Efficient only for small [n]. *)
 val memon_eq : ('a -> 'a -> bool) -> int -> ('a -> 'b) -> ('a -> 'b)
 
-(*s Size of an ocaml value (in words, bytes and kilobytes). *)
+(** {6 Size of an ocaml value (in words, bytes and kilobytes). } *)
 
 val size_w : 'a -> int
 val size_b : 'a -> int
 val size_kb : 'a -> int
 
-(*s Total size of the allocated ocaml heap. *)
+(** {6 Total size of the allocated ocaml heap. } *)
 
 val heap_size : unit -> int
 val heap_size_kb : unit -> int
 
-(*s Coq interruption: set the following boolean reference to interrupt Coq
+(** {6 ... } *)
+(** Coq interruption: set the following boolean reference to interrupt Coq
     (it eventually raises [Break], simulating a Ctrl-C) *)
 
 val interrupt : bool ref
diff --git a/lib/xml_lexer.mli b/lib/xml_lexer.mli
new file mode 100644
index 00000000..a1ca0576
--- /dev/null
+++ b/lib/xml_lexer.mli
@@ -0,0 +1,44 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+ *)
+
+type error =
+	| EUnterminatedComment
+	| EUnterminatedString
+	| EIdentExpected
+	| ECloseExpected
+	| ENodeExpected
+	| EAttributeNameExpected
+	| EAttributeValueExpected
+	| EUnterminatedEntity
+
+exception Error of error
+
+type token =
+	| Tag of string * (string * string) list * bool
+	| PCData of string
+	| Endtag of string
+	| Eof
+
+type pos = int * int * int * int
+
+val init : Lexing.lexbuf -> unit 
+val close : Lexing.lexbuf -> unit
+val token : Lexing.lexbuf -> token
+val pos : Lexing.lexbuf -> pos
+val restore : pos -> unit
\ No newline at end of file
diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll
new file mode 100644
index 00000000..5b06e720
--- /dev/null
+++ b/lib/xml_lexer.mll
@@ -0,0 +1,305 @@
+{(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+ *)
+
+open Lexing
+
+type error =
+	| EUnterminatedComment
+	| EUnterminatedString
+	| EIdentExpected
+	| ECloseExpected
+	| ENodeExpected
+	| EAttributeNameExpected
+	| EAttributeValueExpected
+	| EUnterminatedEntity
+
+exception Error of error
+
+type pos = int * int * int * int
+
+type token =
+	| Tag of string * (string * string) list * bool
+	| PCData of string
+	| Endtag of string
+	| Eof
+
+let last_pos = ref 0
+and current_line = ref 0
+and current_line_start = ref 0
+
+let tmp = Buffer.create 200
+
+let idents = Hashtbl.create 0
+
+let _ = begin
+	Hashtbl.add idents "gt;" ">";
+	Hashtbl.add idents "lt;" "<";
+	Hashtbl.add idents "amp;" "&";
+	Hashtbl.add idents "apos;" "'";
+	Hashtbl.add idents "quot;" "\"";
+end
+
+let init lexbuf =
+	current_line := 1;
+	current_line_start := lexeme_start lexbuf;
+	last_pos := !current_line_start
+
+let close lexbuf =
+	Buffer.reset tmp
+
+let pos lexbuf =
+	!current_line ,	!current_line_start ,
+	!last_pos ,
+	lexeme_start lexbuf
+
+let restore (cl,cls,lp,_) =
+	current_line := cl;
+	current_line_start := cls;
+	last_pos := lp
+
+let newline lexbuf =
+	incr current_line;
+	last_pos := lexeme_end lexbuf;
+	current_line_start := !last_pos
+
+let error lexbuf e =
+	last_pos := lexeme_start lexbuf;
+	raise (Error e)
+
+}
+
+let newline = ['\n']
+let break = ['\r']
+let space = [' ' '\t']
+let identchar =  ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-']
+let entitychar = ['A'-'Z' 'a'-'z']
+let pcchar = [^ '\r' '\n' '<' '>' '&']
+
+rule token = parse
+	| newline | (newline break) | break
+		{
+			newline lexbuf;
+                        PCData "\n"
+		}
+	| "<!--"
+		{
+			last_pos := lexeme_start lexbuf;
+			comment lexbuf;
+			token lexbuf
+		}
+	| "<?"
+		{
+			last_pos := lexeme_start lexbuf;
+			header lexbuf;
+			token lexbuf;
+		}
+	| '<' space* '/' space*
+		{
+			last_pos := lexeme_start lexbuf;
+			let tag = ident_name lexbuf in
+			ignore_spaces lexbuf;
+			close_tag lexbuf;
+			Endtag tag
+		}
+	| '<' space*
+		{
+			last_pos := lexeme_start lexbuf;
+			let tag = ident_name lexbuf in
+			ignore_spaces lexbuf;
+			let attribs, closed = attributes lexbuf in
+			Tag(tag, attribs, closed)
+		}
+	| "&#"
+		{
+			last_pos := lexeme_start lexbuf;
+			Buffer.reset tmp;
+			Buffer.add_string tmp (lexeme lexbuf);
+			PCData (pcdata lexbuf)
+		}
+	| '&'
+		{
+			last_pos := lexeme_start lexbuf;
+			Buffer.reset tmp;
+			Buffer.add_string tmp (entity lexbuf);
+			PCData (pcdata lexbuf)
+		}
+	| pcchar+
+		{
+			last_pos := lexeme_start lexbuf;
+			Buffer.reset tmp;
+			Buffer.add_string tmp (lexeme lexbuf);
+			PCData (pcdata lexbuf)
+		}
+	| eof { Eof }
+	| _
+		{ error lexbuf ENodeExpected }
+
+and ignore_spaces = parse
+        | newline | (newline break) | break
+		{
+			newline lexbuf;
+			ignore_spaces lexbuf
+		}
+	| space +
+		{ ignore_spaces lexbuf }
+	| ""
+		{ () }
+
+and comment = parse
+        | newline | (newline break) | break
+		{
+			newline lexbuf;
+			comment lexbuf
+		}
+	| "-->"
+		{ () }
+	| eof
+		{ raise (Error EUnterminatedComment) }
+	| _
+		{ comment lexbuf }
+
+and header = parse
+        | newline | (newline break) | break
+		{
+			newline lexbuf;
+			header lexbuf
+		}
+	| "?>"
+		{ () }
+	| eof
+		{ error lexbuf ECloseExpected }
+	| _
+		{ header lexbuf }
+
+and pcdata = parse
+        | newline | (newline break) | break
+                {
+                        Buffer.add_char tmp '\n';
+                        newline lexbuf;
+                        pcdata lexbuf
+                }
+	| pcchar+
+		{
+			Buffer.add_string tmp (lexeme lexbuf);
+			pcdata lexbuf
+		}
+	| "&#"
+		{
+			Buffer.add_string tmp (lexeme lexbuf);
+			pcdata lexbuf;
+		}
+	| '&'
+		{
+			Buffer.add_string tmp (entity lexbuf);
+			pcdata lexbuf
+		}
+	| ""
+		{ Buffer.contents tmp }
+
+and entity = parse
+	| entitychar+ ';'
+		{
+			let ident = lexeme lexbuf in
+			try
+				Hashtbl.find idents (String.lowercase ident)
+			with
+				Not_found -> "&" ^ ident
+		}
+	| _ | eof
+		{ raise (Error EUnterminatedEntity) }
+
+and ident_name = parse
+	| identchar+
+		{ lexeme lexbuf }
+	| _ | eof
+		{ error lexbuf EIdentExpected }
+
+and close_tag = parse
+	| '>'
+		{ () }
+	| _ | eof
+		{ error lexbuf ECloseExpected }
+
+and attributes = parse
+	| '>'
+		{ [], false }
+	| "/>"
+		{ [], true }
+	| "" (* do not read a char ! *)
+		{
+			let key = attribute lexbuf in
+			let data = attribute_data lexbuf in
+			ignore_spaces lexbuf;
+			let others, closed = attributes lexbuf in
+			(key, data) :: others, closed
+		}
+
+and attribute = parse
+	| identchar+
+		{ lexeme lexbuf }
+	| _ | eof
+		{ error lexbuf EAttributeNameExpected }
+
+and attribute_data = parse
+	| space* '=' space* '"'
+		{
+			Buffer.reset tmp;
+			last_pos := lexeme_end lexbuf;
+			dq_string lexbuf
+		}
+	| space* '=' space* '\''
+		{
+			Buffer.reset tmp;
+			last_pos := lexeme_end lexbuf;
+			q_string lexbuf
+		}
+	| _ | eof
+		{ error lexbuf EAttributeValueExpected }
+
+and dq_string = parse
+	| '"'
+		{ Buffer.contents tmp }
+	| '\\' [ '"' '\\' ]
+		{
+			Buffer.add_char tmp (lexeme_char lexbuf 1);
+			dq_string lexbuf
+		}
+	| eof
+		{ raise (Error EUnterminatedString) }
+	| _
+		{ 
+			Buffer.add_char tmp (lexeme_char lexbuf 0);
+			dq_string lexbuf
+		}
+
+and q_string = parse
+	| '\''
+		{ Buffer.contents tmp }
+	| '\\' [ '\'' '\\' ]
+		{
+			Buffer.add_char tmp (lexeme_char lexbuf 1);
+			q_string lexbuf
+		}
+	| eof
+		{ raise (Error EUnterminatedString) }
+	| _
+		{ 
+			Buffer.add_char tmp (lexeme_char lexbuf 0);
+			q_string lexbuf
+		}
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
new file mode 100644
index 00000000..600796f7
--- /dev/null
+++ b/lib/xml_parser.ml
@@ -0,0 +1,237 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ * Copyright (C) 2003 Jacques Garrigue
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+ *)
+
+open Printf
+
+type xml = 
+        | Element of (string * (string * string) list * xml list)
+        | PCData of string
+
+type error_pos = {
+        eline : int;
+        eline_start : int;
+        emin : int;
+        emax : int;
+}
+
+type error_msg =
+        | UnterminatedComment
+        | UnterminatedString
+        | UnterminatedEntity
+        | IdentExpected
+        | CloseExpected
+        | NodeExpected
+        | AttributeNameExpected
+        | AttributeValueExpected
+        | EndOfTagExpected of string
+        | EOFExpected
+	| Empty
+
+type error = error_msg * error_pos
+
+exception Error of error
+
+exception File_not_found of string
+
+type t = {
+	mutable check_eof : bool;
+	mutable concat_pcdata : bool;
+}
+
+type source = 
+	| SFile of string
+	| SChannel of in_channel
+	| SString of string
+	| SLexbuf of Lexing.lexbuf
+
+type state = {
+	source : Lexing.lexbuf;
+	stack : Xml_lexer.token Stack.t;
+	xparser : t;
+}
+
+exception Internal_error of error_msg
+exception NoMoreData
+
+let xml_error = ref (fun _ -> assert false)
+let file_not_found = ref (fun _ -> assert false)
+
+let is_blank s =
+  let len = String.length s in
+  let break = ref true in
+  let i = ref 0 in
+  while !break && !i < len do
+    let c = s.[!i] in
+    (* no '\r' because we replaced them in the lexer *)
+    if c = ' ' || c = '\n' || c = '\t' then incr i
+    else break := false
+  done;
+  !i = len
+
+let _raises e f =
+	xml_error := e;
+	file_not_found := f
+
+let make () =
+	{
+		check_eof = true;
+		concat_pcdata = true;
+	}
+
+let check_eof p v = p.check_eof <- v
+let concat_pcdata p v = p.concat_pcdata <- v
+
+let pop s =
+	try
+		Stack.pop s.stack
+	with
+		Stack.Empty ->
+			Xml_lexer.token s.source
+
+let push t s =
+	Stack.push t s.stack
+
+let canonicalize l =
+  let has_elt = List.exists (function Element _ -> true | _ -> false) l in
+  if has_elt then List.filter (function PCData s -> not (is_blank s) | _ -> true) l
+  else l
+
+let rec read_node s =
+	match pop s with
+	| Xml_lexer.PCData s -> PCData s
+	| Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, [])
+	| Xml_lexer.Tag (tag, attr, false) ->
+          let elements = read_elems tag s in
+          Element (tag, attr, canonicalize elements)
+	| t ->
+		push t s;
+		raise NoMoreData
+and
+	read_elems tag s =
+		let elems = ref [] in
+		(try
+                  while true do
+                    let node = read_node s in
+                    match node, !elems with
+                    | PCData c , (PCData c2) :: q ->
+                      elems := PCData (c2 ^ c) :: q
+                    | _, l ->
+                      elems := node :: l
+                  done
+		with
+			NoMoreData -> ());
+		match pop s with
+		| Xml_lexer.Endtag s when s = tag -> List.rev !elems
+		| t -> raise (Internal_error (EndOfTagExpected tag))
+
+let rec read_xml s =
+  let node = read_node s in
+  match node with
+  | Element _ -> node
+  | PCData c ->
+    if is_blank c then read_xml s
+    else raise (Xml_lexer.Error Xml_lexer.ENodeExpected)
+
+let convert = function
+	| Xml_lexer.EUnterminatedComment -> UnterminatedComment
+	| Xml_lexer.EUnterminatedString -> UnterminatedString
+	| Xml_lexer.EIdentExpected -> IdentExpected
+	| Xml_lexer.ECloseExpected -> CloseExpected
+	| Xml_lexer.ENodeExpected -> NodeExpected
+	| Xml_lexer.EAttributeNameExpected -> AttributeNameExpected
+	| Xml_lexer.EAttributeValueExpected -> AttributeValueExpected
+	| Xml_lexer.EUnterminatedEntity -> 	UnterminatedEntity
+
+let error_of_exn stk = function
+  | NoMoreData when Stack.pop stk = Xml_lexer.Eof -> Empty
+  | NoMoreData -> NodeExpected
+  | Internal_error e -> e
+  | Xml_lexer.Error e -> convert e
+  | e -> raise e
+
+let do_parse xparser source =
+        let stk = Stack.create() in
+	try
+		Xml_lexer.init source;
+		let s = { source = source; xparser = xparser; stack = stk } in
+		let x = read_xml s in
+		if xparser.check_eof && pop s <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
+		Xml_lexer.close source;
+		x
+	with e when e <> Sys.Break ->
+	  Xml_lexer.close source;
+	  raise (!xml_error (error_of_exn stk e) source)
+
+let parse p = function
+	| SChannel ch -> do_parse p (Lexing.from_channel ch)
+	| SString str -> do_parse p (Lexing.from_string str)
+	| SLexbuf lex -> do_parse p lex
+	| SFile fname ->
+		let ch = (try open_in fname with Sys_error _ -> raise (!file_not_found fname)) in
+		try
+			let x = do_parse p (Lexing.from_channel ch) in
+			close_in ch;
+			x
+		with
+			reraise ->
+				close_in ch;
+				raise reraise
+
+
+let error_msg = function
+        | UnterminatedComment -> "Unterminated comment"
+        | UnterminatedString -> "Unterminated string"
+        | UnterminatedEntity -> "Unterminated entity"
+        | IdentExpected -> "Ident expected"
+        | CloseExpected -> "Element close expected"
+        | NodeExpected -> "Xml node expected"
+        | AttributeNameExpected -> "Attribute name expected"
+        | AttributeValueExpected -> "Attribute value expected"
+        | EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag
+        | EOFExpected -> "End of file expected"
+	| Empty -> "Empty"
+
+let error (msg,pos) =
+        if pos.emin = pos.emax then
+                sprintf "%s line %d character %d" (error_msg msg) pos.eline (pos.emin - pos.eline_start)
+        else
+                sprintf "%s line %d characters %d-%d" (error_msg msg) pos.eline (pos.emin - pos.eline_start) (pos.emax - pos.eline_start)
+        
+let line e = e.eline
+
+let range e = 
+        e.emin - e.eline_start , e.emax - e.eline_start
+
+let abs_range e =
+        e.emin , e.emax
+
+let pos source =
+        let line, lstart, min, max = Xml_lexer.pos source in
+        {
+                eline = line;
+                eline_start = lstart;
+                emin = min;
+                emax = max;
+        }
+
+let () = _raises (fun x p -> 
+        (* local cast : Xml.error_msg -> error_msg *)
+        Error (x, pos p))
+        (fun f -> File_not_found f)
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
new file mode 100644
index 00000000..cc9bcd33
--- /dev/null
+++ b/lib/xml_parser.mli
@@ -0,0 +1,105 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+ *)
+
+(** Xml Light Parser
+
+ While basic parsing functions can be used in the {!Xml} module, this module
+ is providing a way to create, configure and run an Xml parser.
+
+*)
+
+
+(** An Xml node is either
+        [Element (tag-name, attributes, children)] or [PCData text] *)
+type xml = 
+        | Element of (string * (string * string) list * xml list)
+        | PCData of string
+
+(** Abstract type for an Xml parser. *)
+type t
+
+(** {6:exc Xml Exceptions} *)
+
+(** Several exceptions can be raised when parsing an Xml document : {ul
+        {li {!Xml.Error} is raised when an xml parsing error occurs. the
+                {!Xml.error_msg} tells you which error occured during parsing
+                and the {!Xml.error_pos} can be used to retreive the document
+                location where the error occured at.}
+        {li {!Xml.File_not_found} is raised when and error occured while
+                opening a file with the {!Xml.parse_file} function.}
+        }
+ *)
+
+type error_pos
+
+type error_msg =
+        | UnterminatedComment
+        | UnterminatedString
+        | UnterminatedEntity
+        | IdentExpected
+        | CloseExpected
+        | NodeExpected
+        | AttributeNameExpected
+        | AttributeValueExpected
+        | EndOfTagExpected of string
+        | EOFExpected
+	| Empty
+
+type error = error_msg * error_pos
+
+exception Error of error
+
+exception File_not_found of string
+
+(** Get a full error message from an Xml error. *)
+val error : error -> string
+
+(** Get the Xml error message as a string. *)
+val error_msg : error_msg -> string 
+
+(** Get the line the error occured at. *)
+val line : error_pos -> int
+
+(** Get the relative character range (in current line) the error occured at.*)
+val range : error_pos -> int * int
+
+(** Get the absolute character range the error occured at. *)
+val abs_range : error_pos -> int * int
+
+val pos : Lexing.lexbuf -> error_pos
+
+(** Several kind of resources can contain Xml documents. *)
+type source = 
+	| SFile of string
+	| SChannel of in_channel
+	| SString of string
+	| SLexbuf of Lexing.lexbuf
+
+(** This function returns a new parser with default options. *)
+val make : unit -> t
+
+(** When a Xml document is parsed, the parser will check that the end of the
+ document is reached, so for example parsing ["<A/><B/>"] will fail instead
+ of returning only the A element. You can turn off this check by setting
+ [check_eof] to [false] {i (by default, check_eof is true)}. *)
+val check_eof : t -> bool -> unit
+
+(** Once the parser is configurated, you can run the parser on a any kind
+ of xml document source to parse its contents into an Xml data structure. *)
+val parse :  t -> source -> xml
diff --git a/lib/xml_utils.ml b/lib/xml_utils.ml
new file mode 100644
index 00000000..31003586
--- /dev/null
+++ b/lib/xml_utils.ml
@@ -0,0 +1,223 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+ *)
+
+open Printf
+open Xml_parser
+
+exception Not_element of xml
+exception Not_pcdata of xml
+exception No_attribute of string
+
+let default_parser = Xml_parser.make()
+
+let parse (p:Xml_parser.t) (source:Xml_parser.source) =
+	(* local cast Xml.xml -> xml *)
+	(Obj.magic Xml_parser.parse p source : xml)
+
+let parse_in ch = parse default_parser (Xml_parser.SChannel ch)
+let parse_string str = parse default_parser (Xml_parser.SString str)
+
+let parse_file f = parse default_parser (Xml_parser.SFile f)
+
+let tag = function
+	| Element (tag,_,_) -> tag
+	| x -> raise (Not_element x)
+
+let pcdata = function 
+	| PCData text -> text
+	| x -> raise (Not_pcdata x)
+
+let attribs = function 
+	| Element (_,attr,_) -> attr
+	| x -> raise (Not_element x)
+
+let attrib x att =
+	match x with
+	| Element (_,attr,_) ->
+		(try
+			let att = String.lowercase att in
+			snd (List.find (fun (n,_) -> String.lowercase n = att) attr)
+		with
+			Not_found ->
+				raise (No_attribute att))
+	| x ->
+		raise (Not_element x)
+
+let children = function
+	| Element (_,_,clist) -> clist
+	| x -> raise (Not_element x)
+
+(*let enum = function
+	| Element (_,_,clist) -> List.to_enum clist
+	| x -> raise (Not_element x)
+*)
+
+let iter f = function
+	| Element (_,_,clist) -> List.iter f clist
+	| x -> raise (Not_element x)
+
+let map f = function
+	| Element (_,_,clist) -> List.map f clist
+	| x -> raise (Not_element x)
+
+let fold f v = function
+	| Element (_,_,clist) -> List.fold_left f v clist
+	| x -> raise (Not_element x)
+
+let tmp = Buffer.create 200
+
+let buffer_pcdata text =
+	let l = String.length text in
+	for p = 0 to l-1 do 
+		match text.[p] with
+		| '>' -> Buffer.add_string tmp "&gt;"
+		| '<' -> Buffer.add_string tmp "&lt;"
+		| '&' ->
+			if p < l-1 && text.[p+1] = '#' then
+				Buffer.add_char tmp '&'
+			else
+				Buffer.add_string tmp "&amp;"
+		| '\'' -> Buffer.add_string tmp "&apos;"
+		| '"' -> Buffer.add_string tmp "&quot;"
+		| c -> Buffer.add_char tmp c
+	done
+
+let print_pcdata chan text =
+  let l = String.length text in
+  for p = 0 to l-1 do 
+    match text.[p] with
+    | '>' -> Printf.fprintf chan "&gt;"
+    | '<' -> Printf.fprintf chan "&lt;"
+    | '&' ->
+            if p < l-1 && text.[p+1] = '#' then
+                    Printf.fprintf chan "&"
+            else
+                    Printf.fprintf chan "&amp;"
+    | '\'' -> Printf.fprintf chan "&apos;"
+    | '"' -> Printf.fprintf chan "&quot;"
+    | c -> Printf.fprintf chan "%c" c
+  done
+
+let buffer_attr (n,v) =
+	Buffer.add_char tmp ' ';
+	Buffer.add_string tmp n;
+	Buffer.add_string tmp "=\"";
+	let l = String.length v in
+	for p = 0 to l-1 do
+		match v.[p] with
+		| '\\' -> Buffer.add_string tmp "\\\\"
+		| '"' -> Buffer.add_string tmp "\\\""
+		| c -> Buffer.add_char tmp c
+	done;
+	Buffer.add_char tmp '"'
+
+let rec print_attr chan (n, v) =
+  Printf.fprintf chan " %s=\"" n;
+  let l = String.length v in
+  for p = 0 to l-1 do
+          match v.[p] with
+          | '\\' -> Printf.fprintf chan "\\\\"
+          | '"' -> Printf.fprintf chan  "\\\""
+          | c -> Printf.fprintf chan "%c" c
+  done;
+  Printf.fprintf chan "\""
+
+let print_attrs chan l = List.iter (print_attr chan) l
+
+let rec print_xml chan = function
+| Element (tag, alist, []) ->
+  Printf.fprintf chan "<%s%a/>" tag print_attrs alist;
+| Element (tag, alist, l) ->
+  Printf.fprintf chan "<%s%a>%a</%s>" tag print_attrs alist
+  (fun chan -> List.iter (print_xml chan)) l tag
+| PCData text ->
+  print_pcdata chan text
+
+let to_string x = 
+	let pcdata = ref false in
+	let rec loop = function
+		| Element (tag,alist,[]) ->
+			Buffer.add_char tmp '<';
+			Buffer.add_string tmp tag;
+			List.iter buffer_attr alist;
+			Buffer.add_string tmp "/>";
+			pcdata := false;
+		| Element (tag,alist,l) ->
+			Buffer.add_char tmp '<';
+			Buffer.add_string tmp tag;
+			List.iter buffer_attr alist;
+			Buffer.add_char tmp '>';
+			pcdata := false;
+			List.iter loop l;
+			Buffer.add_string tmp "</";
+			Buffer.add_string tmp tag;
+			Buffer.add_char tmp '>';
+			pcdata := false;
+		| PCData text ->
+			if !pcdata then Buffer.add_char tmp ' ';
+			buffer_pcdata text;
+			pcdata := true;
+	in
+	Buffer.reset tmp;
+	loop x;
+	let s = Buffer.contents tmp in
+	Buffer.reset tmp;
+	s
+
+let to_string_fmt x =
+	let rec loop ?(newl=false) tab = function
+		| Element (tag,alist,[]) ->
+			Buffer.add_string tmp tab;
+			Buffer.add_char tmp '<';
+			Buffer.add_string tmp tag;
+			List.iter buffer_attr alist;
+			Buffer.add_string tmp "/>";
+			if newl then Buffer.add_char tmp '\n';
+		| Element (tag,alist,[PCData text]) ->
+			Buffer.add_string tmp tab;
+			Buffer.add_char tmp '<';
+			Buffer.add_string tmp tag;
+			List.iter buffer_attr alist;
+			Buffer.add_string tmp ">";
+			buffer_pcdata text;
+			Buffer.add_string tmp "</";
+			Buffer.add_string tmp tag;
+			Buffer.add_char tmp '>';
+			if newl then Buffer.add_char tmp '\n';
+		| Element (tag,alist,l) ->
+			Buffer.add_string tmp tab;
+			Buffer.add_char tmp '<';
+			Buffer.add_string tmp tag;
+			List.iter buffer_attr alist;
+			Buffer.add_string tmp ">\n";
+			List.iter (loop ~newl:true (tab^"  ")) l;
+			Buffer.add_string tmp tab;
+			Buffer.add_string tmp "</";
+			Buffer.add_string tmp tag;
+			Buffer.add_char tmp '>';
+			if newl then Buffer.add_char tmp '\n';
+		| PCData text ->
+			buffer_pcdata text;
+			if newl then Buffer.add_char tmp '\n';
+	in
+	Buffer.reset tmp;
+	loop "" x;
+	let s = Buffer.contents tmp in
+	Buffer.reset tmp;
+	s
diff --git a/lib/xml_utils.mli b/lib/xml_utils.mli
new file mode 100644
index 00000000..4a4a1309
--- /dev/null
+++ b/lib/xml_utils.mli
@@ -0,0 +1,93 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+ *)
+
+(** Xml Light
+ 
+  Xml Light is a minimal Xml parser & printer for OCaml.
+  It provide few functions to parse a basic Xml document into
+  an OCaml data structure and to print back the data structures
+  to an Xml document.
+
+  Xml Light has also support for {b DTD} (Document Type Definition).
+
+  {i (c)Copyright 2002-2003 Nicolas Cannasse}
+*)
+
+open Xml_parser
+
+(** {6 Xml Functions} *)
+
+exception Not_element of xml
+exception Not_pcdata of xml
+exception No_attribute of string
+
+(** [tag xdata] returns the tag value of the xml node.
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val tag : xml -> string
+
+(** [pcdata xdata] returns the PCData value of the xml node.
+ Raise {!Xml.Not_pcdata} if the xml is not a PCData *)
+val pcdata : xml -> string
+
+(** [attribs xdata] returns the attribute list of the xml node.
+ First string if the attribute name, second string is attribute value.
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val attribs : xml -> (string * string) list 
+
+(** [attrib xdata "href"] returns the value of the ["href"]
+ attribute of the xml node (attribute matching is case-insensitive).
+ Raise {!Xml.No_attribute} if the attribute does not exists in the node's
+ attribute list 
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val attrib : xml -> string -> string
+
+(** [children xdata] returns the children list of the xml node
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val children : xml -> xml list
+
+(*** [enum xdata] returns the children enumeration of the xml node
+ Raise {!Xml.Not_element} if the xml is not an element *)
+(* val enum : xml -> xml Enum.t *)
+
+(** [iter f xdata] calls f on all children of the xml node.
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val iter : (xml -> unit) -> xml -> unit
+
+(** [map f xdata] is equivalent to [List.map f (Xml.children xdata)]
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val map : (xml -> 'a) -> xml -> 'a list
+
+(** [fold f init xdata] is equivalent to
+ [List.fold_left f init (Xml.children xdata)]
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val fold : ('a -> xml -> 'a) -> 'a -> xml -> 'a
+
+(** {6 Xml Printing} *)
+
+(** Print the xml data structure to a channel into a compact xml string (without
+ any user-readable formating ). *)
+val print_xml : out_channel -> xml -> unit
+
+(** Print the xml data structure into a compact xml string (without
+ any user-readable formating ). *)
+val to_string : xml -> string
+
+(** Print the xml data structure into an user-readable string with
+ tabs and lines break between different nodes. *)
+val to_string_fmt : xml -> string