Imported Upstream version 8.0pl1upstream/8.0pl1

42 files changed, 4996 insertions, 0 deletions

diff --git a/lib/bignat.ml b/lib/bignat.ml
new file mode 100644
index 00000000..583a027f
--- /dev/null
+++ b/lib/bignat.ml
@@ -0,0 +1,116 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: bignat.ml,v 1.5.6.1 2004/07/16 19:30:29 herbelin Exp $ *)
+
+(*i*)
+open Pp
+(*i*)
+
+(* Arbitrary big natural numbers *)
+
+type bignat = int array
+
+let digits =            8
+let base =      100000000 (* let enough room for multiplication by 2 *)
+let base_div_2 = 50000000
+let base_to_string x = Printf.sprintf "%08d" x
+
+let of_string s =
+  let a = Array.create (String.length s / digits + 1) 0 in
+  let r = String.length s mod digits in
+  if r<>0 then a.(0) <- int_of_string (String.sub s 0 r);
+  for i = 1 to String.length s / digits do
+    a.(i) <- int_of_string (String.sub s ((i-1)*digits+r) digits)
+  done;
+  a
+
+let rec to_string s =
+  if s = [||] then "0" else
+    if s.(0) = 0 then to_string (Array.sub s 1 (Array.length s - 1))
+    else 
+      String.concat ""
+        ((string_of_int (s.(0)))
+        ::(List.tl (Array.to_list (Array.map base_to_string s))))
+  
+let is_nonzero a =
+  let b = ref false in Array.iter (fun x -> b := x <> 0 || !b) a; !b
+
+let zero = [|0|]
+let one = [|1|]
+
+let is_one a =
+  let rec leading_zero i = i<0 || (a.(i) = 0 && leading_zero (i-1)) in
+  (a.(Array.length a - 1) = 1) && leading_zero (Array.length a - 2)
+      
+let div2_with_rest n =
+  let len = Array.length n in
+  let q = Array.create len 0 in
+  for i = 0 to len - 2 do
+    q.(i) <- q.(i) + n.(i) / 2; q.(i + 1) <- base_div_2 * (n.(i) mod 2)
+  done;
+  q.(len - 1) <- q.(len - 1) + n.(len - 1) / 2;
+  q, (n.(len - 1) mod 2) = 1
+
+let add_1 n =
+  let m = Array.copy n
+  and i = ref (Array.length n - 1) in
+  while !i >= 0 && m.(!i) = base-1 do
+    m.(!i) <- 0; decr i; 
+  done;
+  if !i < 0 then begin
+    m.(0) <- 0; Array.concat [[| 1 |]; m] 
+  end else begin
+    m.(!i) <- m.(!i) + 1; m
+  end
+
+let sub_1 n =
+  if is_nonzero n then
+    let m = Array.copy n
+    and i = ref (Array.length n - 1) in
+    while m.(!i) = 0 && !i > 0 do
+      m.(!i) <- base-1; decr i;
+    done;
+    m.(!i) <- m.(!i) - 1;
+    m
+  else n
+
+let rec mult_2 n =
+  let m = Array.copy n in
+  m.(Array.length n - 1) <- 2 * m.(Array.length n - 1);
+  for i = Array.length n - 2 downto 0 do
+    m.(i) <- 2 * m.(i);
+    if m.(i + 1) >= base then begin
+      m.(i + 1) <- m.(i + 1) - base; m.(i) <- m.(i) + 1 
+    end
+  done;
+  if m.(0) >= base then begin
+    m.(0) <- m.(0) - base; Array.concat [[| 1 |]; m] 
+  end else 
+    m
+
+let less_than m n =
+  let lm = ref 0 in
+  while !lm < Array.length m && m.(!lm) = 0 do incr lm done;
+  let ln = ref 0 in
+  while !ln < Array.length n && n.(!ln) = 0 do incr ln done;
+  let um = Array.length m - !lm and un = Array.length n - !ln in
+  let rec lt d =
+    d < um && (m.(!lm+d) < n.(!ln+d) || (m.(!lm+d) = n.(!ln+d) && lt (d+1)))
+  in
+  (um < un) || (um = un && lt 0)
+
+type bigint = POS of bignat | NEG of bignat
+
+let pr_bigint = function
+  | POS n -> str (to_string n)
+  | NEG n -> str "-" ++ str (to_string n)
+
+let bigint_to_string = function
+  | POS n -> to_string n
+  | NEG n -> "-" ^ (to_string n);;
diff --git a/lib/bignat.mli b/lib/bignat.mli
new file mode 100644
index 00000000..f08ccc39
--- /dev/null
+++ b/lib/bignat.mli
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: bignat.mli,v 1.4.6.1 2004/07/16 19:30:29 herbelin Exp $ *)
+
+(*i*)
+open Pp
+(*i*)
+
+(* Arbitrary big natural numbers *)
+
+type bignat
+
+val of_string : string -> bignat
+val to_string : bignat -> string
+
+val is_nonzero : bignat -> bool
+val zero : bignat
+val one : bignat
+val is_one : bignat -> bool
+val div2_with_rest : bignat -> bignat * bool (* true=odd; false=even *)
+
+val add_1 : bignat -> bignat
+val sub_1 : bignat -> bignat (* Remark: (sub_1 0)=0 *)
+val mult_2 : bignat -> bignat
+
+val less_than : bignat -> bignat -> bool
+
+type bigint = POS of bignat | NEG of bignat
+
+val bigint_to_string : bigint -> string
+val pr_bigint : bigint -> std_ppcmds
diff --git a/lib/bstack.ml b/lib/bstack.ml
new file mode 100644
index 00000000..d4b995fb
--- /dev/null
+++ b/lib/bstack.ml
@@ -0,0 +1,63 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: bstack.ml,v 1.3.2.1 2004/07/16 19:30:29 herbelin Exp $ *)
+
+(* Queues of a given length *)
+
+open Util
+
+type 'a t = {mutable pos : int;
+             mutable size : int;
+             stack : 'a array}
+
+let create depth e =
+  {pos = 0;
+   size = 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.stack.(bs.pos) <- e
+	  
+let pop bs =
+  if bs.size > 1 then begin
+    bs.size <- bs.size - 1; 
+    let oldpos = bs.pos in
+    decr_pos bs;
+    (* Release the memory at oldpos, by coyping 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.size
diff --git a/lib/bstack.mli b/lib/bstack.mli
new file mode 100644
index 00000000..617f7df1
--- /dev/null
+++ b/lib/bstack.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: bstack.mli,v 1.4.2.1 2004/07/16 19:30:29 herbelin Exp $ 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
diff --git a/lib/compat.ml4 b/lib/compat.ml4
new file mode 100644
index 00000000..5e1c65b4
--- /dev/null
+++ b/lib/compat.ml4
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Compatibility file depending on ocaml version *)
+
+(* IFDEF not available in 3.06; use ifdef instead *)
+
+(* type loc is different in 3.08 *)
+ifdef OCAML308 then
+module M = struct
+type loc = Token.flocation
+let dummy_loc = Token.dummy_loc
+let unloc (b,e) = (b.Lexing.pos_cnum,e.Lexing.pos_cnum)
+let make_loc loc = Token.make_loc loc
+end
+else
+module M = struct
+type loc = int * int
+let dummy_loc = (0,0)
+let unloc x = x
+let make_loc x = x
+end
+
+type loc = M.loc
+let dummy_loc = M.dummy_loc
+let unloc = M.unloc
+let make_loc = M.make_loc
diff --git a/lib/doc.tex b/lib/doc.tex
new file mode 100644
index 00000000..35bd15fa
--- /dev/null
+++ b/lib/doc.tex
@@ -0,0 +1,7 @@
+
+\newpage
+\section*{Utility libraries}
+
+\ocwsection \label{lib}
+This chapter describes the various utility libraries used in the code
+of \Coq.
diff --git a/lib/dyn.ml b/lib/dyn.ml
new file mode 100644
index 00000000..63f00365
--- /dev/null
+++ b/lib/dyn.ml
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: dyn.ml,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ *)
+
+open Util
+
+(* Dynamics, programmed with DANGER !!! *)
+
+type t = string * Obj.t
+
+let dyntab = ref ([] : string list)
+
+let create s =
+  if List.mem s !dyntab then 
+    anomaly ("Dyn.create: already declared dynamic " ^ s);
+  dyntab := s :: !dyntab;
+  ((fun v -> (s,Obj.repr v)),
+   (fun (s',rv) ->
+      if s = s' then Obj.magic rv else failwith "dyn_out"))
+
+let tag (s,_) = s
diff --git a/lib/dyn.mli b/lib/dyn.mli
new file mode 100644
index 00000000..7f46c7e6
--- /dev/null
+++ b/lib/dyn.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: dyn.mli,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ i*)
+
+(* Dynamics. Use with extreme care. Not for kids. *)
+
+type t
+
+val create : string -> ('a -> t) * (t -> 'a)
+val tag : t -> string
diff --git a/lib/edit.ml b/lib/edit.ml
new file mode 100644
index 00000000..5020ef5c
--- /dev/null
+++ b/lib/edit.ml
@@ -0,0 +1,111 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: edit.ml,v 1.8.2.1 2004/07/16 19:30:29 herbelin Exp $ *)
+
+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 Bstack.depth bs = 1 & n > 0 then
+	  errorlabstrm "Edit.undo" (str"Undo stack exhausted");
+        repeat n Bstack.pop bs
+
+let create e (d,b,c,udepth) =
+  if Hashtbl.mem e.buf d then
+    errorlabstrm "Edit.create" 
+      (str"Already editing something of that name");
+  let bs = Bstack.create udepth 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
new file mode 100644
index 00000000..edf0f67b
--- /dev/null
+++ b/lib/edit.mli
@@ -0,0 +1,56 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: edit.mli,v 1.5.2.1 2004/07/16 19:30:29 herbelin Exp $ 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
diff --git a/lib/explore.ml b/lib/explore.ml
new file mode 100644
index 00000000..2eaabef8
--- /dev/null
+++ b/lib/explore.ml
@@ -0,0 +1,97 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: explore.ml,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ i*)
+
+open Format
+
+(*s Definition of a search problem. *)
+
+module type SearchProblem = sig
+  type state
+  val branching : state -> state list
+  val success : state -> bool
+  val pp : state -> unit
+end
+
+module Make = functor(S : SearchProblem) -> struct
+
+  type position = int list
+
+  let pp_position p = 
+    let rec pp_rec = function
+      | [] -> ()
+      | [i] -> printf "%d" i
+      | i :: l -> pp_rec l; printf ".%d" i
+    in
+    open_hbox (); pp_rec p; close_box ()
+
+  (*s Depth first search. *)
+
+  let rec depth_first s = 
+    if S.success s then s else depth_first_many (S.branching s)
+  and depth_first_many = function
+    | [] -> raise Not_found
+    | s :: l -> try depth_first s with Not_found -> depth_first_many l
+
+  let debug_depth_first s = 
+    let rec explore p s =
+      pp_position p; S.pp s;
+      if S.success s then s else explore_many 1 p (S.branching s)
+    and explore_many i p = function
+      | [] -> 
+	  raise Not_found
+      | s :: l -> 
+	  try explore (i::p) s with Not_found -> explore_many (succ i) p l
+    in
+    explore [1] s
+
+  (*s Breadth first search. We use functional FIFOS à la Okasaki. *)
+
+  type 'a queue = 'a list * 'a list
+
+  exception Empty
+
+  let empty = [],[]
+
+  let push x (h,t) = (x::h,t)
+
+  let pop = function
+    | h, x::t -> x, (h,t)
+    | h, [] -> match List.rev h with x::t -> x, ([],t) | [] -> raise Empty
+
+  let breadth_first s = 
+    let rec explore q =
+      try 
+	let (s, q') = pop q in enqueue q' (S.branching s)
+      with Empty ->
+	raise Not_found
+    and enqueue q = function
+      | [] -> explore q
+      | s :: l -> if S.success s then s else enqueue (push s q) l
+    in
+    enqueue empty [s]
+
+  let debug_breadth_first s = 
+    let rec explore q =
+      try 
+	let ((p,s), q') = pop q in 
+	enqueue 1 p q' (S.branching s)
+      with Empty ->
+	raise Not_found
+    and enqueue i p q = function
+      | [] -> 
+	  explore q
+      | s :: l ->
+	  let ps = i::p in 
+	  pp_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]
+
+end
diff --git a/lib/explore.mli b/lib/explore.mli
new file mode 100644
index 00000000..1236f06b
--- /dev/null
+++ b/lib/explore.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: explore.mli,v 1.2.16.1 2004/07/16 19:30:29 herbelin Exp $ i*)
+
+(*s Search strategies. *)
+
+(*s 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
+    recursively searched in the order they appear in the list.
+    [success] determines whether a given state is a success. 
+
+    [pp] is a pretty-printer for states used in debugging versions of the 
+    search functions. *)
+
+module type SearchProblem = sig
+
+  type state
+
+  val branching : state -> state list
+
+  val success : state -> bool
+
+  val pp : state -> unit
+
+end
+
+(*s 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).
+    Debugging versions of the search functions print the position of the
+    visited state together with the state it-self (using [S.pp]). *)
+
+module Make : functor(S : SearchProblem) -> sig
+
+  val depth_first : S.state -> S.state
+  val debug_depth_first : S.state -> S.state
+
+  val breadth_first : S.state -> S.state
+  val debug_breadth_first : S.state -> S.state
+
+end
diff --git a/lib/gmap.ml b/lib/gmap.ml
new file mode 100644
index 00000000..e5d41034
--- /dev/null
+++ b/lib/gmap.ml
@@ -0,0 +1,125 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(* $Id: gmap.ml,v 1.3.16.1 2004/07/16 19:30:29 herbelin Exp $ *)
+
+(* Maps using the generic comparison function of ocaml. Code borrowed from
+   the ocaml standard library. *)
+
+    type ('a,'b) t =
+        Empty
+      | Node of ('a,'b) t * 'a * 'b * ('a,'b) t * int
+
+    let empty = Empty
+
+    let height = function
+        Empty -> 0
+      | Node(_,_,_,_,h) -> h
+
+    let create l x d r =
+      let hl = height l and hr = height r in
+      Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
+
+    let bal l x d 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 "Map.bal"
+        | Node(ll, lv, ld, lr, _) ->
+            if height ll >= height lr then
+              create ll lv ld (create lr x d r)
+            else begin
+              match lr with
+                Empty -> invalid_arg "Map.bal"
+              | Node(lrl, lrv, lrd, lrr, _)->
+                  create (create ll lv ld lrl) lrv lrd (create lrr x d r)
+            end
+      end else if hr > hl + 2 then begin
+        match r with
+          Empty -> invalid_arg "Map.bal"
+        | Node(rl, rv, rd, rr, _) ->
+            if height rr >= height rl then
+              create (create l x d rl) rv rd rr
+            else begin
+              match rl with
+                Empty -> invalid_arg "Map.bal"
+              | Node(rll, rlv, rld, rlr, _) ->
+                  create (create l x d rll) rlv rld (create rlr rv rd rr)
+            end
+      end else
+        Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1))
+
+    let rec add x data = function
+        Empty ->
+          Node(Empty, x, data, Empty, 1)
+      | Node(l, v, d, r, h) as t ->
+          let c = Pervasives.compare x v in
+          if c = 0 then
+            Node(l, x, data, r, h)
+          else if c < 0 then
+            bal (add x data l) v d r
+          else
+            bal l v d (add x data r)
+
+    let rec find x = function
+        Empty ->
+          raise Not_found
+      | Node(l, v, d, r, _) ->
+          let c = Pervasives.compare x v in
+          if c = 0 then d
+          else find x (if c < 0 then l else r)
+
+    let rec mem x = function
+        Empty ->
+          false
+      | Node(l, v, d, r, _) ->
+          let c = Pervasives.compare x v in
+          c = 0 || mem x (if c < 0 then l else r)
+
+    let rec merge t1 t2 =
+      match (t1, t2) with
+        (Empty, t) -> t
+      | (t, Empty) -> t
+      | (Node(l1, v1, d1, r1, h1), Node(l2, v2, d2, r2, h2)) ->
+          bal l1 v1 d1 (bal (merge r1 l2) v2 d2 r2)
+
+    let rec remove x = function
+        Empty ->
+          Empty
+      | Node(l, v, d, r, h) as t ->
+          let c = Pervasives.compare x v in
+          if c = 0 then
+            merge l r
+          else if c < 0 then
+            bal (remove x l) v d r
+          else
+            bal l v d (remove x r)
+
+    let rec iter f = function
+        Empty -> ()
+      | Node(l, v, d, r, _) ->
+          iter f l; f v d; iter f r
+
+    let rec map f = function
+        Empty               -> Empty
+      | Node(l, v, d, r, h) -> Node(map f l, v, f d, map f r, h)
+
+    let rec fold f m accu =
+      match m with
+        Empty -> accu
+      | Node(l, v, d, r, _) ->
+          fold f l (f v d (fold f r accu))
+
+(* Added with respect to ocaml standard library. *)
+
+    let dom m = fold (fun x _ acc -> x::acc) m []
+
+    let rng m = fold (fun _ y acc -> y::acc) m []
+
+    let to_list m = fold (fun x y acc -> (x,y)::acc) m []
+
diff --git a/lib/gmap.mli b/lib/gmap.mli
new file mode 100644
index 00000000..7415a395
--- /dev/null
+++ b/lib/gmap.mli
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: gmap.mli,v 1.4.16.1 2004/07/16 19:30:29 herbelin Exp $ i*)
+
+(* Maps using the generic comparison function of ocaml. Same interface as
+   the module [Map] from the ocaml standard library. *)
+
+type ('a,'b) t
+
+val empty : ('a,'b) t
+val add : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
+val find : 'a -> ('a,'b) t -> 'b
+val remove : 'a -> ('a,'b) t -> ('a,'b) t
+val mem :  'a -> ('a,'b) t -> bool
+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. *)
+
+val dom : ('a,'b) t -> 'a list
+val rng : ('a,'b) t -> 'b list
+val to_list : ('a,'b) t -> ('a * 'b) list
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
new file mode 100644
index 00000000..dcb2eb94
--- /dev/null
+++ b/lib/gmapl.ml
@@ -0,0 +1,35 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: gmapl.ml,v 1.2.16.1 2004/07/16 19:30:29 herbelin Exp $ *)
+
+open Util
+
+type ('a,'b) t = ('a,'b list) Gmap.t
+
+let empty = Gmap.empty
+let mem = Gmap.mem
+let iter = Gmap.iter
+let map = Gmap.map
+let fold = Gmap.fold
+
+let add x y m =
+  try
+    let l = Gmap.find x m in
+    Gmap.add x (if List.mem y l then l else y::l) m
+  with Not_found ->
+    Gmap.add x [y] m
+
+let find x m =
+  try Gmap.find x m with Not_found -> []
+
+let remove x y m =
+  let l = Gmap.find x m in
+  Gmap.add x (if List.mem y l then list_subtract l [y] else l) m
+
+  
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
new file mode 100644
index 00000000..f8855ae4
--- /dev/null
+++ b/lib/gmapl.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: gmapl.mli,v 1.4.16.1 2004/07/16 19:30:30 herbelin Exp $ i*)
+
+(* Maps from ['a] to lists of ['b]. *)
+
+type ('a,'b) t
+
+val empty : ('a,'b) t
+val mem :  'a -> ('a,'b) t -> bool
+val iter : ('a -> 'b list -> unit) -> ('a,'b) t -> unit
+val map : ('b list -> 'c list) -> ('a,'b) t -> ('a,'c) t
+val fold : ('a -> 'b list -> 'c -> 'c) -> ('a,'b) t -> 'c -> 'c
+
+val add : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
+val find : 'a -> ('a,'b) t -> 'b list
+val remove : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
diff --git a/lib/gset.ml b/lib/gset.ml
new file mode 100644
index 00000000..5ea2f82b
--- /dev/null
+++ b/lib/gset.ml
@@ -0,0 +1,242 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: gset.ml,v 1.2.16.1 2004/07/16 19:30:30 herbelin Exp $ *)
+
+(* 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
new file mode 100644
index 00000000..32d798cc
--- /dev/null
+++ b/lib/gset.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: gset.mli,v 1.3.16.1 2004/07/16 19:30:30 herbelin Exp $ 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 -> 'a -> 'a) -> 'a t -> 'a -> 'a
+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
new file mode 100644
index 00000000..5f083459
--- /dev/null
+++ b/lib/hashcons.ml
@@ -0,0 +1,199 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: hashcons.ml,v 1.3.16.1 2004/07/16 19:30:30 herbelin Exp $ *)
+
+(* Hash consing of datastructures *)
+
+(* The generic hash-consing functions (does not use Obj) *)
+
+(* [t] is the type of object to hash-cons
+ * [u] is the type of hash-cons functions for the sub-structures
+ *   of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...).
+ * [hash_sub u x] is a function that hash-cons the sub-structures of x using
+ *   the hash-consing functions u provides.
+ * [equal] is a comparison function. It is allowed to use physical equality
+ *   on the sub-terms hash-consed by the hash_sub function.
+ * [hash] is the hash function given to the Hashtbl.Make function 
+ *
+ * Note that this module type coerces to the argument of Hashtbl.Make.
+ *)
+
+module type Comp =
+  sig
+    type t
+    type u
+    val hash_sub :  u -> t -> t
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
+(* The output is a function f such that
+ * [f ()] has the side-effect of creating (internally) a hash-table of the
+ *   hash-consed objects. The result is a function taking the sub-hashcons
+ *   functions and an object, and hashcons it. It does not really make sense
+ *   to call f() with different sub-hcons functions. That's why we use the
+ *   wrappers simple_hcons, recursive_hcons, ... The latter just take as
+ *   argument the sub-hcons functions (the tables are created at that moment),
+ *   and returns the hcons function for t.
+ *)
+
+module type S =
+  sig
+    type t
+    type u
+    val f : unit -> (u -> t -> t)
+  end
+
+module Make(X:Comp) =
+  struct
+    type t = X.t
+    type u = X.u
+
+    (* We create the type of hashtables for t, with our comparison fun.
+     * An invariant is that the table never contains two entries equals
+     * w.r.t (=), although the equality on keys is X.equal. This is
+     * granted since we hcons the subterms before looking up in the table.
+     *)
+    module Htbl = Hashtbl.Make(
+      struct type t=X.t
+             type u=X.u
+             let hash=X.hash
+             let equal x1 x2 = (*incr comparaison;*) X.equal x1 x2
+      end)
+
+    (* The table is created when () is applied.
+     * Hashconsing is then very simple:
+     *  1- hashcons the subterms using hash_sub and u
+     *  2- look up in the table, if we do not get a hit, we add it
+     *)
+    let f () =
+      let tab = Htbl.create 97 in
+        (fun u x ->
+           let y = X.hash_sub u x in
+            (* incr acces;*)
+             try let r = Htbl.find tab y in(* incr succes;*) r
+             with Not_found -> Htbl.add tab y y; y)
+  end
+
+(* A few usefull wrappers:
+ * takes as argument the function f above and build a function of type
+ * u -> t -> t that creates a fresh table each time it is applied to the
+ * sub-hcons functions. *)
+
+(* For non-recursive types it is quite easy. *)
+let simple_hcons h u = h () u
+
+(* For a recursive type T, we write the module of sig Comp with u equals
+ * to (T -> T) * u0
+ * The first component will be used to hash-cons the recursive subterms
+ * The second one to hashcons the other sub-structures.
+ * We just have to take the fixpoint of h
+ *)
+let recursive_hcons h u =
+  let hc = h () in
+  let rec hrec x = hc (hrec,u) x in
+  hrec
+
+(* If the structure may contain loops, use this one. *)
+let recursive_loop_hcons h u =
+  let hc = h () in
+  let rec hrec visited x =
+    if List.memq x visited then x
+    else hc (hrec (x::visited),u) x
+  in 
+  hrec []
+
+(* For 2 mutually recursive types *)
+let recursive2_hcons h1 h2 u1 u2 =
+  let hc1 = h1 () in
+  let hc2 = h2 () in
+  let rec hrec1 x = hc1 (hrec1,hrec2,u1) x
+  and hrec2 x = hc2 (hrec1,hrec2,u2) x
+  in (hrec1,hrec2)
+
+(* A set of global hashcons functions *)
+let hashcons_resets = ref []
+let init() = List.iter (fun f -> f()) !hashcons_resets
+
+(* [register_hcons h u] registers the hcons function h, result of the above
+ *   wrappers. It returns another hcons function that always uses the same
+ *   table, which can be reinitialized by init()
+ *)
+let register_hcons h u =
+  let hf = ref (h u) in
+  let reset() = hf := h u in
+  hashcons_resets := reset :: !hashcons_resets;
+  (fun x -> !hf x)
+
+(* Basic hashcons modules for string and obj. Integers do not need be
+   hashconsed.  *)
+
+(* string *)
+module Hstring = Make(
+  struct
+    type t = string
+    type u = unit
+    let hash_sub () s =(* incr accesstr;*) s
+    let equal s1 s2 =(* incr comparaisonstr;
+      if*) s1=s2(* then (incr successtr; true) else false*)
+    let hash = Hashtbl.hash
+  end)
+
+(* Obj.t *)
+exception NotEq
+
+(* From CAMLLIB/caml/mlvalues.h *)
+let no_scan_tag = 251
+let tuple_p obj = Obj.is_block obj & (Obj.tag obj < no_scan_tag)
+
+let comp_obj o1 o2 =
+  if tuple_p o1 & tuple_p o2 then
+    let n1 = Obj.size o1 and n2 = Obj.size o2 in
+      if n1=n2 then
+        try
+          for i = 0 to pred n1 do
+            if not (Obj.field o1 i == Obj.field o2 i) then raise NotEq
+          done; true
+        with NotEq -> false
+      else false
+  else o1=o2
+
+let hash_obj hrec o = 
+  begin
+    if tuple_p o then
+      let n = Obj.size o in
+        for i = 0 to pred n do
+          Obj.set_field o i (hrec (Obj.field o i))
+        done
+  end;
+  o
+
+module Hobj = Make(
+  struct
+    type t = Obj.t
+    type u = (Obj.t -> Obj.t) * unit
+    let hash_sub (hrec,_) = hash_obj hrec
+    let equal = comp_obj
+    let hash = Hashtbl.hash
+  end)
+
+(* Hashconsing functions for string and obj. Always use the same
+ * global tables. The latter can be reinitialized with init()
+ *)
+(* string : string -> string *)
+(* obj : Obj.t -> Obj.t *)
+let string = register_hcons (simple_hcons Hstring.f) ()
+let obj = register_hcons (recursive_hcons Hobj.f) ()
+
+(* The unsafe polymorphic hashconsing function *)
+let magic_hash (c : 'a) =
+  init();
+  let r = obj (Obj.repr c) in
+  init();
+  (Obj.magic r : 'a)
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
new file mode 100644
index 00000000..2e32323a
--- /dev/null
+++ b/lib/hashcons.mli
@@ -0,0 +1,52 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: hashcons.mli,v 1.5.16.1 2004/07/16 19:30:30 herbelin Exp $ i*)
+
+(* Generic hash-consing. *)
+
+module type Comp =
+  sig
+    type t
+    type u
+    val hash_sub :  u -> t -> t
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
+module type S =
+  sig
+    type t
+    type u
+    val f : unit -> (u -> t -> t)
+  end
+
+module Make(X:Comp) : (S with type t = X.t and type u = X.u)
+
+val simple_hcons : (unit -> 'u -> 't -> 't) -> ('u -> 't -> 't)
+val recursive_hcons : (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
+val recursive_loop_hcons :
+    (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
+val recursive2_hcons :
+  (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u1 -> 't1 -> 't1) ->
+    (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u2 -> 't2 -> 't2) ->
+      'u1 -> 'u2 -> ('t1 -> 't1) * ('t2 -> 't2)
+
+(* Declaring and reinitializing global hash-consing functions *)
+
+val init : unit -> unit
+val register_hcons : ('u -> 't -> 't) -> ('u -> 't -> 't)
+
+module Hstring : (S with type t = string and type u = unit)
+module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit)
+
+val string : string -> string
+val obj : Obj.t -> Obj.t
+
+val magic_hash : 'a -> 'a
+
diff --git a/lib/heap.ml b/lib/heap.ml
new file mode 100644
index 00000000..f0db2943
--- /dev/null
+++ b/lib/heap.ml
@@ -0,0 +1,153 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: heap.ml,v 1.1.2.1 2004/07/16 19:30:30 herbelin Exp $ *)
+
+(*s Heaps *)
+
+module type Ordered = sig
+  type t
+  val compare : t -> t -> int
+end
+
+module type S =sig
+  
+  (* Type of functional heaps *)
+  type t
+
+  (* Type of elements *)
+  type elt
+    
+  (* The empty heap *)
+  val empty : t
+    
+  (* [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)$ *)
+  val maximum : t -> elt
+    
+  (* [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))$ *) 
+  val remove : t -> t
+    
+  (* usual iterators and combinators; elements are presented in
+     arbitrary order *)
+  val iter : (elt -> unit) -> t -> unit
+    
+  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+    
+end
+
+exception EmptyHeap
+
+(*s Functional implementation *)
+
+module Functional(X : Ordered) = struct
+
+  (* Heaps are encoded as complete binary trees, i.e., binary trees
+     which are full expect, may be, on the bottom level where it is filled 
+     from the left. 
+     These trees also enjoy the heap property, namely the value of any node 
+     is greater or equal than those of its left and right subtrees.
+
+     There are 4 kinds of complete binary trees, denoted by 4 constructors:
+     [FFF] for a full binary tree (and thus 2 full subtrees);
+     [PPF] for a partial tree with a partial left subtree and a full
+     right subtree;
+     [PFF] for a partial tree with a full left subtree and a full right subtree
+     (but of different heights);
+     and [PFP] for a partial tree with a full left subtree and a partial
+     right subtree. *)
+
+  type t = 
+    | Empty
+    | FFF of t * X.t * t (* full    (full,    full) *)
+    | PPF of t * X.t * t (* partial (partial, full) *)
+    | PFF of t * X.t * t (* partial (full,    full) *)
+    | PFP of t * X.t * t (* partial (full,    partial) *)
+
+  type elt = X.t
+
+  let empty = Empty
+ 
+  (* smart constructors for insertion *)
+  let p_f l x r = match l with
+    | Empty | FFF _ -> PFF (l, x, r)
+    | _ -> PPF (l, x, r)
+
+  let pf_ l x = function
+    | Empty | FFF _ as r -> FFF (l, x, r)
+    | r -> PFP (l, x, r)
+
+  let rec add x = function
+    | Empty -> 
+	FFF (Empty, x, Empty)
+    (* insertion to the left *)
+    | FFF (l, y, r) | PPF (l, y, r) ->
+	if X.compare x y > 0 then p_f (add y l) x r else p_f (add x l) y r
+    (* insertion to the right *)
+    | PFF (l, y, r) | PFP (l, y, r) ->
+	if X.compare x y > 0 then pf_ l x (add y r) else pf_ l y (add x r)
+
+  let maximum = function
+    | Empty -> raise EmptyHeap
+    | FFF (_, x, _) | PPF (_, x, _) | PFF (_, x, _) | PFP (_, x, _) -> x
+
+  (* smart constructors for removal; note that they are different
+     from the ones for insertion! *)
+  let p_f l x r = match l with
+    | Empty | FFF _ -> FFF (l, x, r)
+    | _ -> PPF (l, x, r)
+
+  let pf_ l x = function
+    | Empty | FFF _ as r -> PFF (l, x, r)
+    | r -> PFP (l, x, r)
+
+  let rec remove = function
+    | Empty -> 
+	raise EmptyHeap
+    | FFF (Empty, _, Empty) -> 
+	Empty
+    | PFF (l, _, Empty) ->
+	l
+    (* remove on the left *)
+    | PPF (l, x, r) | PFF (l, x, r) ->
+        let xl = maximum l in
+	let xr = maximum r in
+	let l' = remove l in
+	if X.compare xl xr >= 0 then 
+	  p_f l' xl r 
+	else 
+	  p_f l' xr (add xl (remove r))
+    (* remove on the right *)
+    | FFF (l, x, r) | PFP (l, x, r) ->
+        let xl = maximum l in
+	let xr = maximum r in
+	let r' = remove r in
+	if X.compare xl xr > 0 then 
+	  pf_ (add xr (remove l)) xl r'
+	else 
+	  pf_ l xr r'
+
+  let rec iter f = function
+    | Empty -> 
+	()
+    | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) -> 
+	iter f l; f x; iter f r
+
+  let rec fold f h x0 = match h with
+    | Empty -> 
+	x0
+    | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) -> 
+	fold f l (fold f r (f x x0))
+
+end
diff --git a/lib/heap.mli b/lib/heap.mli
new file mode 100644
index 00000000..c865461e
--- /dev/null
+++ b/lib/heap.mli
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: heap.mli,v 1.1.2.1 2004/07/16 19:30:30 herbelin Exp $ *)
+
+(* Heaps *)
+
+module type Ordered = sig
+  type t
+  val compare : t -> t -> int
+end
+
+module type S =sig
+  
+  (* Type of functional heaps *)
+  type t
+
+  (* Type of elements *)
+  type elt
+    
+  (* The empty heap *)
+  val empty : t
+    
+  (* [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)$ *)
+  val maximum : t -> elt
+    
+  (* [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))$ *) 
+  val remove : t -> t
+    
+  (* usual iterators and combinators; elements are presented in
+     arbitrary order *)
+  val iter : (elt -> unit) -> t -> unit
+    
+  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+    
+end
+
+exception EmptyHeap
+
+(*S Functional implementation. *)
+
+module Functional(X: Ordered) : S with type elt=X.t
diff --git a/lib/options.ml b/lib/options.ml
new file mode 100644
index 00000000..b5c5efda
--- /dev/null
+++ b/lib/options.ml
@@ -0,0 +1,107 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: options.ml,v 1.27.2.1 2004/07/16 19:30:30 herbelin Exp $ *)
+
+open Util
+
+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
+
+let boot = ref false
+
+let batch_mode = ref false
+
+let debug = ref false
+
+let print_emacs = ref false
+
+let emacs_str s = if !print_emacs then s else "" 
+
+let term_quality = ref false
+
+let xml_export = ref false
+
+let dont_load_proofs = ref false
+
+let raw_print = ref false
+
+let v7 =
+  let transl = array_exists ((=) "-translate") Sys.argv in
+  let v7 = array_exists ((=) "-v7") Sys.argv in
+  let v8 = array_exists ((=) "-v8") Sys.argv in
+  if v8 & transl then error "Options -translate and -v8 are incompatible";
+  if v8 & v7 then error "Options -v7 and -v8 are incompatible";
+  ref (v7 or transl)
+
+let v7_only = ref false
+
+(* Translate *)
+let translate = ref false
+let make_translate f = translate := f; v7 := f; ()
+let do_translate () = !translate
+let translate_file = ref false
+let translate_strict_impargs = ref true
+
+(* True only when interning from pp*new.ml *)
+let translate_syntax = ref false
+
+(* Silent / Verbose *)
+let silent = ref false
+let make_silent flag = silent := flag; ()
+let is_silent () = !silent
+let is_verbose () = not !silent
+
+let silently f x =
+  let oldsilent = !silent in
+  try 
+    silent := true;
+    let rslt = f x in
+    silent := oldsilent; 
+    rslt
+  with e -> begin
+    silent := oldsilent; raise e
+  end
+
+let if_silent f x = if !silent then f x
+let if_verbose f x = if not !silent then f x
+
+(* The number of printed hypothesis in a goal *)
+
+let print_hyps_limit = ref (None : int option)
+let set_print_hyps_limit n = print_hyps_limit := n
+let print_hyps_limit () = !print_hyps_limit
+
+(* A list of the areas of the system where "unsafe" operation
+ * has been requested *)
+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
+
+
+(* Dump of globalization (to be used by coqdoc) *)
+
+let dump = ref false
+let dump_file = ref ""
+let dump_into_file f = dump := true; dump_file := f
+
+let dump_buffer = Buffer.create 8192
+
+let dump_string = Buffer.add_string dump_buffer
+
+let dump_it () = 
+  if !dump then begin
+    let mode = [Open_wronly; Open_append; Open_creat] in
+    let c = open_out_gen mode 0o666 !dump_file in
+    output_string c (Buffer.contents dump_buffer);
+    close_out c
+  end
+
+let _ = at_exit dump_it
diff --git a/lib/options.mli b/lib/options.mli
new file mode 100644
index 00000000..731b7da4
--- /dev/null
+++ b/lib/options.mli
@@ -0,0 +1,62 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: options.mli,v 1.25.2.1 2004/07/16 19:30:30 herbelin Exp $ i*)
+
+(* Global options of the system. *)
+
+val boot : bool ref
+
+val batch_mode : bool ref
+
+val debug : bool ref
+
+val print_emacs : bool ref
+val emacs_str : string -> string
+
+val term_quality : bool ref
+
+val xml_export : bool ref
+
+val dont_load_proofs : bool ref
+
+val raw_print : bool ref
+
+val v7 : bool ref
+val v7_only : bool ref
+
+val translate : bool ref
+val make_translate : bool -> unit
+val do_translate : unit -> bool
+val translate_file : bool ref
+val translate_syntax : bool ref
+val translate_strict_impargs : bool ref
+
+val make_silent : bool -> unit
+val is_silent : unit -> bool
+val is_verbose : unit -> bool
+val silently : ('a -> 'b) -> 'a -> 'b
+val if_silent : ('a -> unit) -> 'a -> unit
+val if_verbose : ('a -> unit) -> 'a -> unit
+
+(* Temporary activate an option ('c must be an atomic type) *)
+val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
+
+(* 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
+
+(* Dump of globalization (to be used by coqdoc) *)
+
+val dump : bool ref
+val dump_into_file : string -> unit
+val dump_string : string -> unit
+
diff --git a/lib/pp.ml4 b/lib/pp.ml4
new file mode 100644
index 00000000..25ab9ce8
--- /dev/null
+++ b/lib/pp.ml4
@@ -0,0 +1,287 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: pp.ml4,v 1.5.2.1 2004/07/16 19:30:30 herbelin Exp $ *)
+
+open Pp_control
+
+(* The different kinds of blocks are: 
+   \begin{description}
+   \item[hbox:] Horizontal block no line breaking;
+   \item[vbox:] Vertical block each break leads to a new line;
+   \item[hvbox:] Horizontal-vertical block: same as vbox, except if
+      this block is small enough to fit on a single line
+   \item[hovbox:] Horizontal or Vertical block: breaks lead to new line
+      only when necessary to print the content of the block
+   \item[tbox:] Tabulation block: go to tabulation marks and no line breaking
+      (except if no mark yet on the reste of the line)
+   \end{description}
+ *)
+ 
+let comments = ref []
+  
+let rec split_com comacc acc pos = function
+    [] -> comments := List.rev acc; comacc
+  | ((b,e),c as com)::coms ->
+      (* Take all comments that terminates before pos, or begin exactly
+         at pos (used to print comments attached after an expression) *)
+      if e<=pos || pos=b then split_com (c::comacc) acc pos coms
+      else  split_com comacc (com::acc) pos coms
+
+
+type block_type =
+  | Pp_hbox of int
+  | Pp_vbox of int
+  | Pp_hvbox of int
+  | Pp_hovbox of int
+  | Pp_tbox
+
+type 'a ppcmd_token =
+  | Ppcmd_print of 'a
+  | Ppcmd_box of block_type * ('a ppcmd_token Stream.t)
+  | Ppcmd_print_break of int * int
+  | Ppcmd_set_tab
+  | Ppcmd_print_tbreak of int * int
+  | Ppcmd_white_space of int
+  | Ppcmd_force_newline
+  | Ppcmd_print_if_broken
+  | Ppcmd_open_box of block_type
+  | Ppcmd_close_box
+  | Ppcmd_close_tbox
+  | Ppcmd_comment of int
+
+type 'a ppdir_token =
+  | Ppdir_ppcmds of 'a ppcmd_token Stream.t
+  | Ppdir_print_newline
+  | Ppdir_print_flush
+
+type ppcmd = (int*string) ppcmd_token
+
+type std_ppcmds = ppcmd Stream.t
+
+type 'a ppdirs = 'a ppdir_token Stream.t
+
+(* Compute length of an UTF-8 encoded string
+   Rem 1 : utf8_length <= String.length (equal if pure ascii)
+   Rem 2 : if used for an iso8859_1 encoded string, the result is
+   wrong in very rare cases. Such a wrong case corresponds to any
+   sequence of a character in range 192..253 immediately followed by a
+   character in range 128..191 (typical case in french is "déçu" which
+   is counted 3 instead of 4); then no real harm to use always
+   utf8_length even if using an iso8859_1 encoding *)
+
+let utf8_length s =
+  let len = String.length s
+  and cnt = ref 0
+  and nc = ref 0
+  and p = ref 0 in
+  while !p < len do
+    begin
+      match s.[!p] with
+      | '\000'..'\127' -> nc := 0 (* ascii char *)
+      | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *)
+      |	'\192'..'\223' -> nc := 1 (* expect 1 continuation byte *)
+      |	'\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *)
+      |	'\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *)
+      |	'\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *)
+      |	'\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *)
+      |	'\254'..'\255' -> nc := 0 (* invalid byte *)
+    end ;
+    incr p ;
+    while !p < len && !nc > 0 do
+      match s.[!p] with
+      |	'\128'..'\191' (* next continuation byte *) -> incr p ; decr nc
+      |	_ (* not a continuation byte *) -> nc := 0
+    done ;
+    incr cnt
+  done ;
+  !cnt
+
+(* formatting commands *)
+let str s = [< 'Ppcmd_print (utf8_length s,s) >]
+let stras (i,s) = [< 'Ppcmd_print (i,s) >]
+let brk (a,b) = [< 'Ppcmd_print_break (a,b) >]
+let tbrk (a,b) = [< 'Ppcmd_print_tbreak (a,b) >]
+let tab () = [< 'Ppcmd_set_tab >]
+let fnl () = [< 'Ppcmd_force_newline >]
+let pifb () = [< 'Ppcmd_print_if_broken >]
+let ws n = [< 'Ppcmd_white_space n >]
+let comment n = [< ' Ppcmd_comment n >]
+
+(* derived commands *)
+let mt () = [< >]
+let spc () = [< 'Ppcmd_print_break (1,0) >]
+let cut () = [< 'Ppcmd_print_break (0,0) >]
+let align () = [< 'Ppcmd_print_break (0,0) >]
+let int n = str (string_of_int n)
+let real r = str (string_of_float r)
+let bool b = str (string_of_bool b)
+
+let rec escape_string s =
+  let rec escape_at s i =
+    if i<0 then s
+    else if s.[i] == '\\' || s.[i] == '"' then
+      let s' = String.sub s 0 i^"\\"^String.sub s i (String.length s - i) in
+      escape_at s' (i-1)
+    else escape_at s (i-1) in
+  escape_at s (String.length s - 1)
+
+
+let qstring s = str ("\""^(escape_string s)^"\"")
+let qs = qstring
+
+(* boxing commands *)
+let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >]
+let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >]
+let hv n s = [< 'Ppcmd_box(Pp_hvbox n,s) >]
+let hov n s = [< 'Ppcmd_box(Pp_hovbox n,s) >]
+let t s = [< 'Ppcmd_box(Pp_tbox,s) >]
+
+(* Opening and closing of boxes *)
+let hb n = [< 'Ppcmd_open_box(Pp_hbox n) >]
+let vb n = [< 'Ppcmd_open_box(Pp_vbox n) >]
+let hvb n = [< 'Ppcmd_open_box(Pp_hvbox n) >]
+let hovb n = [< 'Ppcmd_open_box(Pp_hovbox n) >]
+let tb () = [< 'Ppcmd_open_box Pp_tbox >]
+let close () = [< 'Ppcmd_close_box >]
+let tclose () = [< 'Ppcmd_close_tbox >]
+
+let (++) = Stream.iapp
+
+(* This flag tells if the last printed comment ends with a newline, to
+  avoid empty lines *)
+let com_eol = ref false
+
+let com_brk ft = com_eol := false
+let com_if ft f =
+  if !com_eol then (com_eol := false; Format.pp_force_newline ft ())
+  else Lazy.force f
+
+let rec pr_com ft s =
+  let (s1,os) =
+    try
+      let n = String.index s '\n' in
+      String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1))
+    with Not_found -> s,None in
+  com_if ft (Lazy.lazy_from_val());
+(*  let s1 =
+    if String.length s1 <> 0 && s1.[0] = ' ' then
+      (Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1))
+    else s1 in*)
+  Format.pp_print_as ft (utf8_length s1) s1;
+  match os with
+      Some s2 ->
+        if String.length s2 = 0 then (com_eol := true)
+        else
+          (Format.pp_force_newline ft (); pr_com ft s2)
+    | None -> ()
+
+(* pretty printing functions *)
+let pp_dirs ft = 
+  let maxbox = (get_gp ft).max_depth in
+  let pp_open_box = function
+    | Pp_hbox n   -> Format.pp_open_hbox ft ()
+    | Pp_vbox n   -> Format.pp_open_vbox ft n
+    | Pp_hvbox n  -> Format.pp_open_hvbox ft n
+    | Pp_hovbox n -> Format.pp_open_hovbox ft n
+    | Pp_tbox     -> Format.pp_open_tbox ft () 
+  in
+  let rec pp_cmd = function
+    | Ppcmd_print(n,s)        ->
+        com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s
+    | Ppcmd_box(bty,ss)       -> (* Prevent evaluation of the stream! *)
+        com_if ft (Lazy.lazy_from_val());
+        pp_open_box bty ;
+        if not (Format.over_max_boxes ()) then Stream.iter pp_cmd ss;
+        Format.pp_close_box ft ()
+    | Ppcmd_open_box bty      -> com_if ft (Lazy.lazy_from_val()); pp_open_box bty
+    | Ppcmd_close_box         -> Format.pp_close_box ft ()
+    | Ppcmd_close_tbox        -> Format.pp_close_tbox ft ()
+    | Ppcmd_white_space n     ->
+        com_if ft (Lazy.lazy_from_fun (fun()->Format.pp_print_break ft n 0))
+    | Ppcmd_print_break(m,n)  ->
+        com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_break ft m n))
+    | Ppcmd_set_tab           -> Format.pp_set_tab ft ()
+    | Ppcmd_print_tbreak(m,n) ->
+        com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_tbreak ft m n))
+    | Ppcmd_force_newline     ->
+        com_brk ft; Format.pp_force_newline ft ()
+    | Ppcmd_print_if_broken   ->
+        com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_if_newline ft ()))
+    | Ppcmd_comment i         ->
+        let coms = split_com [] [] i !comments in
+(*        Format.pp_open_hvbox ft 0;*)
+        List.iter (pr_com ft) coms(*;
+        Format.pp_close_box ft ()*)
+  in
+  let pp_dir = function
+    | Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream
+    | Ppdir_print_newline    ->
+        com_brk ft; Format.pp_print_newline ft ()
+    | Ppdir_print_flush      -> Format.pp_print_flush ft () 
+  in
+  fun dirstream ->
+    try  
+      Stream.iter pp_dir dirstream; com_brk ft
+    with 
+      | e -> Format.pp_print_flush ft () ; raise e
+
+
+(* 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
+
+(* pretty printing functions WITHOUT FLUSH *)
+let pp_with ft strm =
+  pp_dirs ft [< 'Ppdir_ppcmds strm >]
+
+let ppnl_with ft strm =
+  pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >]
+
+let warning_with ft string =
+  ppnl_with ft [< str "Warning: " ; str string >]
+
+let warn_with ft pps =
+  ppnl_with ft [< str "Warning: " ; pps >]
+
+let pp_flush_with ft =
+  Format.pp_print_flush ft
+
+
+(* pretty printing functions WITH FLUSH *)
+let msg_with ft strm =
+  pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_flush >]
+
+let msgnl_with ft strm =
+  pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >]
+
+let msg_warning_with ft strm=
+  pp_dirs ft [< 'Ppdir_ppcmds [< str "Warning: "; strm>]; 
+		'Ppdir_print_newline >]
+
+
+(* pretty printing functions WITHOUT FLUSH *)
+let pp        x = pp_with !std_ft x
+let ppnl      x = ppnl_with !std_ft x
+let pperr     = pp_with err_ft
+let pperrnl   = ppnl_with err_ft
+let message s = ppnl (str s)
+let warning   x = warning_with err_ft x
+let warn      x = warn_with err_ft x
+let pp_flush  x = Format.pp_print_flush !std_ft x
+let flush_all() = flush stderr; flush stdout; pp_flush()
+
+(* pretty printing functions WITH FLUSH *)
+let msg x = msg_with !std_ft x
+let msgnl x = msgnl_with !std_ft x
+let msgerr = msg_with err_ft
+let msgerrnl = msgnl_with err_ft
+let msg_warning x = msg_warning_with err_ft x
diff --git a/lib/pp.mli b/lib/pp.mli
new file mode 100644
index 00000000..417ea107
--- /dev/null
+++ b/lib/pp.mli
@@ -0,0 +1,104 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: pp.mli,v 1.8.2.1 2004/07/16 19:30:30 herbelin Exp $ i*)
+
+(*i*)
+open Pp_control
+(*i*)
+
+(* Pretty-printers. *)
+
+type ppcmd
+
+type std_ppcmds = ppcmd Stream.t
+
+(*s Formatting commands. *)
+
+val str  : string -> std_ppcmds
+val stras : int * string -> std_ppcmds
+val brk : int * int -> std_ppcmds
+val tbrk : int * int -> std_ppcmds
+val tab : unit -> std_ppcmds
+val fnl : unit -> std_ppcmds
+val pifb : unit -> std_ppcmds
+val ws : int -> std_ppcmds
+val mt : unit -> std_ppcmds
+
+val comment : int -> std_ppcmds
+val comments : ((int * int) * string) list ref
+
+(*s Concatenation. *)
+
+val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
+
+(*s Derived commands. *)
+
+val spc : unit -> std_ppcmds
+val cut : unit -> std_ppcmds
+val align : unit -> std_ppcmds
+val int : int -> std_ppcmds
+val real : float -> std_ppcmds
+val bool : bool -> std_ppcmds
+val qstring : string -> std_ppcmds
+val qs : string -> std_ppcmds
+
+(*s Boxing commands. *)
+
+val h : int -> std_ppcmds -> std_ppcmds
+val v : int -> std_ppcmds -> std_ppcmds
+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. *)
+
+val hb : int -> std_ppcmds
+val vb : int -> std_ppcmds
+val hvb : int -> std_ppcmds
+val hovb : int -> std_ppcmds
+val tb : unit -> std_ppcmds
+val close : unit -> std_ppcmds
+val tclose : unit -> std_ppcmds
+
+(*s Pretty-printing functions \emph{without flush}. *)
+
+val pp_with : Format.formatter -> std_ppcmds -> unit
+val ppnl_with : Format.formatter -> std_ppcmds -> unit
+val warning_with : Format.formatter -> string -> unit
+val warn_with : Format.formatter -> std_ppcmds -> unit
+val pp_flush_with : Format.formatter -> unit -> unit
+
+(*s 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
+  [std_ft] and [err_ft]. *)
+
+(*s 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 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]. *)
+
+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
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
new file mode 100644
index 00000000..85303f74
--- /dev/null
+++ b/lib/pp_control.ml
@@ -0,0 +1,108 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: pp_control.ml,v 1.8.2.1 2004/07/16 19:30:31 herbelin Exp $ *)
+
+(* Parameters of pretty-printing *)
+
+type pp_global_params = {
+  margin : int;
+  max_indent : int;
+  max_depth : int;
+  ellipsis : string }
+
+(* Default parameters of pretty-printing *)
+
+let dflt_gp = { 
+  margin     = 78;
+  max_indent = 50;
+  max_depth  = 50;
+  ellipsis   = ".." }
+
+(* A deeper pretty-printer to print proof scripts *)
+
+let deep_gp = { 
+  margin     = 78;
+  max_indent = 50;
+  max_depth  = 10000;
+  ellipsis   = "..." }
+
+(* set_gp : Format.formatter -> pp_global_params -> unit
+ * set the parameters of a formatter *)
+
+let set_gp ft gp = 
+  Format.pp_set_margin ft gp.margin ;
+  Format.pp_set_max_indent ft gp.max_indent ;
+  Format.pp_set_max_boxes ft gp.max_depth ;
+  Format.pp_set_ellipsis_text ft gp.ellipsis
+
+let set_dflt_gp ft = set_gp ft dflt_gp 
+
+let get_gp ft =
+  { margin = Format.pp_get_margin ft ();
+    max_indent = Format.pp_get_max_indent 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;
+  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
+  set_gp ft deep_gp; 
+  ft
+
+let std_ft = ref Format.std_formatter
+let _ = set_dflt_gp !std_ft
+
+let err_ft = with_output_to stderr
+
+let deep_ft = with_output_to stdout
+let _ = set_gp deep_ft deep_gp
+
+(* For parametrization through vernacular *)
+let default = Format.pp_get_max_boxes !std_ft ()
+let default_margin = Format.pp_get_margin !std_ft ()
+
+let get_depth_boxes () = Some (Format.pp_get_max_boxes !std_ft ())
+let set_depth_boxes v =
+  Format.pp_set_max_boxes !std_ft (match v with None -> default | Some v -> v)
+
+let get_margin () = Some (Format.pp_get_margin !std_ft ())
+let set_margin v =
+  Format.pp_set_margin !std_ft (match v with None -> default_margin | Some v -> v)
+
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
new file mode 100644
index 00000000..3588847d
--- /dev/null
+++ b/lib/pp_control.mli
@@ -0,0 +1,49 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: pp_control.mli,v 1.7.2.1 2004/07/16 19:30:31 herbelin Exp $ i*)
+
+(* Parameters of pretty-printing. *)
+
+type pp_global_params = { 
+  margin : int;
+  max_indent : int;
+  max_depth : int;
+  ellipsis : string }
+
+val dflt_gp : pp_global_params
+val deep_gp : pp_global_params
+val set_gp : Format.formatter -> pp_global_params -> unit
+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
+
+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
+val deep_ft : Format.formatter
+
+(*s For parametrization through vernacular. *)
+
+val set_depth_boxes : int option -> unit
+val get_depth_boxes : unit -> int option
+
+val set_margin : int option -> unit
+val get_margin : unit -> int option
diff --git a/lib/predicate.ml b/lib/predicate.ml
new file mode 100644
index 00000000..1eaa20ce
--- /dev/null
+++ b/lib/predicate.ml
@@ -0,0 +1,99 @@
+(************************************************************************)
+(*                                                                     *)
+(*                           Objective Caml                            *)
+(*                                                                     *)
+(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
+(*                                                                     *)
+(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
+(*  en Automatique.  All rights reserved.  This file is distributed    *)
+(*  under the terms of the GNU Library General Public License.         *)
+(*                                                                     *)
+(************************************************************************)
+
+(* $Id: predicate.ml,v 1.1.14.1 2004/07/16 19:30:31 herbelin Exp $ *)
+
+(* Sets over ordered types *)
+
+module type OrderedType =
+  sig
+    type t
+    val compare: t -> t -> int
+  end
+
+module type S =
+  sig
+    type elt
+    type t
+    val empty: t
+    val full: t
+    val is_empty: t -> bool
+    val is_full: t -> bool
+    val mem: elt -> t -> bool
+    val singleton: elt -> t
+    val add: elt -> t -> t
+    val remove: elt -> t -> t
+    val union: t -> t -> t
+    val inter: t -> t -> t
+    val diff: t -> t -> t
+    val complement: t -> t
+    val equal: t -> t -> bool
+    val subset: t -> t -> bool
+    val elements: t -> bool * elt list
+  end
+
+module Make(Ord: OrderedType) =
+  struct
+    module EltSet = Set.Make(Ord)
+ 
+    (* when bool is false, the denoted set is the complement of
+       the given set *)
+    type elt = Ord.t
+    type t = bool * EltSet.t
+
+    let elements (b,s) = (b, EltSet.elements s)
+
+    let empty = (false,EltSet.empty)
+    let full = (true,EltSet.empty)
+
+    (* assumes the set is infinite *)
+    let is_empty (b,s) = not b & EltSet.is_empty s
+    let is_full (b,s) = b & EltSet.is_empty s
+
+    let mem x (b,s) =
+      if b then not (EltSet.mem x s) else EltSet.mem x s
+
+    let singleton x = (false,EltSet.singleton x)
+
+    let add x (b,s) =
+      if b then (b,EltSet.remove x s)
+      else (b,EltSet.add x s)
+
+    let remove x (b,s) =
+      if b then (b,EltSet.add x s)
+      else (b,EltSet.remove x s)
+
+    let complement (b,s) = (not b, s)
+
+    let union s1 s2 =
+      match (s1,s2) with
+          ((false,p1),(false,p2)) -> (false,EltSet.union p1 p2)
+        | ((true,n1),(true,n2)) -> (true,EltSet.inter n1 n2)
+        | ((false,p1),(true,n2)) -> (true,EltSet.diff n2 p1)
+        | ((true,n1),(false,p2)) -> (true,EltSet.diff n1 p2)
+
+    let inter s1 s2 =
+      complement (union (complement s1) (complement s2))
+
+    let diff s1 s2 = inter s1 (complement s2)
+
+    let subset s1 s2 =
+      match (s1,s2) with
+          ((false,p1),(false,p2)) -> EltSet.subset p1 p2
+        | ((true,n1),(true,n2)) -> EltSet.subset n2 n1
+        | ((false,p1),(true,n2)) -> EltSet.is_empty (EltSet.inter p1 n2)
+        | ((true,_),(false,_)) -> false
+
+    let equal (b1,s1) (b2,s2) =
+      b1=b2 & EltSet.equal s1 s2
+
+  end
diff --git a/lib/predicate.mli b/lib/predicate.mli
new file mode 100644
index 00000000..160fa648
--- /dev/null
+++ b/lib/predicate.mli
@@ -0,0 +1,69 @@
+
+(* $Id: predicate.mli,v 1.1 2001/09/20 18:10:43 barras Exp $ *)
+
+(* Module [Pred]: sets over infinite ordered types with complement. *)
+
+(* 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. *)
+
+module type OrderedType =
+  sig
+    type t
+    val compare: t -> t -> int
+  end
+          (* 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
+             [f e1 e2] is zero if the elements [e1] and [e2] are equal,
+             [f e1 e2] is strictly negative if [e1] is smaller than [e2],
+             and [f e1 e2] is strictly positive if [e1] is greater than [e2].
+             Example: a suitable ordering function is
+             the generic structural comparison function [compare]. *)
+
+module type S =
+  sig
+    type elt
+          (* The type of the set elements. *)
+    type t
+          (* The type of sets. *)
+    val empty: t
+          (* The empty set. *)
+    val full: t
+          (* The whole type. *)
+    val is_empty: t -> bool
+        (* Test whether a set is empty or not. *)
+    val is_full: t -> bool
+        (* 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]. *)
+    val singleton: elt -> t
+        (* [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],
+           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],
+           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. *)
+    val equal: t -> t -> bool
+        (* [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
+           the set [s2]. *)
+    val elements: t -> bool * elt list
+        (* 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
+           given a totally ordered type. *)
diff --git a/lib/profile.ml b/lib/profile.ml
new file mode 100644
index 00000000..f55388f8
--- /dev/null
+++ b/lib/profile.ml
@@ -0,0 +1,742 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: profile.ml,v 1.13.16.1 2004/07/16 19:30:31 herbelin Exp $ *)
+
+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.)
+
+let get_time () =
+  let  {Unix.tms_utime = ut;Unix.tms_stime = st} = Unix.times () in
+  time_of_float (ut +. st)
+
+(* Since ocaml 3.01, gc statistics are in float *)
+let get_alloc () =
+  (* If you are unlucky, a minor collection can occur between the *)
+  (* measurements and produces allocation; we trigger a minor *)
+  (* collection in advance to be sure the measure is not corrupted *)
+  Gc.minor ();
+  Gc.allocated_bytes ()
+
+(* Rem: overhead was 16 bytes in ocaml 3.00 (long int) *)
+(* Rem: overhead is 100 bytes in ocaml 3.01 (double) *)
+
+let get_alloc_overhead =
+  let mark1 = get_alloc () in
+  let mark2 = get_alloc () in
+  let mark3 = get_alloc () in
+  (* If you are unlucky, a major collection can occur between the *)
+  (* measurements; with two measures the risk decreases *)
+  min (mark2 -. mark1) (mark3 -. mark2)
+
+let last_alloc = ref 0.0 (* set by init_profile () *)
+
+let spent_alloc () =
+  let now = get_alloc () in
+  let before = !last_alloc in
+  last_alloc := now;
+  now -. before -. get_alloc_overhead
+
+(* Profile records *)
+
+type profile_key = {
+  mutable owntime : int;
+  mutable tottime : int;
+  mutable ownalloc : float;
+  mutable totalloc : float;
+  mutable owncount : int;
+  mutable intcount : int;
+  mutable immcount : int;
+}
+
+let create_record () = {
+  owntime=0;
+  tottime=0;
+  ownalloc=0.0;
+  totalloc=0.0;
+  owncount=0;
+  intcount=0;
+  immcount=0
+}
+
+let ajoute_totalloc e dw = e.totalloc <- e.totalloc +. dw
+let ajoute_ownalloc e dw = e.ownalloc <- e.ownalloc +. dw
+
+let reset_record (n,e) =
+  e.owntime <- 0;
+  e.tottime <- 0;
+  e.ownalloc <- 0.0;
+  e.totalloc <- 0.0;
+  e.owncount <- 0;
+  e.intcount <- 0;
+  e.immcount <- 0
+
+(* Profile tables *)
+
+let prof_table = ref []
+let stack = ref []
+let init_time = ref 0
+let init_alloc = ref 0.0
+
+let reset_profile () = List.iter reset_record !prof_table
+
+let init_profile () =
+  let outside = create_record () in
+  stack := [outside];
+  last_alloc := get_alloc ();
+  init_alloc := !last_alloc;
+  init_time := get_time ();
+  outside.tottime <- - !init_time;
+  outside.owntime <- - !init_time
+
+let ajoute n o =
+  o.owntime <- o.owntime + n.owntime;
+  o.tottime <- o.tottime + n.tottime;
+  ajoute_ownalloc o n.ownalloc;
+  ajoute_totalloc o n.totalloc;
+  o.owncount <- o.owncount + n.owncount;
+  o.intcount <- o.intcount + n.intcount;
+  o.immcount <- o.immcount + n.immcount
+
+let ajoute_to_list ((name,n) as e) l =
+  try ajoute n (List.assoc name l); l
+  with Not_found -> e::l
+
+let magic = 1249
+  
+let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
+  let (old_table, old_outside, old_total) =
+    try 
+      let c = open_in filename in
+      if input_binary_int c <> magic 
+      then Printf.printf "Incompatible recording file: %s\n" filename;
+      let old_data = input_value c in
+      close_in c;
+      old_data
+    with Sys_error msg ->
+      (Printf.printf "Unable to open %s: %s\n" filename msg;
+       new_data) in
+  let updated_data =
+    let updated_table = List.fold_right ajoute_to_list curr_table old_table in
+    ajoute curr_outside old_outside;
+    ajoute curr_total old_total;
+    (updated_table, old_outside, old_total) in
+  begin
+    (try
+       let c =
+	 open_out_gen 
+           [Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 filename in
+       output_binary_int c magic;
+       output_value c updated_data;
+       close_out c
+     with Sys_error _ -> Printf.printf "Unable to create recording file");
+    updated_data
+  end
+
+(************************************************)
+(* Compute a rough estimation of time overheads *)
+
+(* Time and space are not measured in the same way *)
+
+(* Byte allocation is an exact number and for long runs, the total
+   number of allocated bytes may exceed the maximum integer capacity
+   (2^31 on 32-bits architectures);  therefore, allocation is measured
+   by small steps, total allocations are computed by adding elementary
+   measures and carries are controled from step to step *)
+
+(* Unix measure of time is approximative and shoitt delays are often
+   unperceivable; therefore, total times are measured in one (big)
+   step to avoid rounding errors and to get the best possible
+   approximation *)
+
+(*
+----------        start profile for f1
+overheadA|        ...
+  ---------- [1w1]  1st call to get_time for f1
+  overheadB|        ...
+  ----------        start f1
+   real 1  |        ...
+  ----------        start profile for 1st call to f2 inside f1
+  overheadA|        ...
+    ---------- [2w1]  1st call to get_time for 1st f2
+    overheadB|        ...
+    ----------        start 1st f2
+     real 2  |        ...
+    ----------        end 1st f2
+    overheadC|        ...
+    ---------- [2w1]  2nd call to get_time for 1st f2
+  overheadD|        ...
+  ----------        end profile for 1st f2
+   real 1  |        ...
+  ----------        start profile for 2nd call to f2 inside f1
+  overheadA|        ...
+    ---------- [2'w1] 1st call to get_time for 2nd f2
+    overheadB|        ...
+    ----------        start 2nd f2
+     real 2' |        ...
+    ----------        end 2nd f2
+    overheadC|        ...
+    ---------- [2'w2]  2nd call to get_time for 2nd f2 
+  overheadD|        ...
+  ----------        end profile for f2
+   real 1  |        ...
+  ----------        end f1
+  overheadC|        ...
+---------- [1w1'] 2nd call to get_time for f1
+overheadD|        ...
+----------        end profile for f1
+
+When profiling f2, overheadB + overheadC should be subtracted from measure
+and overheadA + overheadB + overheadC + overheadD should be subtracted from
+the amount for f1
+
+Then the relevant overheads are :
+
+  "overheadB + overheadC" to be subtracted to the measure of f as many time as f is called and
+
+  "overheadA + overheadB + overheadC + overheadD" to be subtracted to
+  the measure of f as many time as f calls a profiled function (itself
+  included)
+*)
+
+let dummy_last_alloc = ref 0.0
+let dummy_spent_alloc () =
+  let now = get_alloc () in
+  let before = !last_alloc in
+  last_alloc := now;
+  now -. before
+let dummy_f x = x
+let dummy_stack = ref [create_record ()]
+let dummy_ov = 0
+
+let loops = 10000
+
+let time_overhead_A_D () =
+  let e = create_record () in
+  let before = get_time () in
+  for i=1 to loops do
+    (* This is a copy of profile1 for overhead estimation *)
+    let dw = dummy_spent_alloc () in
+    match !dummy_stack with [] -> assert false | p::_ ->
+      ajoute_ownalloc p dw;
+      ajoute_totalloc p dw;
+      e.owncount <- e.owncount + 1;
+      if not (p==e) then stack := e::!stack;
+      let totalloc0 = e.totalloc in
+      let intcount0 = e.intcount in
+      let dt = get_time () - 1 in
+      e.tottime <- dt + dummy_ov; e.owntime <- e.owntime + e.tottime;
+      ajoute_ownalloc p dw;
+      ajoute_totalloc p dw;
+      p.owntime <- p.owntime - e.tottime;
+      ajoute_totalloc p (e.totalloc-.totalloc0);
+      p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+      p.immcount <- p.immcount + 1;
+      if not (p==e) then 
+	(match !dummy_stack with [] -> assert false | _::s -> stack := s);
+      dummy_last_alloc := get_alloc ()
+  done;
+  let after = get_time () in
+  let beforeloop =  get_time () in
+  for i=1 to loops do () done;
+  let afterloop = get_time () in
+  float_of_int ((after - before) - (afterloop - beforeloop))
+  /. float_of_int loops
+
+let time_overhead_B_C () =
+  let dummy_x = 0 in
+  let before = get_time () in
+  for i=1 to loops do
+    try
+      dummy_last_alloc := get_alloc ();
+      let r = dummy_f dummy_x in
+      let dw = dummy_spent_alloc () in
+      let dt = get_time () in
+      ()
+    with _ -> assert false
+  done;
+  let after = get_time () in
+  let beforeloop =  get_time () in
+  for i=1 to loops do () done;
+  let afterloop = get_time () in
+  float_of_int ((after - before) - (afterloop - beforeloop))
+  /. float_of_int loops
+
+let compute_alloc lo = lo /. (float_of_int word_length)
+
+(************************************************)
+(* End a profiling session and print the result *)
+
+let format_profile (table, outside, total) =
+  print_newline ();
+  Printf.printf 
+    "%-23s  %9s %9s %10s %10s %10s\n"
+    "Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls ";
+  let l = Sort.list (fun (_,{tottime=p}) (_,{tottime=p'}) -> p > p') table in
+  List.iter (fun (name,e) ->
+    Printf.printf
+      "%-23s %9.2f %9.2f %10.0f %10.0f %6d %6d\n"
+      name
+      (float_of_time e.owntime) (float_of_time e.tottime)
+      (compute_alloc e.ownalloc)
+      (compute_alloc e.totalloc)
+      e.owncount e.intcount)
+    l;
+  Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f        %6d\n"
+    "others" 
+    (float_of_time outside.owntime) (float_of_time outside.tottime)
+    (compute_alloc outside.ownalloc)
+    (compute_alloc outside.totalloc)
+    outside.intcount;
+  (* Here, own contains overhead time/alloc *)
+  Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f\n"
+    "Est. overhead/total"
+    (float_of_time total.owntime) (float_of_time total.tottime)
+    (compute_alloc total.ownalloc)
+    (compute_alloc total.totalloc);
+  Printf.printf
+    "Time in seconds and allocation in words (1 word = %d bytes)\n" 
+    word_length
+
+let recording_file = ref ""
+let set_recording s = recording_file := s
+
+let adjust_time ov_bc ov_ad e =
+  let bc_imm = float_of_int e.owncount *. ov_bc in
+  let ad_imm = float_of_int e.immcount *. ov_ad in
+  let abcd_all = float_of_int e.intcount *. (ov_ad +. ov_bc) in
+  {e with
+     tottime = e.tottime - int_of_float (abcd_all +. bc_imm);
+     owntime = e.owntime - int_of_float (ad_imm +. bc_imm) }
+
+let close_profile print = 
+  let dw = spent_alloc () in
+  let t = get_time () in
+  match !stack with
+    | [outside] ->
+	outside.tottime <- outside.tottime + t;
+	outside.owntime <- outside.owntime + t;
+	ajoute_ownalloc outside dw;
+	ajoute_totalloc outside dw;
+	if List.length !prof_table <> 0 then begin
+	  let ov_bc = time_overhead_B_C () (* B+C overhead *) in
+	  let ov_ad = time_overhead_A_D () (* A+D overhead *) in
+	  let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in
+	  let adjtable = List.map adjust !prof_table in
+	  let adjoutside = adjust_time ov_bc ov_ad outside in
+	  let totalloc = !last_alloc -. !init_alloc in
+	  let total = create_record () in
+	  total.tottime <- outside.tottime;
+	  total.totalloc <- totalloc;
+	  (* We compute estimations of overhead, put into "own" fields *)
+	  total.owntime <- outside.tottime - adjoutside.tottime;
+	  total.ownalloc <- totalloc -. outside.totalloc;
+	  let current_data = (adjtable, adjoutside, total) in
+	  let updated_data =
+	    match !recording_file with
+	      |	"" -> current_data
+	      | name -> merge_profile !recording_file current_data
+	  in
+	  if print then format_profile updated_data;
+	  init_profile ()
+	end
+    | _ -> failwith "Inconsistency"
+
+let append_profile () = close_profile false
+let print_profile () = close_profile true
+
+let declare_profile name =
+  if name = "___outside___" or name = "___total___" then
+    failwith ("Error: "^name^" is a reserved keyword");
+  let e = create_record () in
+  prof_table := (name,e)::!prof_table;
+  e
+
+(* Default initialisation, may be overriden *)
+let _ = init_profile ()
+
+(******************************)
+(* Entry points for profiling *)
+let profile1 e f a =
+  let dw = spent_alloc () in
+  match !stack with [] -> assert false | p::_ ->
+  (* We add spent alloc since last measure to current caller own/total alloc *)
+  ajoute_ownalloc p dw;
+  ajoute_totalloc p dw;
+  e.owncount <- e.owncount + 1;
+  if not (p==e) then stack := e::!stack;
+  let totalloc0 = e.totalloc in
+  let intcount0 = e.intcount in
+  let t = get_time () in
+  try
+    last_alloc := get_alloc ();
+    let r = f a in
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    r
+  with exn ->
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    raise exn
+
+let profile2 e f a b =
+  let dw = spent_alloc () in
+  match !stack with [] -> assert false | p::_ ->
+  (* We add spent alloc since last measure to current caller own/total alloc *)
+  ajoute_ownalloc p dw;
+  ajoute_totalloc p dw;
+  e.owncount <- e.owncount + 1;
+  if not (p==e) then stack := e::!stack;
+  let totalloc0 = e.totalloc in
+  let intcount0 = e.intcount in
+  let t = get_time () in
+  try
+    last_alloc := get_alloc ();
+    let r = f a b in
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    r
+  with exn ->
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    raise exn
+
+let profile3 e f a b c =
+  let dw = spent_alloc () in
+  match !stack with [] -> assert false | p::_ ->
+  (* We add spent alloc since last measure to current caller own/total alloc *)
+  ajoute_ownalloc p dw;
+  ajoute_totalloc p dw;
+  e.owncount <- e.owncount + 1;
+  if not (p==e) then stack := e::!stack;
+  let totalloc0 = e.totalloc in
+  let intcount0 = e.intcount in
+  let t = get_time () in
+  try
+    last_alloc := get_alloc ();
+    let r = f a b c in
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    r
+  with exn ->
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    raise exn
+
+let profile4 e f a b c d =
+  let dw = spent_alloc () in
+  match !stack with [] -> assert false | p::_ ->
+  (* We add spent alloc since last measure to current caller own/total alloc *)
+  ajoute_ownalloc p dw;
+  ajoute_totalloc p dw;
+  e.owncount <- e.owncount + 1;
+  if not (p==e) then stack := e::!stack;
+  let totalloc0 = e.totalloc in
+  let intcount0 = e.intcount in
+  let t = get_time () in
+  try
+    last_alloc := get_alloc ();
+    let r = f a b c d in
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    r
+  with exn ->
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    raise exn
+
+let profile5 e f a b c d g =
+  let dw = spent_alloc () in
+  match !stack with [] -> assert false | p::_ ->
+  (* We add spent alloc since last measure to current caller own/total alloc *)
+  ajoute_ownalloc p dw;
+  ajoute_totalloc p dw;
+  e.owncount <- e.owncount + 1;
+  if not (p==e) then stack := e::!stack;
+  let totalloc0 = e.totalloc in
+  let intcount0 = e.intcount in
+  let t = get_time () in
+  try
+    last_alloc := get_alloc ();
+    let r = f a b c d g in
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    r
+  with exn ->
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    raise exn
+
+let profile6 e f a b c d g h =
+  let dw = spent_alloc () in
+  match !stack with [] -> assert false | p::_ ->
+  (* We add spent alloc since last measure to current caller own/total alloc *)
+  ajoute_ownalloc p dw;
+  ajoute_totalloc p dw;
+  e.owncount <- e.owncount + 1;
+  if not (p==e) then stack := e::!stack;
+  let totalloc0 = e.totalloc in
+  let intcount0 = e.intcount in
+  let t = get_time () in
+  try
+    last_alloc := get_alloc ();
+    let r = f a b c d g h in
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    r
+  with exn ->
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    raise exn
+
+let profile7 e f a b c d g h i =
+  let dw = spent_alloc () in
+  match !stack with [] -> assert false | p::_ ->
+  (* We add spent alloc since last measure to current caller own/total alloc *)
+  ajoute_ownalloc p dw;
+  ajoute_totalloc p dw;
+  e.owncount <- e.owncount + 1;
+  if not (p==e) then stack := e::!stack;
+  let totalloc0 = e.totalloc in
+  let intcount0 = e.intcount in
+  let t = get_time () in
+  try
+    last_alloc := get_alloc ();
+    let r = f a b c d g h i in
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    r
+  with exn ->
+    let dw = spent_alloc () in
+    let dt = get_time () - t in
+    e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
+    ajoute_ownalloc e dw;
+    ajoute_totalloc e dw;
+    p.owntime <- p.owntime - dt;
+    ajoute_totalloc p (e.totalloc -. totalloc0);
+    p.intcount <- p.intcount + e.intcount - intcount0 + 1;
+    p.immcount <- p.immcount + 1;
+    if not (p==e) then 
+      (match !stack with [] -> assert false | _::s -> stack := s);
+    last_alloc := get_alloc ();
+    raise exn
+
+(* Some utilities to compute the logical and physical sizes and depth
+   of ML objects *)
+
+open Obj
+
+let c = ref 0
+let s = ref 0
+let b = ref 0
+let m = ref 0
+
+let rec obj_stats d t =
+  if is_int t then m := max d !m
+  else if tag t >= no_scan_tag then
+    if tag t = string_tag then
+      (c := !c + size t; b := !b + 1; m := max d !m)
+    else if tag t = double_tag then
+      (s := !s + 2; b := !b + 1; m := max d !m)
+    else if tag t = double_array_tag then
+      (s := !s + 2 * size t; b := !b + 1; m := max d !m)
+    else (b := !b + 1; m := max d !m)
+  else
+    let n = Obj.size t in
+    s := !s + n; b := !b + 1;
+    block_stats (d + 1) (n - 1) t
+
+and block_stats d i t =
+  if i >= 0 then (obj_stats d (field t i); block_stats d (i-1) t)
+
+let obj_stats a =
+  c := 0; s:= 0; b:= 0; m:= 0;
+  obj_stats 0 (Obj.repr a);
+  (!c, !s + !b, !m)
+
+module H = Hashtbl.Make(
+  struct 
+    type t = Obj.t 
+    let equal = (==) 
+    let hash o = Hashtbl.hash (magic o : int)
+  end)
+
+let tbl = H.create 13
+
+let rec obj_shared_size s t =
+  if is_int t then s
+  else if H.mem tbl t then s
+  else begin
+    H.add tbl t ();
+    let n = Obj.size t in
+    if tag t >= no_scan_tag then
+      if tag t = string_tag then (c := !c + n; s + 1)
+      else if tag t = double_tag then s + 3
+      else if tag t = double_array_tag then s + 2 * n + 1
+      else s + 1
+    else
+      block_shared_size (s + n + 1) (n - 1) t
+  end
+
+and block_shared_size s i t =
+  if i < 0 then s
+  else block_shared_size (obj_shared_size s (field t i)) (i-1) t
+
+let obj_shared_size a =
+  H.clear tbl;
+  c := 0;
+  let s = obj_shared_size 0 (Obj.repr a) in
+  (!c, s)
+
+let print_logical_stats a =
+  let (c, s, d) = obj_stats a in
+  Printf.printf "Expanded size: %10d (str: %8d) Depth: %6d\n" (s+c) c d
+
+let print_stats a =
+  let (c1, s, d) = obj_stats a in
+  let (c2, o) = obj_shared_size a in
+  Printf.printf "Size: %8d (str: %8d) (exp: %10d)  Depth: %6d\n"
+    (o + c2) c2 (s + c1) d
+(*
+let _ = Gc.set { (Gc.get()) with Gc.verbose = 13 }
+*)
diff --git a/lib/profile.mli b/lib/profile.mli
new file mode 100644
index 00000000..e0488de3
--- /dev/null
+++ b/lib/profile.mli
@@ -0,0 +1,129 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: profile.mli,v 1.7.16.1 2004/07/16 19:30:31 herbelin Exp $ *)
+
+(*s This program is a small time and allocation profiler for Objective Caml *)
+
+(*i It requires the UNIX library *)
+
+(* Adapted from Christophe Raffalli *)
+
+(* To use it, link it with the program you want to profile (do not forget
+"-cclib -lunix -custom unix.cma" among the link options).
+
+To trace a function "f" you first need to get a key for it by using :
+
+let fkey = declare_profile "f";;
+
+(the string is used to print the profile infomation). Warning: this
+function does a side effect. Choose the ident you want instead "fkey".
+
+Then if the function has ONE argument add the following just after
+the definition of "f" or just after the declare_profile if this one
+follows the definition of f.
+
+let f = profile1 fkey f;;
+
+If f has two arguments do the same with profile2, idem with 3, ...
+For more arguments than provided in this module, make a new copy of
+function profile and adapt for the needed arity.
+
+If you want to profile two mutually recursive functions, you had better
+to rename them :
+
+let fkey = declare_profile "f";;
+let gkey = declare_profile "g";;
+let f' = .... f' ... g'
+and g' = .... f' .... g'
+;;
+
+let f = profile fkey f';;
+let g = profile gkey g';;
+
+Before the program quits, you should call "print_profile ();;". It
+produces a result of the following kind:
+
+Function name              Own time Total time  Own alloc Tot. alloc     Calls 
+f                            0.28      0.47        116        116      5      4
+h                            0.19      0.19          0          0      4      0
+g                            0.00      0.00          0          0      0      0
+others                       0.00      0.47        392        508             9
+Est. overhead/total          0.00      0.47       2752       3260
+
+- The first column is the name of the function.
+- The third column give the time (utime + stime) spent inside the function.
+- The second column give the time spend inside the function minus the
+  time spend in other profiled functions called by it
+- The 4th and 5th columns give the same for allocated words
+- The 6th and 7th columns give the number of calls to the function and
+  the number of calls to profiled functions inside the scope of the
+  current function
+
+Remarks: 
+
+- If a function has a polymorphic type, you need to supply it with at
+  least one argument as in "let f a = profile1 fkey f a;;" (instead of
+  "let f = profile1 fkey f;;") in order to get generalization of the
+  type.
+- Each line of the form "let f a = profile1 fkey f a;;" in your code
+  counts for 5 words and each line of the form "let f
+  = profile1 fkey f;;" counts for 6 words (a word is 4 or 8 bytes
+  according to the architecture); this is counted for "others".
+- Time fields for functions doing a little job is usually non pertinent.
+
+i*)
+
+type profile_key
+
+val set_recording : string -> unit
+
+val print_profile : unit -> unit
+val reset_profile : unit -> unit
+val init_profile : unit -> unit
+val declare_profile : string -> profile_key
+
+val profile1 : profile_key -> ('a -> 'b) -> 'a -> 'b
+val profile2 : profile_key -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c
+val profile3 :
+  profile_key -> ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
+val profile4 :
+  profile_key -> ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e
+val profile5 :
+  profile_key ->
+  ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f
+val profile6 :
+  profile_key ->
+  ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g)
+    -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g
+val profile7 :
+  profile_key ->
+  ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) 
+    -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h
+
+
+(* 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 *)
+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
+   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 *)
+val obj_stats : 'a -> int * int * int
+
+(* 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/rtree.ml b/lib/rtree.ml
new file mode 100644
index 00000000..53cc372f
--- /dev/null
+++ b/lib/rtree.ml
@@ -0,0 +1,131 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: rtree.ml,v 1.2.8.1 2004/07/16 19:30:31 herbelin Exp $ i*)
+
+
+(* Type of regular trees:
+   - Param denotes tree variables (like de Bruijn indices)
+   - Node denotes the usual tree node, labelles with 'a
+   - Rec(j,v1..vn) introduces infinite tree. It denotes
+     v(j+1) with parameters 0..n-1 replaced by
+     Rec(0,v1..vn)..Rec(n-1,v1..vn) respectively.
+     Parameters n and higher denote parameters globals to the
+     current Rec node (as usual in de Bruijn binding system)
+ *)
+type 'a t =
+    Param of int 
+  | Node of 'a * 'a t array
+  | Rec of int * 'a t array
+
+(* Building trees *)
+let mk_param i = Param i
+let mk_node lab sons = Node (lab, sons)
+
+(* Given a vector of n bodies, builds the n mutual recursive trees.
+   Recursive calls are made with parameters 0 to n-1. We check
+   the bodies actually build something by checking it is not
+   directly one of the parameters 0 to n-1. *)
+let mk_rec defs =
+  Array.mapi
+    (fun i d ->
+      (match d with
+          Param k when k < Array.length defs -> failwith "invalid rec call"
+        | _ -> ());
+      Rec(i,defs))
+    defs
+
+(* The usual lift operation *)
+let rec lift_rtree_rec depth n = function
+    Param i -> if i < depth then Param i else Param (i+n)
+  | Node (l,sons) -> Node (l,Array.map (lift_rtree_rec depth n) sons)
+  | Rec(j,defs) ->
+      Rec(j, Array.map (lift_rtree_rec (depth+Array.length defs) n) defs)
+
+let lift n t = if n=0 then t else lift_rtree_rec 0 n t
+
+(* The usual subst operation *)
+let rec subst_rtree_rec depth sub = function
+    Param i ->
+      if i < depth then Param i
+      else if i-depth < Array.length sub then lift depth sub.(i-depth)
+      else Param (i-Array.length sub)
+  | Node (l,sons) -> Node (l,Array.map (subst_rtree_rec depth sub) sons)
+  | Rec(j,defs) ->
+      Rec(j, Array.map (subst_rtree_rec (depth+Array.length defs) sub) defs)
+
+let subst_rtree sub t = subst_rtree_rec 0 sub t
+
+let rec map f t = match t with
+    Param i -> Param i
+  | Node (a,sons) -> Node (f a, Array.map (map f) sons)
+  | Rec(j,defs) -> Rec (j, Array.map (map f) defs)
+
+let rec smartmap f t = match t with
+    Param i -> t
+  | Node (a,sons) -> 
+      let a'=f a and sons' = Util.array_smartmap (map f) sons in
+	if a'==a && sons'==sons then
+	  t
+	else
+	  Node (a',sons')
+  | Rec(j,defs) -> 
+      let defs' = Util.array_smartmap (map f) defs in
+	if defs'==defs then
+	  t
+	else
+	  Rec(j,defs')
+
+(* To avoid looping, we must check that every body introduces a node 
+   or a parameter *)
+let rec expand_rtree = function
+  | Rec(j,defs) ->
+      let sub = Array.init (Array.length defs) (fun i -> Rec(i,defs)) in
+      expand_rtree (subst_rtree sub defs.(j))
+  | t -> t
+
+(* Tree destructors, expanding loops when necessary *)
+let dest_param t = 
+  match expand_rtree t with
+      Param i -> i
+    | _ -> failwith "dest_param"
+
+let dest_node t = 
+  match expand_rtree t with
+      Node (l,sons) -> (l,sons)
+    | _ -> failwith "dest_node"
+
+(* Tests if a given tree is infinite or not. It proceeds *)
+let rec is_infinite = function
+    Param i -> i = (-1)
+  | Node(_,sons) -> Util.array_exists is_infinite sons
+  | Rec(j,defs) ->
+      let newdefs =
+        Array.mapi (fun i def -> if i=j then Param (-1) else def) defs in
+      let sub =
+        Array.init (Array.length defs)
+          (fun i -> if i=j then Param (-1) else Rec(i,newdefs)) in
+      is_infinite (subst_rtree sub defs.(j))
+
+(* Pretty-print a tree (not so pretty) *)
+open Pp
+
+let rec pp_tree prl t =
+  match t with
+      Param k -> str"#"++int k
+    | Node(lab,[||]) -> hov 2 (str"("++prl lab++str")")
+    | Node(lab,v) ->
+        hov 2 (str"("++prl lab++str","++brk(1,0)++
+               Util.prvect_with_sep Util.pr_coma (pp_tree prl) v++str")")
+    | Rec(i,v) ->
+        if Array.length v = 0 then str"Rec{}"
+        else if Array.length v = 1 then
+          hov 2 (str"Rec{"++pp_tree prl v.(0)++str"}")
+        else
+          hov 2 (str"Rec{"++int i++str","++brk(1,0)++
+                 Util.prvect_with_sep Util.pr_coma (pp_tree prl) v++str"}")
diff --git a/lib/rtree.mli b/lib/rtree.mli
new file mode 100644
index 00000000..0f854bc0
--- /dev/null
+++ b/lib/rtree.mli
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: rtree.mli,v 1.2.8.1 2004/07/16 19:30:31 herbelin Exp $ i*)
+
+(* Type of regular tree with nodes labelled by values of type 'a *)
+type 'a t
+
+(* Building trees *)
+(* build a recursive call *) 
+val mk_param : int -> 'a t
+(* build a node given a label and the vector of sons *)
+val mk_node  : 'a -> 'a t array -> 'a t
+(* build mutually dependent trees *)
+val mk_rec   : 'a t array -> 'a t array
+
+(* [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 map : ('a -> 'b) -> 'a t -> 'b t
+
+(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
+val smartmap : ('a -> 'a) -> 'a t -> 'a t
+
+(* Destructors (recursive calls are expanded) *)
+val dest_param : 'a t -> int
+val dest_node  : 'a t -> 'a * 'a t array
+
+(* Tells if a tree has an infinite branch *)
+val is_infinite : 'a t -> bool
+
+(* A rather simple minded pretty-printer *)
+val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
diff --git a/lib/stamps.ml b/lib/stamps.ml
new file mode 100644
index 00000000..1697c309
--- /dev/null
+++ b/lib/stamps.ml
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: stamps.ml,v 1.2.16.1 2004/07/16 19:30:31 herbelin Exp $ *)
+
+let new_stamp = 
+  let stamp_ctr = ref 0 in
+  fun () -> incr stamp_ctr; !stamp_ctr
+
+type 'a timestamped = { stamp : int; ed : 'a }
+
+let ts_stamp st = st.stamp
+let ts_mod f st = { stamp = new_stamp(); ed = f st.ed }
+let ts_it st = st.ed
+let ts_mk v = { stamp = new_stamp(); ed = v}
+let ts_eq st1 st2 = st1.stamp = st2.stamp
+
+type 'a idstamped = 'a timestamped
+
+let ids_mod f st = { stamp = st.stamp; ed = f st.ed}
+let ids_it = ts_it
+let ids_mk = ts_mk
+let ids_eq = ts_eq
diff --git a/lib/stamps.mli b/lib/stamps.mli
new file mode 100644
index 00000000..36f238b9
--- /dev/null
+++ b/lib/stamps.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: stamps.mli,v 1.3.16.1 2004/07/16 19:30:31 herbelin Exp $ i*)
+
+(* Time stamps. *)
+
+type 'a timestamped
+
+(* [ts_mod] gives a ['b timestamped] with a new stamp *)
+val ts_mod : ('a -> 'b) -> 'a timestamped -> 'b timestamped
+val ts_it : 'a timestamped -> 'a
+val ts_mk : 'a -> 'a timestamped
+val ts_eq : 'a timestamped -> 'a timestamped -> bool
+val ts_stamp : 'a timestamped -> int
+
+type 'a idstamped
+
+(* [ids_mod] gives a ['b stamped] with the same stamp *)
+val ids_mod : ('a -> 'b) -> 'a idstamped -> 'b idstamped
+val ids_it : 'a idstamped -> 'a
+val ids_mk : 'a -> 'a idstamped
+val ids_eq : 'a idstamped -> 'a idstamped -> bool
diff --git a/lib/system.ml b/lib/system.ml
new file mode 100644
index 00000000..fd782fe6
--- /dev/null
+++ b/lib/system.ml
@@ -0,0 +1,208 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: system.ml,v 1.31.8.1 2004/07/16 19:30:31 herbelin Exp $ *)
+
+open Pp
+open Util
+open Unix
+
+(* Expanding shell variables and home-directories *)
+
+let safe_getenv_def var def =
+  try 
+    Sys.getenv var
+  with Not_found ->
+    warning ("Environment variable "^var^" not found: using '"^def^"' .");
+    flush Pervasives.stdout;
+    def
+
+let home = (safe_getenv_def "HOME" ".")
+
+let safe_getenv n = safe_getenv_def n ("$"^n)
+
+let rec expand_atom s i =
+  let l = String.length s in
+  if i<l && (is_digit s.[i] or is_letter s.[i] or s.[i] = '_')
+  then expand_atom s (i+1)
+  else i
+
+let rec expand_macros b s i =
+  let l = String.length s in
+  if i=l then s else
+    match s.[i] with
+      | '$' -> 
+	  let n = expand_atom s (i+1) in
+	  let v = safe_getenv (String.sub s (i+1) (n-i-1)) in
+	  let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in
+	  expand_macros false s (i + String.length v)
+      | '/' ->
+	  expand_macros true s (i+1)
+      | '~' ->
+	  let n = expand_atom s (i+1) in
+	  let v =
+	    if n=i+1 then home
+	    else (getpwnam (String.sub s (i+1) (n-i-1))).pw_dir
+	  in
+	  let s = v^(String.sub s n (l-n)) in
+	  expand_macros false s (String.length v)
+      | c -> expand_macros false s (i+1)
+
+let glob s = expand_macros true s 0
+
+(* Files and load path. *)
+
+type physical_path = string
+type load_path = physical_path list
+
+(* All subdirectories, recursively *)
+
+let exists_dir dir =
+  try let _ = opendir dir in true with Unix_error _ -> false
+
+let all_subdirs ~unix_path:root =
+  let l = ref [] in
+  let add f rel = l := (f, rel) :: !l in
+  let rec traverse dir rel =
+    let dirh = opendir dir in
+    try
+      while true do
+	let f = readdir dirh in
+	if f <> "" && f.[0] <> '.' && (not Coq_config.local or (f <> "CVS"))
+        then
+	  let file = Filename.concat dir f in
+	  try 
+	    if (stat file).st_kind = S_DIR then begin
+	      let newrel = rel@[f] in
+	      add file newrel;
+	      traverse file newrel
+	    end
+	  with Unix_error (e,s1,s2) -> ()
+      done
+    with End_of_file ->
+      closedir dirh
+  in
+  if exists_dir root then
+   begin
+     add root [];
+     traverse root []
+   end ;
+  List.rev !l
+
+let search_in_path path filename =
+  let rec search = function
+    | lpe :: rem ->
+	let f = glob (Filename.concat lpe filename) in
+	if Sys.file_exists f then (lpe,f) else search rem
+    | [] ->
+	raise Not_found
+  in
+  search path
+
+let where_in_path = search_in_path
+
+let find_file_in_path paths name =
+  let globname = glob name in
+  if not (Filename.is_implicit globname) then
+    let root = Filename.dirname globname in
+    root, globname
+  else 
+    try 
+      search_in_path paths name
+    with Not_found ->
+      errorlabstrm "System.find_file_in_path"
+	(hov 0 (str "Can't find file" ++ spc () ++ str name ++ spc () ++ 
+		str "on loadpath"))
+
+let is_in_path lpath filename =
+  try
+    let _ = search_in_path lpath filename in true
+  with
+    Not_found -> false
+
+let make_suffix name suffix =
+  if Filename.check_suffix name suffix then name else (name ^ suffix)
+
+let file_readable_p na =
+  try access (glob na) [R_OK];true with Unix_error (_, _, _) -> false
+
+let open_trapping_failure open_fun name suffix =
+  let rname = glob (make_suffix name suffix) in
+  try open_fun rname with _ -> error ("Can't open " ^ rname)
+
+let try_remove f =
+  try Sys.remove f
+  with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++
+                   str f ++ str" which is corrupted!" )
+
+let marshal_out ch v = Marshal.to_channel ch v []
+let marshal_in ch =
+  try Marshal.from_channel ch
+  with End_of_file -> error "corrupted file: reached end of file"
+
+exception Bad_magic_number of string
+
+let raw_extern_intern magic suffix =
+  let extern_state name = 
+    let (_,channel) as filec =
+      open_trapping_failure (fun n -> n,open_out_bin n) name suffix in
+    output_binary_int channel magic;
+    filec
+  and intern_state fname = 
+    let channel = open_in_bin fname in
+    if input_binary_int channel <> magic then
+      raise (Bad_magic_number fname);
+    channel
+  in 
+  (extern_state,intern_state)
+
+let extern_intern magic suffix =
+  let (raw_extern,raw_intern) = raw_extern_intern magic suffix in
+  let extern_state name val_0 = 
+    try
+      let (fname,channel) = raw_extern name in
+      try
+        marshal_out channel val_0;
+        close_out channel
+      with e -> 
+	begin try_remove fname; raise e end
+    with Sys_error s -> error ("System error: " ^ s)
+  and intern_state paths name = 
+    try
+      let _,fname = find_file_in_path paths (make_suffix name suffix) in
+      let channel = raw_intern fname in
+      let v = marshal_in channel in
+      close_in channel; 
+      v
+    with Sys_error s -> 
+      error("System error: " ^ s)
+  in 
+  (extern_state,intern_state)
+
+
+(* 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)
+
+let time_difference (t1,_,_) (t2,_,_) = t2 -. t1
+			      
+let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) =
+  real (stopreal -. startreal) ++ str " secs " ++
+  str "(" ++
+  real ((-.) ustop ustart) ++ str "u" ++
+  str "," ++
+  real ((-.) sstop sstart) ++ str "s" ++
+  str ")"
diff --git a/lib/system.mli b/lib/system.mli
new file mode 100644
index 00000000..86d78b52
--- /dev/null
+++ b/lib/system.mli
@@ -0,0 +1,58 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: system.mli,v 1.17.16.1 2004/07/16 19:30:31 herbelin Exp $ i*)
+
+(*s Files and load paths. Load path entries remember the original root
+    given by the user. For efficiency, we keep the full path (field
+    [directory]), the root path and the path relative to the root. *)
+
+
+type physical_path = string
+type load_path = physical_path list
+
+val all_subdirs : unix_path:string -> (physical_path * string list) list
+val is_in_path : load_path -> string -> bool
+val where_in_path : load_path -> string -> physical_path * string
+
+val make_suffix : string -> string -> string
+val file_readable_p : string -> bool
+
+val glob : string -> string
+
+val home : string
+
+val exists_dir : string -> bool
+
+val find_file_in_path : load_path -> string -> physical_path * string
+
+(*s 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
+
+exception Bad_magic_number of string
+
+val raw_extern_intern : int -> string -> 
+  (string -> string * out_channel) * (string -> in_channel)
+
+val extern_intern : 
+  int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a)
+
+(*s Time stamps. *)
+
+type time
+
+val process_time : unit -> float * float
+val get_time : unit -> time
+val time_difference : time -> time -> float (* in seconds *)
+val fmt_time_difference : time -> time -> Pp.std_ppcmds
+
+
diff --git a/lib/tlm.ml b/lib/tlm.ml
new file mode 100644
index 00000000..23021be4
--- /dev/null
+++ b/lib/tlm.ml
@@ -0,0 +1,63 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: tlm.ml,v 1.3.16.1 2004/07/16 19:30:31 herbelin Exp $ *)
+
+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
new file mode 100644
index 00000000..a3011932
--- /dev/null
+++ b/lib/tlm.mli
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: tlm.mli,v 1.5.16.1 2004/07/16 19:30:31 herbelin Exp $ 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/util.ml b/lib/util.ml
new file mode 100644
index 00000000..37568f9b
--- /dev/null
+++ b/lib/util.ml
@@ -0,0 +1,824 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: util.ml,v 1.84.2.2 2004/07/16 20:43:46 herbelin Exp $ *)
+
+open Pp
+
+(* Errors *)
+
+exception Anomaly of string * std_ppcmds  (* System errors *)
+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 errorlabstrm l pps = raise (UserError(l,pps))
+
+let todo s = prerr_string ("TODO: "^s^"\n")
+
+type loc = Compat.loc
+let dummy_loc = Compat.dummy_loc
+let unloc = Compat.unloc
+let make_loc = Compat.make_loc
+
+(* 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 join_loc (deb1,_) (_,fin2) = (deb1,fin2)
+
+(* Like Exc_located, but specifies the outermost file read, the filename
+   associated to the location of the error, and the error itself. *)
+
+exception Error_in_file of string * (bool * string * loc) * exn
+
+(* Projections from triplets *)
+
+let pi1 (a,_,_) = a
+let pi2 (_,a,_) = a
+let pi3 (_,_,a) = a
+
+(* Characters *)
+
+let is_letter c =
+  (c >= 'a' && c <= 'z') or
+  (c >= 'A' && c <= 'Z') or
+  (c >= '\248' && c <= '\255') or
+  (c >= '\192' && c <= '\214') or
+  (c >= '\216' && c <= '\246')
+
+let is_digit c = (c >= '0' && c <= '9')
+
+let is_ident_tail c =
+  is_letter c or is_digit c or c = '\'' or c = '_'
+
+(* Strings *)
+
+let explode s = 
+  let rec explode_rec n =
+    if n >= String.length s then
+      []
+    else 
+      String.make 1 (String.get s n) :: explode_rec (succ n)
+  in 
+  explode_rec 0
+
+let implode sl = String.concat "" sl
+
+(* substring searching... *)
+
+(* gdzie = where, co = what *)
+(* gdzie=gdzie(string) gl=gdzie(length) gi=gdzie(index) *)
+let rec is_sub gdzie gl gi co cl ci = 
+  (ci>=cl) ||
+  ((String.unsafe_get gdzie gi = String.unsafe_get co ci) && 
+   (is_sub gdzie gl (gi+1) co cl (ci+1)))
+
+let rec raw_str_index i gdzie l c co cl = 
+  let i' = String.index_from gdzie i c in
+    if (i'+cl <= l) && (is_sub gdzie l i' co cl 0) then i' else
+      raw_str_index (i'+1) gdzie l c co cl
+
+let string_index_from gdzie i co = 
+  if co="" then i else
+    raw_str_index i gdzie (String.length gdzie)
+      (String.unsafe_get co 0) co (String.length co)
+
+let string_string_contains ~where ~what =
+  try
+    let _ = string_index_from where 0 what in true
+  with
+      Not_found -> false
+
+(* string parsing *)
+
+let parse_loadpath s =
+  let len = String.length s in
+  let rec decoupe_dirs n =
+    try  
+      let pos = String.index_from s n '/' in
+      if pos = n then
+	invalid_arg "parse_loadpath: find an empty dir in loadpath";
+      let dir = String.sub s n (pos-n) in
+      dir :: (decoupe_dirs (succ pos))
+    with
+      | Not_found -> [String.sub s n (len-n)]
+  in
+  if len = 0 then [] else decoupe_dirs 0
+
+module Stringset = Set.Make(struct type t = string let compare = compare end)
+
+module Stringmap = Map.Make(struct type t = string let compare = compare end)
+
+let stringmap_to_list m = Stringmap.fold (fun s y l -> (s,y)::l) m []
+
+let stringmap_dom m = Stringmap.fold (fun s _ l -> s::l) m []
+
+(* Lists *)
+
+let list_add_set x l = if List.mem x l then l else x::l
+
+let list_intersect l1 l2 = 
+  List.filter (fun x -> List.mem x l2) l1
+
+let list_union l1 l2 = 
+  let rec urec = function
+    | [] -> l2
+    | a::l -> if List.mem a l2 then urec l else a::urec l
+  in 
+  urec l1
+
+let list_unionq l1 l2 = 
+  let rec urec = function
+    | [] -> l2
+    | a::l -> if List.memq a l2 then urec l else a::urec l
+  in 
+  urec l1
+
+let list_subtract l1 l2 =
+  if l2 = [] then l1 else List.filter (fun x -> not (List.mem x l2)) l1
+
+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 list_assign l n e = 
+  let rec assrec stk = function
+    | ((h::t), 0) -> List.rev_append stk (e::t)
+    | ((h::t), n) -> assrec (h::stk) (t, n-1)
+    | ([], _) -> failwith "list_assign"
+  in 
+  assrec [] (l,n)
+
+let rec list_smartmap f l = match l with
+    [] -> l
+  | h::tl -> 
+      let h' = f h and tl' = list_smartmap f tl in
+	if h'==h && tl'==tl then l
+	else h'::tl'
+
+let list_map_left f = (* ensures the order in case of side-effects *)
+  let rec map_rec = function
+    | [] -> [] 
+    | x::l -> let v = f x in v :: map_rec l
+  in 
+  map_rec
+
+let list_map_i f = 
+  let rec map_i_rec i = function
+    | [] -> [] 
+    | x::l -> let v = f i x in v :: map_i_rec (i+1) l
+  in 
+  map_i_rec
+
+let list_map2_i f i l1 l2 =  
+  let rec map_i i = function
+    | ([], []) -> []
+    | ((h1::t1), (h2::t2)) -> (f i h1 h2) :: (map_i (succ i) (t1,t2))
+    | (_, _) -> invalid_arg "map2_i"
+  in 
+  map_i i (l1,l2)
+
+let list_map3 f l1 l2 l3 =
+  let rec map = function
+    | ([], [], []) -> []
+    | ((h1::t1), (h2::t2), (h3::t3)) -> (f h1 h2 h3) :: (map (t1,t2,t3))
+    | (_, _, _) -> invalid_arg "map3"
+  in 
+  map (l1,l2,l3)
+
+let list_index x = 
+  let rec index_x n = function
+    | y::l -> if x = y then n else index_x (succ n) l
+    | [] -> raise Not_found
+  in 
+  index_x 1
+
+let list_fold_left_i f = 
+  let rec it_list_f i a = function
+    | [] -> a 
+    | b::l -> it_list_f (i+1) (f i a b) l
+  in 
+  it_list_f 
+
+(* [list_fold_right_and_left f [a1;...;an] hd =
+   f (f (... (f (f hd
+                   an
+                   [an-1;...;a1])
+              an-1
+              [an-2;...;a1])
+         ...)
+        a2
+        [a1])
+     a1
+     []] *)
+
+let rec list_fold_right_and_left f l hd =
+  let rec aux tl = function
+    | [] -> hd
+    | a::l -> let hd = aux (a::tl) l in f hd a tl
+   in aux [] l
+
+let list_iter_i f l = list_fold_left_i (fun i _ x -> f i x) 0 () l
+
+let list_for_all_i p = 
+  let rec for_all_p i = function
+    | [] -> true 
+    | a::l -> p i a && for_all_p (i+1) l
+  in 
+  for_all_p
+
+let list_except x l = List.filter (fun y -> not (x = y)) l
+
+let list_for_all2eq f l1 l2 = try List.for_all2 f l1 l2 with Failure _ -> false
+
+let list_map_i f = 
+  let rec map_i_rec i = function
+    | [] -> [] 
+    | x::l -> let v = f i x in v::map_i_rec (i+1) l
+  in 
+  map_i_rec
+
+let rec list_sep_last = function
+  | [] -> failwith "sep_last"
+  | hd::[] -> (hd,[])
+  | hd::tl -> let (l,tl) = list_sep_last tl in (l,hd::tl)
+
+let list_try_find_i f = 
+  let rec try_find_f n = function
+    | [] -> failwith "try_find_i"
+    | h::t -> try f n h with Failure _ -> try_find_f (n+1) t
+  in 
+  try_find_f
+
+let list_try_find f = 
+  let rec try_find_f = function
+    | [] -> failwith "try_find"
+    | h::t -> try f h with Failure _ -> try_find_f t
+  in 
+  try_find_f
+
+let rec list_uniquize = function
+  | [] -> []
+  | h::t -> if List.mem h t then list_uniquize t else h::(list_uniquize t)
+
+let rec list_distinct = function
+  | h::t -> (not (List.mem h t)) && list_distinct t
+  | _ -> true
+
+let rec list_filter2 f = function
+  | [], [] as p -> p
+  | d::dp, l::lp ->
+     let (dp',lp' as p) = list_filter2 f (dp,lp) in
+      if f d l then d::dp', l::lp' else p
+  | _ -> invalid_arg "list_filter2"
+
+let list_subset l1 l2 =
+  let t2 = Hashtbl.create 151 in
+  List.iter (fun x -> Hashtbl.add t2 x ()) l2;
+  let rec look = function
+    | [] -> true
+    | x::ll -> try Hashtbl.find t2 x; look ll with Not_found -> false
+  in 
+  look l1
+
+let list_splitby p = 
+  let rec splitby_loop x y = 
+    match y with 
+      | []      -> ([],[])
+      | (a::l)  -> if (p a) then (x,y) else (splitby_loop (x@[a]) l)
+  in 
+  splitby_loop []
+
+let rec list_split3 = function
+  | [] -> ([], [], [])
+  | (x,y,z)::l ->
+      let (rx, ry, rz) = list_split3 l in (x::rx, y::ry, z::rz)
+
+let list_firstn n l =
+  let rec aux acc = function
+    | (0, l) -> List.rev acc
+    | (n, (h::t)) -> aux (h::acc) (pred n, t)
+    | _ -> failwith "firstn"
+  in 
+  aux [] (n,l)
+
+let rec list_last = function
+  | [] -> failwith "list_last"
+  | [x] -> x
+  | _ :: l -> list_last l
+
+let list_lastn n l =
+  let len = List.length l in
+  let rec aux m l =
+    if m = n then l else aux (m - 1) (List.tl l)
+  in
+  if len < n then failwith "lastn" else aux len l
+
+let rec list_skipn n l = match n,l with 
+  | 0, _ -> l 
+  | _, [] -> failwith "list_fromn"
+  | n, _::l -> list_skipn (pred n) l
+
+let list_prefix_of prefl l = 
+  let rec prefrec = function
+    | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)
+    | ([], _) -> true
+    | (_, _) -> false
+  in 
+  prefrec (prefl,l)
+
+let list_map_append f l = List.flatten (List.map f l)
+
+let list_map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
+
+let list_share_tails l1 l2 =
+  let rec shr_rev acc = function
+    | ((x1::l1), (x2::l2)) when x1 == x2 -> shr_rev (x1::acc) (l1,l2)
+    | (l1,l2) -> (List.rev l1, List.rev l2, acc)
+  in 
+  shr_rev [] (List.rev l1, List.rev l2)
+
+let list_join_map f l = List.flatten (List.map f l)
+
+let rec list_fold_map f e = function 
+  |  []  -> (e,[])
+  |  h::t -> 
+       let e',h' = f e h in
+       let e'',t' = list_fold_map f e' t in
+	 e'',h'::t'
+
+(* (* tail-recursive version of the above function *)
+let list_fold_map f e l = 
+  let g (e,b') h = 
+    let (e',h') = f e h in
+      (e',h'::b') 
+  in
+  let (e',lrev) = List.fold_left g (e,[]) l in
+    (e',List.rev lrev)
+*)
+
+let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
+
+(* Arrays *)
+
+let array_exists f v = 
+  let rec exrec = function
+    | -1 -> false
+    | n -> (f v.(n)) || (exrec (n-1))
+  in 
+  exrec ((Array.length v)-1) 
+
+let array_for_all f v = 
+  let rec allrec = function
+    | -1 -> true
+    | n -> (f v.(n)) && (allrec (n-1))
+  in 
+  allrec ((Array.length v)-1) 
+
+let array_for_all2 f v1 v2 =
+  let rec allrec = function
+    | -1 -> true
+    | n -> (f v1.(n) v2.(n)) && (allrec (n-1))
+  in 
+  let lv1 = Array.length v1 in
+  lv1 = Array.length v2 && allrec (pred lv1) 
+
+let array_for_all3 f v1 v2 v3 =
+  let rec allrec = function
+    | -1 -> true
+    | n -> (f v1.(n) v2.(n) v3.(n)) && (allrec (n-1))
+  in 
+  let lv1 = Array.length v1 in
+  lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1) 
+
+let array_for_all4 f v1 v2 v3 v4 =
+  let rec allrec = function
+    | -1 -> true
+    | n -> (f v1.(n) v2.(n) v3.(n) v4.(n)) && (allrec (n-1))
+  in 
+  let lv1 = Array.length v1 in
+  lv1 = Array.length v2 &&
+  lv1 = Array.length v3 &&
+  lv1 = Array.length v4 &&
+    allrec (pred lv1) 
+
+let array_hd v = 
+  match Array.length v with
+    | 0 -> failwith "array_hd"
+    | _ -> v.(0)
+
+let array_tl v = 
+  match Array.length v with
+    | 0 -> failwith "array_tl"
+    | n -> Array.sub v 1 (pred n)
+
+let array_last v =
+  match Array.length v with
+    | 0 -> failwith "array_last"
+    | n -> v.(pred n)
+
+let array_cons e v = Array.append [|e|] v
+
+let array_fold_right_i f v a =
+  let rec fold a n =
+    if n=0 then a
+    else
+      let k = n-1 in
+      fold (f k v.(k) a) k in
+  fold a (Array.length v)
+
+let array_fold_left_i f v a =
+  let n = Array.length a in
+  let rec fold i v = if i = n then v else fold (succ i) (f i v a.(i)) in
+  fold 0 v
+
+let array_fold_right2 f v1 v2 a =
+  let lv1 = Array.length v1 in
+  let rec fold a n =
+    if n=0 then a
+    else
+      let k = n-1 in
+      fold (f v1.(k) v2.(k) a) k in
+  if Array.length v2 <> lv1 then invalid_arg "array_fold_right2";
+  fold a lv1
+
+let array_fold_left2 f a v1 v2 =
+  let lv1 = Array.length v1 in
+  let rec fold a n = 
+    if n >= lv1 then a else fold (f a v1.(n) v2.(n)) (succ n)
+  in
+  if Array.length v2 <> lv1 then invalid_arg "array_fold_left2";
+  fold a 0
+
+let array_fold_left2_i f a v1 v2 =
+  let lv1 = Array.length v1 in
+  let rec fold a n = 
+    if n >= lv1 then a else fold (f n a v1.(n) v2.(n)) (succ n)
+  in
+  if Array.length v2 <> 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)
+  in 
+  fold a n
+
+let array_fold_right_from n f v a = 
+  let rec fold n =
+    if n >= Array.length v then a else f v.(n) (fold (succ n))
+  in 
+  fold n
+
+let array_app_tl v l = 
+  if Array.length v = 0 then invalid_arg "array_app_tl";
+  array_fold_right_from 1 (fun e l -> e::l) v l
+
+let array_list_of_tl v =
+  if Array.length v = 0 then invalid_arg "array_list_of_tl";
+  array_fold_right_from 1 (fun e l -> e::l) v []
+
+let array_map_to_list f v =
+  List.map f (Array.to_list v)
+
+let array_chop n v =
+  let vlen = Array.length v in
+  if n > vlen then failwith "array_chop";
+  (Array.sub v 0 n, Array.sub v n (vlen-n))
+
+exception Local of int
+
+(* If none of the elements is changed by f we return ar itself.
+   The for loop looks for the first such an element.
+   If found it is temporarily stored in a ref and the new array is produced, 
+   but f is not re-applied to elements that are already checked *)
+let array_smartmap f ar = 
+  let ar_size = Array.length ar in
+  let aux = ref None in
+  try
+    for i = 0 to ar_size-1 do
+      let a = ar.(i) in
+      let a' = f a in
+	if a != a' then (* pointer (in)equality *) begin
+	  aux := Some a';
+	  raise (Local i)
+	end
+    done;
+    ar
+  with
+      Local i -> 
+	let copy j = 
+	  if j<i then ar.(j) 
+	  else if j=i then 
+	    match !aux with Some a' -> a' | None -> failwith "Error"
+	  else f (ar.(j))
+	in
+	  Array.init ar_size copy
+
+let array_map2 f v1 v2 =
+  if Array.length v1 <> Array.length v2 then invalid_arg "array_map2";
+  if Array.length v1 == 0 then 
+    [| |] 
+  else begin
+    let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in
+    for i = 1 to pred (Array.length v1) do
+      res.(i) <- f v1.(i) v2.(i)
+    done;
+    res
+  end
+
+let array_map2_i f v1 v2 =
+  if Array.length v1 <> Array.length v2 then invalid_arg "array_map2";
+  if Array.length v1 == 0 then 
+    [| |] 
+  else begin
+    let res = Array.create (Array.length v1) (f 0 v1.(0) v2.(0)) in
+    for i = 1 to pred (Array.length v1) do
+      res.(i) <- f i v1.(i) v2.(i)
+    done;
+    res
+  end
+
+let array_map3 f v1 v2 v3 =
+  if Array.length v1 <> Array.length v2 ||
+     Array.length v1 <> Array.length v3 then invalid_arg "array_map3";
+  if Array.length v1 == 0 then 
+    [| |] 
+  else begin
+    let res = Array.create (Array.length v1) (f v1.(0) v2.(0) v3.(0)) in
+    for i = 1 to pred (Array.length v1) do
+      res.(i) <- f v1.(i) v2.(i) v3.(i)
+    done;
+    res
+  end
+
+let array_map_left f a = (* Ocaml does not guarantee Array.map is LR *)
+  let l = Array.length a in (* (even if so), then we rewrite it *)
+  if l = 0 then [||] else begin
+    let r = Array.create l (f a.(0)) in
+    for i = 1 to l - 1 do
+      r.(i) <- f a.(i)
+    done;
+    r
+  end
+
+let array_map_left_pair f a g b =
+  let l = Array.length a in
+  if l = 0 then [||],[||] else begin
+    let r = Array.create l (f a.(0)) in
+    let s = Array.create l (g b.(0)) in
+    for i = 1 to l - 1 do
+      r.(i) <- f a.(i);
+      s.(i) <- g b.(i)
+    done;
+    r, s
+  end
+
+(* Matrices *)
+
+let matrix_transpose mat =
+  List.fold_right (List.map2 (fun p c -> p::c)) mat
+    (if mat = [] then [] else List.map (fun _ -> []) (List.hd mat))
+
+(* Functions *)
+
+let identity x = x
+
+let compose f g x = f (g x)
+
+let iterate f = 
+  let rec iterate_f n x =
+    if n <= 0 then x else iterate_f (pred n) (f x)
+  in 
+  iterate_f
+
+let repeat n f x =
+  for i = 1 to n do f x done
+
+let iterate_for a b f x =
+  let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in
+  iterate a x
+ 
+(* Misc *)
+
+type ('a,'b) union = Inl of 'a | Inr of 'b
+
+module Intset = Set.Make(struct type t = int let compare = compare end)
+
+module Intmap = Map.Make(struct type t = int let compare = compare end)
+
+let intmap_in_dom x m =
+  try let _ = Intmap.find x m in true with Not_found -> false
+
+let intmap_to_list m = Intmap.fold (fun n v l -> (n,v)::l) m []
+
+let intmap_inv m b = Intmap.fold (fun n v l -> if v = b then n::l else l) m []
+
+let interval n m = 
+  let rec interval_n (l,m) =
+    if n > m then l else interval_n (m::l,pred m)
+  in 
+  interval_n ([],m)
+
+let in_some x = Some x
+
+let out_some = function
+  | Some x -> x
+  | None -> failwith "out_some"
+
+let option_app f = function
+  | None -> None
+  | Some x -> Some (f x)
+
+let option_cons a l = match a with
+  | Some x -> x::l
+  | None -> l
+
+let option_fold_left2 f e a b = match (a,b) with
+  | Some x, Some y -> f e x y
+  | _ -> e
+
+let option_fold_right f a e = match a with
+  | Some x -> f x e
+  | _ -> e
+
+let option_compare f a b = match (a,b) with
+  | None, None -> true
+  | Some a', Some b' -> f a' b'
+  | _ -> failwith "option_compare"
+
+let option_iter f = function
+  | None -> ()
+  | Some x -> f x
+
+let option_smartmap f a = match a with
+  | None -> a
+  | Some x -> let x' = f x in if x'==x then a else Some x'
+
+let map_succeed f = 
+  let rec map_f = function 
+    | [] -> []
+    |  h::t -> try (let x = f h in x :: map_f t) with Failure _ -> map_f t
+  in 
+  map_f 
+
+(* Pretty-printing *)
+  
+let pr_spc = spc
+let pr_fnl = fnl
+let pr_int = int
+let pr_str = str
+let pr_coma () = str "," ++ spc ()
+let pr_semicolon () = str ";" ++ spc ()
+let pr_bar () = str "|" ++ spc ()
+
+let pr_ord n =
+  let suff = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
+  int n ++ str suff
+
+let rec prlist elem l = match l with 
+  | []   -> mt ()
+  | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
+
+let rec prlist_with_sep sep elem l = match l with
+  | []   -> mt ()
+  | [h]  -> elem h
+  | h::t ->
+      let e = elem h and s = sep() and r = prlist_with_sep sep elem t in
+      e ++ s ++ r
+
+let pr_vertical_list pr = function
+  | [] -> str "none" ++ fnl ()
+  | l -> fnl () ++ str "  " ++ hov 0 (prlist_with_sep pr_fnl pr l) ++ fnl ()
+      
+let prvecti elem v =
+  let n = Array.length v in
+  let rec pr i =
+    if i = 0 then 
+      elem 0 v.(0)
+    else
+      let r = pr (i-1) and e = elem i v.(i) in r ++ e
+  in
+  if n = 0 then mt () else pr (n - 1)
+
+let prvect_with_sep sep elem v =
+  let rec pr n =
+    if n = 0 then 
+      elem v.(0)
+    else 
+      let r = pr (n-1) and s = sep() and e = elem v.(n) in 
+      r ++ s ++ e
+      in
+  let n = Array.length v in
+  if n = 0 then mt () else pr (n - 1)
+
+(*s Size of ocaml values. *)
+
+module Size = struct
+  
+  open Obj
+
+  (*s Pointers already visited are stored in a hash-table, where
+      comparisons are done using physical equality. *)
+
+  module H = Hashtbl.Make(
+    struct 
+      type t = Obj.t 
+      let equal = (==) 
+      let hash o = Hashtbl.hash (magic o : int)
+    end)
+	       
+  let node_table = (H.create 257 : unit H.t)
+		     
+  let in_table o = try H.find node_table o; true with Not_found -> false
+      
+  let add_in_table o = H.add node_table o ()
+			 
+  let reset_table () = H.clear node_table
+			 
+  (*s Objects are traversed recursively, as soon as their tags are less than
+      [no_scan_tag]. [count] records the numbers of words already visited. *)
+
+  let size_of_double = size (repr 1.0)
+			 
+  let count = ref 0
+		
+  let rec traverse t =
+    if not (in_table t) then begin
+      add_in_table t;
+      if is_block t then begin
+	let n = size t in
+	let tag = tag t in
+	if tag < no_scan_tag then begin
+	  count := !count + 1 + n;
+	  for i = 0 to n - 1 do
+      	    let f = field t i in 
+	    if is_block f then traverse f
+	  done
+	end else if tag = string_tag then
+	  count := !count + 1 + n 
+	else if tag = double_tag then
+	  count := !count + size_of_double
+	else if tag = double_array_tag then
+	  count := !count + 1 + size_of_double * n 
+	else
+	  incr count
+      end
+    end
+      
+  (*s Sizes of objects in words and in bytes. The size in bytes is computed
+      system-independently according to [Sys.word_size]. *)
+
+  let size_w o =
+    reset_table ();
+    count := 0;
+    traverse (repr o);
+    !count
+
+  let size_b o = (size_w o) * (Sys.word_size / 8)
+
+  let size_kb o = (size_w o) / (8192 / Sys.word_size)
+
+end
+
+let size_w = Size.size_w
+let size_b = Size.size_b
+let size_kb = Size.size_kb
+
+(*s Total size of the allocated ocaml heap. *)
+
+let heap_size () =
+  let stat = Gc.stat ()
+  and control = Gc.get () in
+  let max_words_total = stat.Gc.heap_words + control.Gc.minor_heap_size in
+  (max_words_total * Sys.word_size / 8)
+
+let heap_size_kb () = (heap_size () + 1023) / 1024
+
+(*s interruption *)
+
+let interrupt = ref false
+let check_for_interrupt () = 
+  if !interrupt then begin interrupt := false; raise Sys.Break end
+
diff --git a/lib/util.mli b/lib/util.mli
new file mode 100644
index 00000000..19f05ea4
--- /dev/null
+++ b/lib/util.mli
@@ -0,0 +1,250 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: util.mli,v 1.84.2.2 2004/07/16 20:43:46 herbelin Exp $ i*)
+
+(*i*)
+open Pp
+(*i*)
+
+(* This module contains numerous utility functions on strings, lists,
+   arrays, etc. *)
+
+(*s Errors. [Anomaly] is used for system errors and [UserError] for the
+   user's ones. *)
+
+exception Anomaly of string * std_ppcmds
+val anomaly : string -> 'a
+val anomalylabstrm : string -> std_ppcmds -> 'a
+
+exception UserError of string * std_ppcmds
+val error : string -> 'a
+val errorlabstrm : string -> std_ppcmds -> 'a
+
+(* [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 *)
+
+val todo : string -> unit
+
+type loc = Compat.loc
+
+type 'a located = loc * 'a
+
+val unloc : loc -> int * int
+val make_loc : int * int -> loc
+val dummy_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
+
+(* 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
+
+(*s Projections from triplets *)
+
+val pi1 : 'a * 'b * 'c -> 'a
+val pi2 : 'a * 'b * 'c -> 'b
+val pi3 : 'a * 'b * 'c -> 'c
+
+(*s Chars. *)
+
+val is_letter : char -> bool
+val is_digit : char -> bool
+val is_ident_tail : char -> bool
+
+(*s Strings. *)
+
+val explode : string -> string list
+val implode : string list -> string
+val string_index_from : string -> int -> string -> int
+val string_string_contains : where:string -> what:string -> bool
+
+val parse_loadpath : string -> string list
+
+module Stringset : Set.S with type elt = string
+
+module Stringmap : Map.S with type key = string
+
+val stringmap_to_list : 'a Stringmap.t -> (string * 'a) list 
+val stringmap_dom : 'a Stringmap.t -> string list
+
+(*s Lists. *)
+
+val list_add_set : 'a -> 'a list -> 'a list
+val list_intersect : 'a list -> 'a list -> 'a list
+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)]] *)
+val list_tabulate : (int -> 'a) -> int -> 'a list
+val list_assign : 'a list -> int -> 'a -> 'a list
+val list_distinct : 'a list -> bool
+val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
+
+(* [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
+   [ 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
+val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
+val list_map2_i : 
+  (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
+val list_map3 :
+  ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
+val list_index : 'a -> 'a list -> int
+val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
+val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
+val list_fold_right_and_left :
+    ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
+val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
+val list_except : 'a -> 'a list -> 'a list
+val list_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
+val list_subset : 'a list -> 'a list -> bool
+val list_splitby : ('a -> bool) -> 'a list -> 'a list * 'a list
+val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
+val list_firstn : int -> 'a list -> 'a list
+val list_last : 'a list -> 'a
+val list_lastn : int -> 'a list -> 'a list
+val list_skipn : int -> 'a list -> 'a list 
+val list_prefix_of : 'a list -> 'a list -> bool
+(* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
+val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
+(* 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
+val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
+(* [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
+   where [(e_i,k_i)=f e_{i-1} l_i] *)
+val list_fold_map : 
+  ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list 
+val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
+
+(*s Arrays. *)
+
+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
+val array_for_all3 : ('a -> 'b -> 'c -> bool) ->
+  'a array -> 'b array -> 'c array -> bool
+val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) ->
+  'a array -> 'b array -> 'c array -> 'd array -> bool
+val array_hd : 'a array -> 'a
+val array_tl : 'a array -> 'a array
+val array_last : 'a array -> 'a
+val array_cons : 'a -> 'a array -> 'a array
+val array_fold_right_i : 
+  (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a
+val array_fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
+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_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
+val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
+val array_app_tl : 'a array -> 'a list -> 'a list
+val array_list_of_tl : 'a array -> 'a list
+val array_map_to_list : ('a -> 'b) -> 'a array -> 'b list
+val array_chop : int -> 'a array -> 'a array * 'a array
+val array_smartmap : ('a -> 'a) -> 'a array -> 'a array
+val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
+val array_map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
+val array_map3 : 
+  ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
+val array_map_left : ('a -> 'b) -> 'a array -> 'b array
+val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array ->
+  'b array * 'd array
+
+(*s Matrices *)
+
+val matrix_transpose : 'a list list -> 'a list list
+
+(*s Functions. *)
+
+val identity : 'a -> 'a
+val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+val iterate : ('a -> 'a) -> int -> 'a -> 'a
+val repeat : int -> ('a -> unit) -> 'a -> unit
+val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a
+
+(*s Misc. *)
+
+type ('a,'b) union = Inl of 'a | Inr of 'b
+
+module Intset : Set.S with type elt = int
+
+module Intmap : Map.S with type key = int
+
+val intmap_in_dom : int -> 'a Intmap.t -> bool
+val intmap_to_list : 'a Intmap.t -> (int * 'a) list
+val intmap_inv : 'a Intmap.t -> 'a -> int list
+
+val interval : int -> int -> int list
+
+val in_some : 'a -> 'a option
+val out_some : 'a option -> 'a
+val option_app : ('a -> 'b) -> 'a option -> 'b option
+val option_cons : 'a option -> 'a list -> 'a list
+val option_fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
+val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option ->
+  'c option -> 'a
+val option_iter : ('a -> unit) -> 'a option -> unit
+val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool 
+val option_smartmap : ('a -> 'a) -> 'a option -> 'a option
+
+(* 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. *)
+
+val pr_spc : unit -> std_ppcmds
+val pr_fnl : unit -> std_ppcmds
+val pr_int : int -> std_ppcmds
+val pr_str : string -> std_ppcmds
+val pr_coma : unit -> std_ppcmds
+val pr_semicolon : unit -> std_ppcmds
+val pr_bar : unit -> std_ppcmds
+val pr_ord : int -> std_ppcmds
+
+val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prlist_with_sep :
+   (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+val prvect_with_sep :
+   (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds
+val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+
+(*s 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. *)
+
+val heap_size : unit -> int
+val heap_size_kb : unit -> int
+
+(*s Coq interruption: set the following boolean reference to interrupt Coq
+    (it eventually raises [Break], simulating a Ctrl-C) *)
+
+val interrupt : bool ref
+val check_for_interrupt : unit -> unit