61 files changed, 1424 insertions, 2092 deletions

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index f7bd81f85..c6c7b4242 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -25,9 +25,9 @@ let mk_absolute vfile =
   if Filename.is_relative vfile then CUnix.correct_path vfile (Sys.getcwd ())
   else vfile
 
-let start_aux_file_for vfile =
-  let vfile = mk_absolute vfile in
-  oc := Some (open_out (aux_file_name_for vfile));
+let start_aux_file ~aux_file:output_file ~v_file =
+  let vfile = mk_absolute v_file in
+  oc := Some (open_out output_file);
   Printf.fprintf (Option.get !oc) "COQAUX%d %s %s\n"
     version (Digest.to_hex (Digest.file vfile)) vfile
 
@@ -87,8 +87,7 @@ let load_aux_file_for vfile =
   | End_of_file -> !h
   | Sys_error s | Scanf.Scan_failure s
   | Failure s | Invalid_argument s ->
-     Flags.if_verbose
-       Pp.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s);
+    Flags.if_verbose Feedback.msg_info Pp.(str"Loading file "++str aux_fname++str": "++str s);
      empty_aux_file
 
 let set h loc k v = set h (Loc.unloc loc) k v
diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index 127827ab6..86e322b71 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -17,7 +17,8 @@ module H : Map.S with type key = int * int
 module M : Map.S with type key = string
 val contents : aux_file -> string M.t H.t
 
-val start_aux_file_for : string -> unit
+val aux_file_name_for : string -> string
+val start_aux_file : aux_file:string -> v_file:string -> unit
 val stop_aux_file : unit -> unit 
 val recording : unit -> bool
 
diff --git a/lib/errors.ml b/lib/cErrors.ml
index c1d224dfc..1459141d1 100644
--- a/lib/errors.ml
+++ b/lib/cErrors.ml
@@ -16,6 +16,13 @@ let push = Backtrace.add_backtrace
 
 exception Anomaly of string option * std_ppcmds (* System errors *)
 
+let _ =
+  let pr = function
+  | Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"")
+  | _ -> None
+  in
+  Printexc.register_printer pr
+
 let make_anomaly ?label pp =
   Anomaly (label, pp)
 
@@ -137,5 +144,5 @@ let handled e =
 let fatal_error info anomaly =
   let msg = info ++ fnl () in
   pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg;
-  flush_all ();
+  Format.pp_print_flush !Pp_control.err_ft ();
   exit (if anomaly then 129 else 1)
diff --git a/lib/errors.mli b/lib/cErrors.mli
index e5dad93fd..e5dad93fd 100644
--- a/lib/errors.mli
+++ b/lib/cErrors.mli
diff --git a/lib/cList.ml b/lib/cList.ml
index 0ac372d8d..602bba6a5 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -47,7 +47,11 @@ sig
     ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
   val filteri :
     (int -> 'a -> bool) -> 'a list -> 'a list
+  val partitioni :
+    (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
+  val extend : bool list -> 'a -> 'a list -> 'a list
+  val count : ('a -> bool) -> 'a list -> int
   val index : 'a eq -> 'a -> 'a list -> int
   val index0 : 'a eq -> 'a -> 'a list -> int
   val iteri :  (int -> 'a -> unit) -> 'a list -> unit
@@ -61,6 +65,7 @@ sig
   val except : 'a eq -> 'a -> 'a list -> 'a list
   val remove : 'a eq -> 'a -> 'a list -> 'a list
   val remove_first : ('a -> bool) -> 'a list -> 'a list
+  val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
   val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
   val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
   val sep_last : 'a list -> 'a * 'a list
@@ -375,6 +380,18 @@ let rec smartfilter f l = match l with
           else h :: tl'
         else tl'
 
+let rec extend l a l' = match l,l' with
+  | true::l, b::l' -> b :: extend l a l'
+  | false::l, l' -> a :: extend l a l'
+  | [], [] -> []
+  | _ -> invalid_arg "extend"
+
+let count f l =
+  let rec aux acc = function
+    | [] -> acc
+    | h :: t -> if f h then aux (acc + 1) t else aux acc t in
+  aux 0 l
+
 let rec index_f f x l n = match l with
 | [] -> raise Not_found
 | y :: l -> if f x y then n else index_f f x l (succ n)
@@ -445,6 +462,14 @@ let rec remove_first p = function
   | b::l -> b::remove_first p l
   | [] -> raise Not_found
 
+let extract_first p li =
+  let rec loop rev_left = function
+    | [] -> raise Not_found
+    | x::right ->
+       if p x then List.rev_append rev_left right, x
+       else loop (x :: rev_left) right
+  in loop [] li
+
 let insert p v l =
   let rec insrec = function
     | [] -> [v]
@@ -472,6 +497,15 @@ let filteri p =
   in
   filter_i_rec 0
 
+let partitioni p =
+  let rec aux i = function
+    | [] -> [], []
+    | x :: l ->
+        let (l1, l2) = aux (succ i) l in
+        if p i x then (x :: l1, l2)
+        else (l1, x :: l2)
+  in aux 0
+
 let rec sep_last = function
   | [] -> failwith "sep_last"
   | hd::[] -> (hd,[])
@@ -638,12 +672,13 @@ let rec split3 = function
       let (rx, ry, rz) = split3 l in (x::rx, y::ry, z::rz)
 
 let firstn n l =
-  let rec aux acc = function
-    | (0, l) -> List.rev acc
-    | (n, (h::t)) -> aux (h::acc) (pred n, t)
+  let rec aux acc n l =
+    match n, l with
+    | 0, _ -> List.rev acc
+    | n, h::t -> aux (h::acc) (pred n) t
     | _ -> failwith "firstn"
   in
-  aux [] (n,l)
+  aux [] n l
 
 let rec last = function
   | [] -> failwith "List.last"
diff --git a/lib/cList.mli b/lib/cList.mli
index 19eeb2509..bc8749b4f 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -89,11 +89,17 @@ sig
   val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list ->
     'd list -> 'e list
   val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
+  val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
 
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
   (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
     [f ai = true], then [smartfilter f l == l] *)
 
+  val extend : bool list -> 'a -> 'a list -> 'a list
+(** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n];
+    it extends [a1..an] by inserting [a] at the position of [false] in [l] *)
+  val count : ('a -> bool) -> 'a list -> int
+
   val index : 'a eq -> 'a -> 'a list -> int
   (** [index] returns the 1st index of an element in a list (counting from 1). *)
 
@@ -119,6 +125,10 @@ sig
   val remove_first : ('a -> bool) -> 'a list -> 'a list
   (** Remove the first element satisfying a predicate, or raise [Not_found] *)
 
+  val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
+  (** Remove and return the first element satisfying a predicate,
+      or raise [Not_found] *)
+
   val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
   (** Insert at the (first) position so that if the list is ordered wrt to the
       total order given as argument, the order is preserved *)
diff --git a/lib/cMap.ml b/lib/cMap.ml
index 665e1a216..4b058380c 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -12,12 +12,20 @@ sig
   val compare : t -> t -> int
 end
 
+module type MonadS =
+sig
+  type +'a t
+  val return : 'a -> 'a t
+  val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+end
+
 module type S = Map.S
 
 module type ExtS =
 sig
   include CSig.MapS
   module Set : CSig.SetS with type elt = key
+  val get : key -> 'a t -> 'a
   val update : key -> 'a -> 'a t -> 'a t
   val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t
   val domain : 'a t -> Set.t
@@ -30,6 +38,12 @@ sig
   sig
     val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
   end
+  module Monad(M : MonadS) :
+  sig
+    val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+    val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+    val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+  end
 end
 
 module MapExt (M : Map.OrderedType) :
@@ -47,6 +61,12 @@ sig
   sig
     val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map
   end
+  module Monad(MS : MonadS) :
+  sig
+    val fold : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t
+    val fold_left : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t
+    val fold_right : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t
+  end
 end =
 struct
   (** This unsafe module is a way to access to the actual implementations of
@@ -159,10 +179,34 @@ struct
 
   end
 
+  module Monad(M : MonadS) =
+  struct
+
+    open M
+
+    let rec fold_left f s accu = match map_prj s with
+    | MEmpty -> return accu
+    | MNode (l, k, v, r, h) ->
+      fold_left f l accu >>= fun accu ->
+      f k v accu >>= fun accu ->
+      fold_left f r accu
+
+    let rec fold_right f s accu = match map_prj s with
+    | MEmpty -> return accu
+    | MNode (l, k, v, r, h) ->
+      fold_right f r accu >>= fun accu ->
+      f k v accu >>= fun accu ->
+      fold_right f l accu
+
+    let fold = fold_left
+
+  end
+
 end
 
 module Make(M : Map.OrderedType) =
 struct
   include Map.Make(M)
   include MapExt(M)
+  let get k m = try find k m with Not_found -> assert false
 end
diff --git a/lib/cMap.mli b/lib/cMap.mli
index 2f243da83..3ef7fa2c8 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -14,6 +14,13 @@ sig
   val compare : t -> t -> int
 end
 
+module type MonadS =
+sig
+  type +'a t
+  val return : 'a -> 'a t
+  val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+end
+
 module type S = Map.S
 
 module type ExtS =
@@ -24,6 +31,9 @@ sig
   module Set : CSig.SetS with type elt = key
   (** Sets used by the domain function *)
 
+  val get : key -> 'a t -> 'a
+  (** Same as {!find} but fails an assertion instead of raising [Not_found] *)
+
   val update : key -> 'a -> 'a t -> 'a t
   (** Same as [add], but expects the key to be present, and thus faster.
       @raise Not_found when the key is unbound in the map. *)
@@ -59,6 +69,14 @@ sig
         i.e.: for all (k : key) (x : 'a), compare (fst (f k x)) k = 0. *)
   end
 
+  module Monad(M : MonadS) :
+  sig
+    val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+    val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+    val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+  end
+  (** Fold operators parameterized by any monad. *)
+
 end
 
 module Make(M : Map.OrderedType) : ExtS with
diff --git a/lib/cSig.mli b/lib/cSig.mli
index e095c82cb..151cfbdca 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -14,6 +14,8 @@ type ('a, 'b) union = Inl of 'a | Inr of 'b
 type 'a until = Stop of 'a | Cont of 'a
 (** Used for browsable-until structures. *)
 
+type (_, _) eq = Refl : ('a, 'a) eq
+
 module type SetS =
 sig
     type elt
@@ -46,6 +48,8 @@ end
 (** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml
     documentation for more information. *)
 
+module type EmptyS = sig end
+
 module type MapS =
 sig
     type key
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
new file mode 100644
index 000000000..78fa84f33
--- /dev/null
+++ b/lib/cWarnings.ml
@@ -0,0 +1,120 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+
+type status =
+  Disabled | Enabled | AsError
+
+type t = {
+  default : status;
+  category : string;
+  status : status;
+}
+
+let warnings : (string, t) Hashtbl.t = Hashtbl.create 97
+let categories : (string, string list) Hashtbl.t = Hashtbl.create 97
+
+let current_loc = ref Loc.ghost
+let flags = ref ""
+
+let set_current_loc = (:=) current_loc
+
+let get_flags () = !flags
+
+let add_warning_in_category ~name ~category =
+  let ws =
+    try
+      Hashtbl.find categories category
+    with Not_found -> []
+  in
+  Hashtbl.replace categories category (name::ws)
+
+let create ~name ~category ?(default=Enabled) pp =
+  Hashtbl.add warnings name { default; category; status = default };
+  add_warning_in_category ~name ~category;
+  if default <> Disabled then
+    add_warning_in_category ~name ~category:"default";
+  fun ?loc x -> let w = Hashtbl.find warnings name in
+           match w.status with
+           | Disabled -> ()
+           | AsError ->
+              let loc = Option.default !current_loc loc in
+              CErrors.user_err_loc (loc,"_",pp x)
+           | Enabled ->
+              let msg =
+                pp x ++ spc () ++ str "[" ++ str name ++ str "," ++
+                  str category ++ str "]"
+              in
+              let loc = Option.default !current_loc loc in
+              Feedback.msg_warning ~loc msg
+
+let warn_unknown_warning =
+  create ~name:"unknown-warning" ~category:"toplevel"
+         (fun name -> strbrk "Unknown warning name: " ++ str name)
+
+let set_warning_status ~name status =
+  try
+    let w = Hashtbl.find warnings name in 
+    Hashtbl.replace warnings name { w with status = status }
+  with Not_found -> warn_unknown_warning name
+
+let reset_default_warnings () =
+  Hashtbl.iter (fun name w ->
+                Hashtbl.replace warnings name { w with status = w.default })
+    warnings
+
+let set_all_warnings_status status =
+  Hashtbl.iter (fun name w ->
+                Hashtbl.replace warnings name { w with status })
+    warnings
+
+let parse_flag s =
+  if String.length s > 1 then
+    match String.get s 0 with
+    | '+' -> (AsError, String.sub s 1 (String.length s - 1))
+    | '-' -> (Disabled, String.sub s 1 (String.length s - 1))
+    | _ -> (Enabled, s)
+  else CErrors.error "Invalid warnings flag"
+
+let rec do_all_keyword = function
+  | [] -> []
+  | (status, name as item) :: items -> 
+     if CString.equal name "all" then
+       (set_all_warnings_status status; do_all_keyword items)
+     else item :: do_all_keyword items
+
+let rec do_categories = function
+  | [] -> []
+  | (status, name as item) :: items -> 
+     try
+       let names = Hashtbl.find categories name in
+       List.iter (fun name -> set_warning_status name status) names;
+       do_categories items
+     with Not_found -> item :: do_categories items
+
+let rec parse_warnings items =
+  List.iter (fun (status, name) -> set_warning_status ~name status) items
+
+(* For compatibility, we accept "none" *)
+let parse_flags s = 
+  if CString.equal s "none" then begin
+      Flags.make_warn false;
+      set_all_warnings_status Disabled
+    end
+  else begin
+      Flags.make_warn true;
+      let reg = Str.regexp "[ ,]+" in
+      let items = List.map parse_flag (Str.split reg s) in
+      let items = do_all_keyword items in
+      let items = do_categories items in
+      parse_warnings items
+    end
+
+let set_flags s =
+  flags := s; reset_default_warnings (); parse_flags s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
new file mode 100644
index 000000000..351554284
--- /dev/null
+++ b/lib/cWarnings.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type status =
+  Disabled | Enabled | AsError
+
+(*
+type 'a repr = {
+  print : 'a -> Pp.std_ppcmds;
+  kind : string;
+  enabled : bool;
+}
+ *)
+
+val set_current_loc : Loc.t -> unit
+
+val create : name:string -> category:string -> ?default:status ->
+             ('a -> Pp.std_ppcmds) -> ?loc:Loc.t -> 'a -> unit
+
+(*
+val emit : 'a t -> 'a -> unit
+
+type any = Any : string * string * 'a repr -> any
+
+val dump : unit -> any list
+ *)
+
+val get_flags : unit -> string
+val set_flags : string -> unit
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 9c9607abd..1e33173ee 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -8,6 +8,7 @@ Hashcons
 CSet
 CMap
 Int
+Dyn
 HMap
 Option
 Store
@@ -20,20 +21,16 @@ Control
 Loc
 CList
 CString
-Serialize
 Deque
 CObj
 CArray
 CStack
 Util
 Stateid
-Feedback
 Pp
 Ppstyle
-Xml_lexer
-Xml_parser
-Xml_printer
 Richpp
+Feedback
 CUnix
 Envars
 Aux_file
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 04b32870a..65d1442ac 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -6,12 +6,68 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Pp
+module type TParam =
+sig
+  type 'a t
+end
 
+module type PreS =
+sig
+type 'a tag
+type t = Dyn : 'a tag * 'a -> t
+
+val create : string -> 'a tag
+val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+val repr : 'a tag -> string
+
+type any = Any : 'a tag -> any
+
+val name : string -> any option
+
+module Map(M : TParam) :
+sig
+  type t
+  val empty : t
+  val add : 'a tag -> 'a M.t -> t -> t
+  val remove : 'a tag -> t -> t
+  val find : 'a tag -> t -> 'a M.t
+  val mem : 'a tag -> t -> bool
+
+  type any = Any : 'a tag * 'a M.t -> any
+
+  type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
+  val map : map -> t -> t
+
+  val iter : (any -> unit) -> t -> unit
+  val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
+
+end
+
+val dump : unit -> (int * string) list
+
+end
+
+module type S =
+sig
+  include PreS
+
+  module Easy : sig
+    val make_dyn : string -> ('a -> t) * (t -> 'a)
+    val inj : 'a -> 'a tag -> t
+    val prj : t -> 'a tag -> 'a option
+  end
+
+end
+
+module Make(M : CSig.EmptyS) = struct
+module Self : PreS = struct
 (* Dynamics, programmed with DANGER !!! *)
 
-type t = int * Obj.t
+type 'a tag = int
+
+type t = Dyn : 'a tag * 'a -> t
+
+type any = Any : 'a tag -> any
 
 let dyntab = ref (Int.Map.empty : string Int.Map.t)
 (** Instead of working with tags as strings, which are costly, we use their
@@ -24,27 +80,69 @@ let create (s : string) =
   let () =
     if Int.Map.mem hash !dyntab then
       let old = Int.Map.find hash !dyntab in
-      let msg = str "Dynamic tag collision: " ++ str s ++ str " vs. " ++ str old in
-      anomaly ~label:"Dyn.create" msg
+      let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in
+      assert false
   in
   let () = dyntab := Int.Map.add hash s !dyntab in
-  let infun v = (hash, Obj.repr v) in
-  let outfun (nh, rv) =
-    if Int.equal hash nh then Obj.magic rv
-    else
-      anomaly (str "dyn_out: expected " ++ str s)
-  in
-  (infun, outfun)
+  hash
 
-let has_tag (s, _) tag =
-  let hash = Hashtbl.hash (tag : string) in
-  Int.equal s hash
+let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option =
+  fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None
 
-let tag (s,_) =
+let repr s =
   try Int.Map.find s !dyntab
   with Not_found ->
-    anomaly (str "Unknown dynamic tag " ++ int s)
+    let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in
+    assert false
 
-let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2
+let name s =
+  let hash = Hashtbl.hash s in
+  if Int.Map.mem hash !dyntab then Some (Any hash) else None
 
 let dump () = Int.Map.bindings !dyntab
+
+module Map(M : TParam) =
+struct
+type t = Obj.t M.t Int.Map.t
+let cast : 'a M.t -> 'b M.t = Obj.magic
+let empty = Int.Map.empty
+let add tag v m = Int.Map.add tag (cast v) m
+let remove tag m = Int.Map.remove tag m
+let find tag m = cast (Int.Map.find tag m)
+let mem = Int.Map.mem
+
+type any = Any : 'a tag * 'a M.t -> any
+
+type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
+let map f m = Int.Map.mapi f.map m
+
+let iter f m = Int.Map.iter (fun k v -> f (Any (k, v))) m
+let fold f m accu = Int.Map.fold (fun k v accu -> f (Any (k, v)) accu) m accu
+end
+
+end
+include Self
+
+module Easy = struct
+(* now tags are opaque, we can do the trick *)
+let make_dyn (s : string) =
+ (fun (type a) (tag : a tag) ->
+  let infun : (a -> t) = fun x -> Dyn (tag, x) in
+  let outfun : (t -> a) = fun (Dyn (t, x)) ->
+    match eq tag t with
+    | None -> assert false
+    | Some CSig.Refl -> x
+  in
+  (infun, outfun))
+ (create s)
+
+let inj x tag = Dyn(tag,x)
+let prj : type a. t -> a tag -> a option =
+    fun (Dyn(tag',x)) tag ->
+    match eq tag tag' with
+    | None -> None
+    | Some CSig.Refl -> Some x
+end
+
+end
+
diff --git a/lib/dyn.mli b/lib/dyn.mli
index c040d8b0b..448b11a18 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -6,12 +6,58 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Dynamics. Use with extreme care. Not for kids. *)
+(** Dynamically typed values *)
 
-type t
+module type TParam =
+sig
+  type 'a t
+end
+
+module type S =
+sig
+type 'a tag
+type t = Dyn : 'a tag * 'a -> t
+
+val create : string -> 'a tag
+val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+val repr : 'a tag -> string
+
+type any = Any : 'a tag -> any
+
+val name : string -> any option
+
+module Map(M : TParam) :
+sig
+  type t
+  val empty : t
+  val add : 'a tag -> 'a M.t -> t -> t
+  val remove : 'a tag -> t -> t
+  val find : 'a tag -> t -> 'a M.t
+  val mem : 'a tag -> t -> bool
+
+  type any = Any : 'a tag * 'a M.t -> any
+
+  type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
+  val map : map -> t -> t
+
+  val iter : (any -> unit) -> t -> unit
+  val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
+
+end
 
-val create : string -> ('a -> t) * (t -> 'a)
-val tag : t -> string
-val has_tag : t -> string -> bool
-val pointer_equal : t -> t -> bool
 val dump : unit -> (int * string) list
+
+module Easy : sig
+
+  (* To create a dynamic type on the fly *)
+  val make_dyn : string -> ('a -> t) * (t -> 'a)
+
+  (* For types declared with the [create] function above *)
+  val inj : 'a -> 'a tag -> t
+  val prj : t -> 'a tag -> 'a option
+end
+
+end
+
+(** FIXME: use OCaml 4.02 generative functors when available *)
+module Make(M : CSig.EmptyS) : S
diff --git a/lib/envars.ml b/lib/envars.ml
index 679e3fdfe..89ce52831 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -146,23 +146,12 @@ let coqpath =
 
 let exe s = s ^ Coq_config.exec_extension
 
-let guess_camlbin () = which (user_path ()) (exe "ocamlc")
+let guess_ocamlfind () = which (user_path ()) (exe "ocamlfind")
 
-let camlbin () =
-  if !Flags.camlbin_spec then !Flags.camlbin else
-    if !Flags.boot then Coq_config.camlbin else
-      try guess_camlbin () with Not_found -> Coq_config.camlbin
-
-let ocamlc () = camlbin () / Coq_config.ocamlc
-
-let ocamlopt () = camlbin () / Coq_config.ocamlopt
-
-let camllib () =
-  if !Flags.boot then
-    Coq_config.camllib
-  else
-    let _, res = CUnix.run_command (ocamlc () ^ " -where") in
-    String.strip res
+let ocamlfind () =
+  if !Flags.ocamlfind_spec then !Flags.ocamlfind else
+    if !Flags.boot then Coq_config.ocamlfind else
+      try guess_ocamlfind () / "ocamlfind"  with Not_found -> Coq_config.ocamlfind
 
 (** {2 Camlp4 paths} *)
 
@@ -173,9 +162,7 @@ let camlp4bin () =
     if !Flags.boot then Coq_config.camlp4bin else
       try guess_camlp4bin ()
       with Not_found ->
-        let cb = camlbin () in
-        if Sys.file_exists (cb / exe Coq_config.camlp4) then cb
-        else Coq_config.camlp4bin
+        Coq_config.camlp4bin
 
 let camlp4 () = camlp4bin () / exe Coq_config.camlp4
 
@@ -183,7 +170,7 @@ let camlp4lib () =
   if !Flags.boot then
     Coq_config.camlp4lib
   else
-    let ex, res = CUnix.run_command (camlp4 () ^ " -where") in
+    let ex, res = CUnix.run_command (ocamlfind () ^ " query " ^ Coq_config.camlp4) in
     match ex with
       | Unix.WEXITED 0 -> String.strip res
       | _ -> "/dev/null"
diff --git a/lib/envars.mli b/lib/envars.mli
index d95b6f099..90a42859b 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -47,17 +47,8 @@ val coqroot : string
     the order it gets added to the search path. *)
 val coqpath : string list
 
-(** [camlbin ()] is the path to the ocaml binaries. *)
-val camlbin : unit -> string
-
-(** [camllib ()] is the path to the ocaml standard library. *)
-val camllib : unit -> string
-
-(** [ocamlc ()] is the ocaml bytecode compiler that compiled this Coq. *)
-val ocamlc   : unit -> string
-
-(** [ocamlc ()] is the ocaml native compiler that compiled this Coq. *)
-val ocamlopt : unit -> string
+(** [camlbin ()] is the path to the ocamlfind binary. *)
+val ocamlfind : unit -> string
 
 (** [camlp4bin ()] is the path to the camlp4 binary. *)
 val camlp4bin : unit -> string
diff --git a/lib/explore.ml b/lib/explore.ml
index 587db1156..aa7bddf2b 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -27,7 +27,7 @@ module Make = functor(S : SearchProblem) -> struct
       | [i] -> int i
       | i :: l -> pp_rec l ++ str "." ++ int i
     in
-    msg_debug (h 0 (pp_rec p) ++ pp)
+    Feedback.msg_debug (h 0 (pp_rec p) ++ pp)
 
   (*s Depth first search. *)
 
diff --git a/lib/feedback.ml b/lib/feedback.ml
index cce0c6bc6..0ec3b2ebe 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -7,51 +7,14 @@
 (************************************************************************)
 
 open Xml_datatype
-open Serialize
 
-type message_level =
-  | Debug of string
+type level =
+  | Debug
   | Info
   | Notice
   | Warning
   | Error
 
-type message = {
-  message_level : message_level;
-  message_content : string;
-}
-
-let of_message_level = function
-  | Debug s ->
-      Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s]
-  | Info -> Serialize.constructor "message_level" "info" []
-  | Notice -> Serialize.constructor "message_level" "notice" []
-  | Warning -> Serialize.constructor "message_level" "warning" []
-  | Error -> Serialize.constructor "message_level" "error" []
-let to_message_level =
-  Serialize.do_match "message_level" (fun s args -> match s with
-  | "debug" -> Debug (Serialize.raw_string args)
-  | "info" -> Info
-  | "notice" -> Notice
-  | "warning" -> Warning
-  | "error" -> Error
-  | _ -> raise Serialize.Marshal_error)
-
-let of_message msg =
-  let lvl = of_message_level msg.message_level in
-  let content = Serialize.of_string msg.message_content in
-  Xml_datatype.Element ("message", [], [lvl; content])
-let to_message xml = match xml with
-  | Xml_datatype.Element ("message", [], [lvl; content]) -> {
-      message_level = to_message_level lvl;
-      message_content = Serialize.to_string content }
-  | _ -> raise Serialize.Marshal_error
-
-let is_message = function
-  | Xml_datatype.Element ("message", _, _) -> true
-  | _ -> false
-
-
 type edit_id = int
 type state_id = Stateid.t
 type edit_or_state_id = Edit of edit_id | State of state_id
@@ -61,7 +24,6 @@ type feedback_content =
   | Processed
   | Incomplete
   | Complete
-  | ErrorMsg of Loc.t * string
   | ProcessingIn of string
   | InProgress of int
   | WorkerStatus of string * string
@@ -71,8 +33,10 @@ type feedback_content =
   | GlobDef of Loc.t * string * string * string
   | FileDependency of string option * string
   | FileLoaded of string * string
+  (* Extra metadata *)
   | Custom of Loc.t * string * xml
-  | Message of message
+  (* Generic messages *)
+  | Message of level * Loc.t option * Richpp.richpp
 
 type feedback = {
   id : edit_or_state_id;
@@ -80,92 +44,129 @@ type feedback = {
   route : route_id;
 }
 
-let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
-  | "addedaxiom", _ -> AddedAxiom
-  | "processed", _ -> Processed
-  | "processingin", [where] -> ProcessingIn (to_string where)
-  | "incomplete", _ -> Incomplete
-  | "complete", _ -> Complete
-  | "globref", [loc; filepath; modpath; ident; ty] ->
-       GlobRef(to_loc loc, to_string filepath,
-         to_string modpath, to_string ident, to_string ty)
-  | "globdef", [loc; ident; secpath; ty] ->
-       GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty)
-  | "errormsg", [loc;  s] -> ErrorMsg (to_loc loc, to_string s)
-  | "inprogress", [n] -> InProgress (to_int n)
-  | "workerstatus", [ns] ->
-       let n, s = to_pair to_string to_string ns in
-       WorkerStatus(n,s)
-  | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
-  | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x)
-  | "filedependency", [from; dep] ->
-      FileDependency (to_option to_string from, to_string dep)
-  | "fileloaded", [dirpath; filename] ->
-      FileLoaded (to_string dirpath, to_string filename)
-  | "message", [m] -> Message (to_message m)
-  | _ -> raise Marshal_error)
-let of_feedback_content = function
-  | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
-  | Processed -> constructor "feedback_content" "processed" []
-  | ProcessingIn where ->
-      constructor "feedback_content" "processingin" [of_string where]
-  | Incomplete -> constructor "feedback_content" "incomplete" []
-  | Complete -> constructor "feedback_content" "complete" []
-  | GlobRef(loc, filepath, modpath, ident, ty) ->
-      constructor "feedback_content" "globref" [
-        of_loc loc;
-        of_string filepath;
-        of_string modpath;
-        of_string ident;
-        of_string ty ]
-  | GlobDef(loc, ident, secpath, ty) ->
-      constructor "feedback_content" "globdef" [
-        of_loc loc;
-        of_string ident;
-        of_string secpath;
-        of_string ty ]
-  | ErrorMsg(loc, s) ->
-      constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
-  | InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
-  | WorkerStatus(n,s) ->
-      constructor "feedback_content" "workerstatus"
-        [of_pair of_string of_string (n,s)]
-  | Goals (loc,s) ->
-      constructor "feedback_content" "goals" [of_loc loc;of_string s]
-  | Custom (loc, name, x) ->
-      constructor "feedback_content" "custom" [of_loc loc; of_string name; x]
-  | FileDependency (from, depends_on) ->
-      constructor "feedback_content" "filedependency" [
-        of_option of_string from;
-        of_string depends_on]
-  | FileLoaded (dirpath, filename) ->
-      constructor "feedback_content" "fileloaded" [
-        of_string dirpath;
-        of_string filename ]
-  | Message m -> constructor "feedback_content" "message" [ of_message m ]
-
-let of_edit_or_state_id = function
-  | Edit id -> ["object","edit"], of_edit_id id
-  | State id -> ["object","state"], Stateid.to_xml id
-
-let of_feedback msg =
-  let content = of_feedback_content msg.contents in
-  let obj, id = of_edit_or_state_id msg.id in
-  let route = string_of_int msg.route in
-  Element ("feedback", obj @ ["route",route], [id;content])
-let to_feedback xml = match xml with
-  | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
-      id = Edit(to_edit_id id);
-      route = int_of_string route;
-      contents = to_feedback_content content }
-  | Element ("feedback", ["object","state";"route",route], [id;content]) -> { 
-      id = State(Stateid.of_xml id);
-      route = int_of_string route;
-      contents = to_feedback_content content }
-  | _ -> raise Marshal_error
-
-let is_feedback = function
-  | Element ("feedback", _, _) -> true
-  | _ -> false
-
 let default_route = 0
+
+(** Feedback and logging *)
+open Pp
+open Pp_control
+
+type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
+
+let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ())
+let msgnl          strm = msgnl_with !std_ft strm
+
+(* XXX: This is really painful! *)
+module Emacs = struct
+
+  (* Special chars for emacs, to detect warnings inside goal output *)
+  let emacs_quote_start = String.make 1 (Char.chr 254)
+  let emacs_quote_end   = String.make 1 (Char.chr 255)
+
+  let emacs_quote_err g =
+    hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
+
+  let emacs_quote_info_start = "<infomsg>"
+  let emacs_quote_info_end = "</infomsg>"
+
+  let emacs_quote_info g =
+    hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
+
+end
+
+open Emacs
+
+let  dbg_str = str "Debug:"   ++ spc ()
+let info_str = mt ()
+let warn_str = str "Warning:" ++ spc ()
+let  err_str = str "Error:"   ++ spc ()
+
+let make_body quoter info ?loc s =
+  let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
+  quoter (hov 0 (loc ++ info ++ s))
+
+(* Generic logger *)
+let gen_logger dbg err ?loc level msg = match level with
+  | Debug   -> msgnl (make_body dbg  dbg_str ?loc msg)
+  | Info    -> msgnl (make_body dbg info_str ?loc msg)
+  (* XXX: What to do with loc here? *)
+  | Notice  -> msgnl msg
+  | Warning -> Flags.if_warn (fun () ->
+               msgnl_with !err_ft (make_body err warn_str ?loc msg)) ()
+  | Error   -> msgnl_with !err_ft (make_body err  err_str ?loc msg)
+
+(** Standard loggers *)
+let std_logger  = gen_logger (fun x -> x) (fun x -> x)
+
+(* Color logger *)
+let color_terminal_logger ?loc level strm =
+  let msg  = Ppstyle.color_msg in
+  match level with
+  | Debug   -> msg ?loc ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
+  | Info    -> msg ?loc !std_ft strm
+  | Notice  -> msg ?loc !std_ft strm
+  | Warning -> Flags.if_warn (fun () ->
+               msg ?loc ~header:("Warning", Ppstyle.warning_tag) !err_ft strm) ()
+  | Error   -> msg ?loc ~header:("Error",   Ppstyle.error_tag)   !err_ft strm
+
+(* Rules for emacs:
+   - Debug/info: emacs_quote_info
+   - Warning/Error: emacs_quote_err
+   - Notice: unquoted
+ *)
+let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
+
+let logger       = ref std_logger
+let set_logger l = logger := l
+
+let msg_info    ?loc x = !logger ?loc Info x
+let msg_notice  ?loc x = !logger ?loc Notice x
+let msg_warning ?loc x = !logger ?loc Warning x
+let msg_error   ?loc x = !logger ?loc Error x
+let msg_debug   ?loc x = !logger ?loc Debug x
+
+(** Feeders *)
+let feeder = ref ignore
+let set_feeder f = feeder := f
+
+let feedback_id    = ref (Edit 0)
+let feedback_route = ref default_route
+
+let set_id_for_feedback ?(route=default_route) i =
+  feedback_id := i; feedback_route := route
+
+let feedback ?id ?route what =
+  !feeder {
+     contents = what;
+     route = Option.default !feedback_route route;
+     id    = Option.default !feedback_id id;
+  }
+
+let feedback_logger ?loc lvl msg =
+  feedback ~route:!feedback_route ~id:!feedback_id
+    (Message (lvl, loc, Richpp.richpp_of_pp msg))
+
+(* Output to file *)
+let ft_logger old_logger ft ?loc level mesg =
+  let id x = x in
+  match level with
+  | Debug   -> msgnl_with ft (make_body id  dbg_str mesg)
+  | Info    -> msgnl_with ft (make_body id info_str mesg)
+  | Notice  -> msgnl_with ft mesg
+  | Warning -> old_logger ?loc level mesg
+  | Error   -> old_logger ?loc level mesg
+
+let with_output_to_file fname func input =
+  let old_logger = !logger in
+  let channel = open_out (String.concat "." [fname; "out"]) in
+  logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
+  try
+    let output = func input in
+    logger := old_logger;
+    close_out channel;
+    output
+  with reraise ->
+    let reraise = Backtrace.add_backtrace reraise in
+    logger := old_logger;
+    close_out channel;
+    Exninfo.iraise reraise
+
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 162867626..d72524e65 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -9,27 +9,19 @@
 open Xml_datatype
 
 (* Old plain messages (used to be in Pp) *)
-type message_level =
-  | Debug of string
+type level =
+  | Debug
   | Info
   | Notice
   | Warning
   | Error
 
-type message = {
-  message_level : message_level;
-  message_content : string;
-}
-
-val of_message : message -> xml
-val to_message : xml -> message
-val is_message : xml -> bool
-
 
 (** Coq "semantic" infos obtained during parsing/execution *)
 type edit_id = int
 type state_id = Stateid.t
 type edit_or_state_id = Edit of edit_id | State of state_id
+
 type route_id = int
 
 val default_route : route_id
@@ -39,7 +31,6 @@ type feedback_content =
   | Processed
   | Incomplete
   | Complete
-  | ErrorMsg of Loc.t * string
   (* STM optional data *)
   | ProcessingIn of string
   | InProgress of int
@@ -53,16 +44,89 @@ type feedback_content =
   | FileLoaded of string * string
   (* Extra metadata *)
   | Custom of Loc.t * string * xml
-  (* Old generic messages *)
-  | Message of message
+  (* Generic messages *)
+  | Message of level * Loc.t option * Richpp.richpp
 
 type feedback = {
-  id : edit_or_state_id;       (* The document part concerned *)
+  id       : edit_or_state_id;  (* The document part concerned *)
   contents : feedback_content;  (* The payload *)
-  route : route_id;            (* Extra routing info *)
+  route    : route_id;          (* Extra routing info *)
 }
 
-val of_feedback : feedback -> xml
-val to_feedback : xml -> feedback
-val is_feedback : xml -> bool
+(** {6 Feedback sent, even asynchronously, to the user interface} *)
+
+(** Moved here from pp.ml *)
+
+(* Morally the parser gets a string and an edit_id, and gives back an AST.
+ * Feedbacks during the parsing phase are attached to this edit_id.
+ * The interpreter assignes an exec_id to the ast, and feedbacks happening
+ * during interpretation are attached to the exec_id.
+ * Only one among state_id and edit_id can be provided. *)
+
+(** A [logger] takes a level plus a pretty printing doc and logs it *)
+type logger = ?loc:Loc.t -> level -> Pp.std_ppcmds -> unit
+
+(** [set_logger l] makes the [msg_*] to use [l] for logging *)
+val set_logger : logger -> unit
+
+(** [std_logger] standard logger to [stdout/stderr]  *)
+val std_logger : logger
+
+val color_terminal_logger : logger
+(* This logger will apply the proper {!Pp_style} tags, and in
+   particular use the formatters {!Pp_control.std_ft} and
+   {!Pp_control.err_ft} to display those messages. Be careful this is
+   not compatible with the Emacs mode!  *)
+
+(** [feedback_logger] will produce feedback messages instead IO events *)
+val feedback_logger : logger
+val emacs_logger    : logger
+
+
+(** [set_feeder] A feeder processes the feedback, [ignore] by default *)
+val set_feeder : (feedback -> unit) -> unit
+
+(** [feedback ?id ?route fb] produces feedback fb, with [route] and
+    [id] set appropiatedly, if absent, it will use the defaults set by
+    [set_id_for_feedback] *)
+val feedback :
+  ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit
+
+(** [set_id_for_feedback route id] Set the defaults for feedback *)
+val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
+
+(** [with_output_to_file file f x] executes [f x] with logging
+    redirected to a file [file] *)
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+
+(** {6 output functions}
+
+[msg_notice] do not put any decoration on output by default. If
+possible don't mix it with goal output (prefer msg_info or
+msg_warning) so that interfaces can dispatch outputs easily. Once all
+interfaces use the xml-like protocol this constraint can be
+relaxed. *)
+(* Should we advertise these functions more? Should they be the ONLY
+   allowed way to output something? *)
+
+val msg_info : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+(** Message that displays information, usually in verbose mode, such as [Foobar
+    is defined] *)
+
+val msg_notice : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
+
+val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+(** Message indicating that something went wrong, but without serious
+    consequences. *)
+
+val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+(** Message indicating that something went really wrong, though still
+    recoverable; otherwise an exception would have been raised. *)
+
+val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+(** For debugging purposes *)
+
+
+
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 2c23ec984..13525165a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -47,6 +47,7 @@ let batch_mode = ref false
 
 type compilation_mode = BuildVo | BuildVio | Vio2Vo
 let compilation_mode = ref BuildVo
+let compilation_output_name = ref None
 
 let test_mode = ref false
 
@@ -68,11 +69,15 @@ let priority_of_string = function
   | "low" -> Low
   | "high" -> High
   | _ -> raise (Invalid_argument "priority_of_string")
+type tac_error_filter = [ `None | `Only of string list | `All ]
+let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "curly" ])
+let async_proofs_cmd_error_resilience = ref true
 
 let async_proofs_is_worker () =
   !async_proofs_worker_id <> "master"
 let async_proofs_is_master () =
   !async_proofs_mode = APon && !async_proofs_worker_id = "master"
+let async_proofs_delegation_threshold = ref 0.03
 
 let debug = ref false
 let in_debugger = ref false
@@ -103,18 +108,20 @@ let we_are_parsing = ref false
 (* Current means no particular compatibility consideration.
    For correct comparisons, this constructor should remain the last one. *)
 
-type compat_version = V8_2 | V8_3 | V8_4 | Current
+type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current
 
 let compat_version = ref Current
 
 let version_strictly_greater v = match !compat_version, v with
-| V8_2, (V8_2 | V8_3 | V8_4 | Current) -> false
-| V8_3, (V8_3 | V8_4 | Current) -> false
-| V8_4, (V8_4 | Current) -> false
+| V8_2, (V8_2 | V8_3 | V8_4 | V8_5 | Current) -> false
+| V8_3, (V8_3 | V8_4 | V8_5 | Current) -> false
+| V8_4, (V8_4 | V8_5 | Current) -> false
+| V8_5, (V8_5 | Current) -> false
 | Current, Current -> false
 | V8_3, V8_2 -> true
 | V8_4, (V8_2 | V8_3) -> true
-| Current, (V8_2 | V8_3 | V8_4) -> true
+| V8_5, (V8_2 | V8_3 | V8_4) -> true
+| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> true
 
 let version_less_or_equal v = not (version_strictly_greater v)
 
@@ -122,6 +129,7 @@ let pr_version = function
   | V8_2 -> "8.2"
   | V8_3 -> "8.3"
   | V8_4 -> "8.4"
+  | V8_5 -> "8.5"
   | Current -> "current"
 
 (* Translate *)
@@ -164,7 +172,7 @@ let make_polymorphic_flag b =
 let program_mode = ref false
 let is_program_mode () = !program_mode
 
-let warn = ref false
+let warn = ref true
 let make_warn flag = warn := flag;  ()
 let if_warn f x = if !warn then f x
 
@@ -195,9 +203,9 @@ let is_standard_doc_url url =
 let coqlib_spec = ref false
 let coqlib = ref "(not initialized yet)"
 
-(* Options for changing camlbin (used by coqmktop) *)
-let camlbin_spec = ref false
-let camlbin = ref Coq_config.camlbin
+(* Options for changing ocamlfind (used by coqmktop) *)
+let ocamlfind_spec = ref false
+let ocamlfind = ref Coq_config.camlbin
 
 (* Options for changing camlp4bin (used by coqmktop) *)
 let camlp4bin_spec = ref false
@@ -217,6 +225,7 @@ let native_compiler = ref false
 let print_mod_uid = ref false
 
 let tactic_context_compat = ref false
+let profile_ltac = ref false
 
 let dump_bytecode = ref false
 let set_dump_bytecode = (:=) dump_bytecode
diff --git a/lib/flags.mli b/lib/flags.mli
index 69caad5b6..8fe64d24f 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -14,6 +14,7 @@ val load_init : bool ref
 val batch_mode : bool ref
 type compilation_mode = BuildVo | BuildVio | Vio2Vo
 val compilation_mode : compilation_mode ref
+val compilation_output_name : string option ref
 
 val test_mode : bool ref
 
@@ -34,6 +35,10 @@ type priority = Low | High
 val async_proofs_worker_priority : priority ref
 val string_of_priority : priority -> string
 val priority_of_string : string -> priority
+type tac_error_filter = [ `None | `Only of string list | `All ]
+val async_proofs_tac_error_resilience : tac_error_filter ref
+val async_proofs_cmd_error_resilience : bool ref
+val async_proofs_delegation_threshold : float ref
 
 val debug : bool ref
 val in_debugger : bool ref
@@ -57,7 +62,7 @@ val raw_print : bool ref
 val record_print : bool ref
 val univ_print : bool ref
 
-type compat_version = V8_2 | V8_3 | V8_4 | Current
+type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current
 val compat_version : compat_version ref
 val version_strictly_greater : compat_version -> bool
 val version_less_or_equal : compat_version -> bool
@@ -123,8 +128,8 @@ val coqlib_spec : bool ref
 val coqlib : string ref
 
 (** Options for specifying where OCaml binaries reside *)
-val camlbin_spec : bool ref
-val camlbin : string ref
+val ocamlfind_spec : bool ref
+val ocamlfind : string ref
 val camlp4bin_spec : bool ref
 val camlp4bin : string ref
 
@@ -143,6 +148,8 @@ val tactic_context_compat : bool ref
 (** Set to [true] to trigger the compatibility bugged context matching (old
     context vs. appcontext) is set. *)
 
+val profile_ltac : bool ref
+
 (** Dump the bytecode after compilation (for debugging purposes) *)
 val dump_bytecode : bool ref
 val set_dump_bytecode : bool -> unit
diff --git a/lib/future.ml b/lib/future.ml
index e8f33db5e..ea0382a63 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -7,8 +7,9 @@
 (************************************************************************)
 
 (* To deal with side effects we have to save/restore the system state *)
-let freeze = ref (fun () -> assert false : unit -> Dyn.t)
-let unfreeze = ref (fun _ -> () : Dyn.t -> unit)
+type freeze
+let freeze = ref (fun () -> assert false : unit -> freeze)
+let unfreeze = ref (fun _ -> () : freeze -> unit)
 let set_freeze f g = freeze := f; unfreeze := g
 
 let not_ready_msg = ref (fun name ->
@@ -29,10 +30,10 @@ let customize_not_here_msg f = not_here_msg := f
 
 exception NotReady of string
 exception NotHere of string
-let _ = Errors.register_handler (function
+let _ = CErrors.register_handler (function
   | NotReady name -> !not_ready_msg name
   | NotHere name -> !not_here_msg name
-  | _ -> raise Errors.Unhandled)
+  | _ -> raise CErrors.Unhandled)
 
 type fix_exn = Exninfo.iexn -> Exninfo.iexn
 let id x = prerr_endline "Future: no fix_exn.\nYou have probably created a Future.computation from a value without passing the ~fix_exn argument.  You probably want to chain with an already existing future instead."; x
@@ -58,7 +59,7 @@ type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computat
 and 'a comp =
   | Delegated of (unit -> unit)
   | Closure of (unit -> 'a)
-  | Val of 'a * Dyn.t option
+  | Val of 'a * freeze option
   | Exn of Exninfo.iexn  (* Invariant: this exception is always "fixed" as in fix_exn *)
 
 and 'a comput =
@@ -135,7 +136,7 @@ let rec compute ~pure ck : 'a value =
         let state = if pure then None else Some (!freeze ()) in
         c := Val (data, state); `Val data
       with e ->
-        let e = Errors.push e in
+        let e = CErrors.push e in
         let e = fix_exn e in
         match e with
         | (NotReady _, _) -> `Exn e
@@ -155,9 +156,9 @@ let chain ~pure ck f =
   | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v)
   | Val (v, None) ->
       match !ck with
-      | Finished _ -> Errors.anomaly(Pp.str
+      | Finished _ -> CErrors.anomaly(Pp.str
           "Future.chain ~pure:false call on an already joined computation")
-      | Ongoing _ -> Errors.anomaly(Pp.strbrk(
+      | Ongoing _ -> CErrors.anomaly(Pp.strbrk(
           "Future.chain ~pure:false call on a pure computation. "^
           "This can happen if the computation was initial created with "^
           "Future.from_val or if it was Future.chain ~pure:true with a "^
@@ -169,7 +170,7 @@ let replace kx y =
   let _, _, _, x = get kx in
   match !x with
   | Exn _ -> x := Closure (fun () -> force ~pure:false y)
-  | _ -> Errors.anomaly
+  | _ -> CErrors.anomaly
            (Pp.str "A computation can be replaced only if is_exn holds")
 
 let purify f x =
@@ -179,13 +180,13 @@ let purify f x =
     !unfreeze state;
     v
   with e ->
-    let e = Errors.push e in !unfreeze state; Exninfo.iraise e
+    let e = CErrors.push e in !unfreeze state; Exninfo.iraise e
 
 let transactify f x =
   let state = !freeze () in
   try f x
   with e ->
-    let e = Errors.push e in !unfreeze state; Exninfo.iraise e
+    let e = CErrors.push e in !unfreeze state; Exninfo.iraise e
 
 let purify_future f x = if is_over x then f x else purify f x
 let compute x = purify_future (compute ~pure:false) x
@@ -212,7 +213,7 @@ let map2 ?greedy f x l =
     let xi = chain ?greedy ~pure:true x (fun x ->
         try List.nth x i
         with Failure _ | Invalid_argument _ ->
-          Errors.anomaly (Pp.str "Future.map2 length mismatch")) in
+          CErrors.anomaly (Pp.str "Future.map2 length mismatch")) in
     f xi y) 0 l
 
 let print f kx =
diff --git a/lib/future.mli b/lib/future.mli
index 58f0a71ad..114c59176 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -157,10 +157,11 @@ val transactify : ('a -> 'b) -> 'a -> 'b
 (** Debug: print a computation given an inner printing function. *)
 val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds
 
+type freeze
 (* These functions are needed to get rid of side effects.
    Thy are set for the outermos layer of the system, since they have to
    deal with the whole system state. *)
-val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
+val set_freeze : (unit -> freeze) -> (freeze -> unit) -> unit
 
 val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit
 val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit
diff --git a/lib/genarg.ml b/lib/genarg.ml
index cba54c114..05c828d5f 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -9,168 +9,160 @@
 open Pp
 open Util
 
-type argument_type =
-  (* Basic types *)
-  | IntOrVarArgType
-  | IdentArgType
-  | VarArgType
-  (* Specific types *)
-  | GenArgType
-  | ConstrArgType
-  | ConstrMayEvalArgType
-  | QuantHypArgType
-  | OpenConstrArgType
-  | ConstrWithBindingsArgType
-  | BindingsArgType
-  | RedExprArgType
-  | ListArgType of argument_type
-  | OptArgType of argument_type
-  | PairArgType of argument_type * argument_type
-  | ExtraArgType of string
-
-let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
-| IntOrVarArgType, IntOrVarArgType -> true
-| IdentArgType, IdentArgType -> true
-| VarArgType, VarArgType -> true
-| GenArgType, GenArgType -> true
-| ConstrArgType, ConstrArgType -> true
-| ConstrMayEvalArgType, ConstrMayEvalArgType -> true
-| QuantHypArgType, QuantHypArgType -> true
-| OpenConstrArgType, OpenConstrArgType -> true
-| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true
-| BindingsArgType, BindingsArgType -> true
-| RedExprArgType, RedExprArgType -> true
-| ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2
-| OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2
-| PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) ->
-  argument_type_eq arg1l arg2l && argument_type_eq arg1r arg2r
-| ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2
-| _ -> false
-
-let rec pr_argument_type = function
-| IntOrVarArgType -> str "int_or_var"
-| IdentArgType -> str "ident"
-| VarArgType -> str "var"
-| GenArgType -> str "genarg"
-| ConstrArgType -> str "constr"
-| ConstrMayEvalArgType -> str "constr_may_eval"
-| QuantHypArgType -> str "qhyp"
-| OpenConstrArgType -> str "open_constr"
-| ConstrWithBindingsArgType -> str "constr_with_bindings"
-| BindingsArgType -> str "bindings"
-| RedExprArgType -> str "redexp"
-| ListArgType t -> pr_argument_type t ++ spc () ++ str "list"
-| OptArgType t -> pr_argument_type t ++ spc () ++ str "opt"
-| PairArgType (t1, t2) ->
-    str "("++ pr_argument_type t1 ++ spc () ++
-    str "*" ++ spc () ++ pr_argument_type t2 ++ str ")"
-| ExtraArgType s -> str s
-
-type ('raw, 'glob, 'top) genarg_type = argument_type
+module ArgT =
+struct
+  module DYN = Dyn.Make(struct end)
+  module Map = DYN.Map
+  type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag
+  type any = Any : ('a, 'b, 'c) tag -> any
+  let eq = DYN.eq
+  let repr = DYN.repr
+  let create = DYN.create
+  let name s = match DYN.name s with
+  | None -> None
+  | Some (DYN.Any t) ->
+    Some (Any (Obj.magic t)) (** All created tags are made of triples *)
+end
+
+type (_, _, _) genarg_type =
+| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
+| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
+| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
+| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type ->
+  ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
+
+type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type
+
+let rec genarg_type_eq : type a1 a2 b1 b2 c1 c2.
+  (a1, b1, c1) genarg_type -> (a2, b2, c2) genarg_type ->
+  (a1 * b1 * c1, a2 * b2 * c2) CSig.eq option =
+fun t1 t2 -> match t1, t2 with
+| ExtraArg t1, ExtraArg t2 -> ArgT.eq t1 t2
+| ListArg t1, ListArg t2 ->
+  begin match genarg_type_eq t1 t2 with
+  | None -> None
+  | Some Refl -> Some Refl
+  end
+| OptArg t1, OptArg t2 ->
+  begin match genarg_type_eq t1 t2 with
+  | None -> None
+  | Some Refl -> Some Refl
+  end
+| PairArg (t1, u1), PairArg (t2, u2) ->
+  begin match genarg_type_eq t1 t2 with
+  | None -> None
+  | Some Refl ->
+    match genarg_type_eq u1 u2 with
+    | None -> None
+    | Some Refl -> Some Refl
+  end
+| _ -> None
+
+let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> std_ppcmds = function
+| ListArg t -> pr_genarg_type t ++ spc () ++ str "list"
+| OptArg t -> pr_genarg_type t ++ spc () ++ str "opt"
+| PairArg (t1, t2) ->
+    str "("++ pr_genarg_type t1 ++ spc () ++
+    str "*" ++ spc () ++ pr_genarg_type t2 ++ str ")"
+| ExtraArg s -> str (ArgT.repr s)
+
+let argument_type_eq arg1 arg2 = match arg1, arg2 with
+| ArgumentType t1, ArgumentType t2 ->
+  match genarg_type_eq t1 t2 with
+  | None -> false
+  | Some Refl -> true
+
+let pr_argument_type (ArgumentType t) = pr_genarg_type t
 
 type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
 (** Alias for concision *)
 
 (* Dynamics but tagged by a type expression *)
 
-type rlevel
-type glevel
-type tlevel
+type rlevel = [ `rlevel ]
+type glevel = [ `glevel ]
+type tlevel = [ `tlevel ]
+
+type (_, _) abstract_argument_type =
+| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
+| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
+| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
+
+type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument
 
-type 'a generic_argument = argument_type * Obj.t
 type raw_generic_argument = rlevel generic_argument
 type glob_generic_argument = glevel generic_argument
 type typed_generic_argument = tlevel generic_argument
 
-let rawwit t = t
-let glbwit t = t
-let topwit t = t
-
-let wit_list t = ListArgType t
+let rawwit t = Rawwit t
+let glbwit t = Glbwit t
+let topwit t = Topwit t
+
+let wit_list t = ListArg t
+
+let wit_opt t = OptArg t
+
+let wit_pair t1 t2 = PairArg (t1, t2)
+
+let in_gen t o = GenArg (t, o)
+
+let abstract_argument_type_eq :
+  type a b l. (a, l) abstract_argument_type -> (b, l) abstract_argument_type -> (a, b) CSig.eq option =
+  fun t1 t2 -> match t1, t2 with
+  | Rawwit t1, Rawwit t2 ->
+    begin match genarg_type_eq t1 t2 with
+    | None -> None
+    | Some Refl -> Some Refl
+    end
+  | Glbwit t1, Glbwit t2 ->
+    begin match genarg_type_eq t1 t2 with
+    | None -> None
+    | Some Refl -> Some Refl
+    end
+  | Topwit t1, Topwit t2 ->
+    begin match genarg_type_eq t1 t2 with
+    | None -> None
+    | Some Refl -> Some Refl
+    end
+
+let out_gen (type a) (type l) (t : (a, l) abstract_argument_type) (o : l generic_argument) : a =
+  let GenArg (t', v) = o in
+  match abstract_argument_type_eq t t' with
+  | None -> failwith "out_gen"
+  | Some Refl -> v
+
+let has_type (GenArg (t, v)) u = match abstract_argument_type_eq t u with
+| None -> false
+| Some _ -> true
+
+let unquote : type l. (_, l) abstract_argument_type -> _ = function
+| Rawwit t -> ArgumentType t
+| Glbwit t -> ArgumentType t
+| Topwit t -> ArgumentType t
+
+let genarg_tag (GenArg (t, _)) = unquote t
 
-let wit_opt t = OptArgType t
-
-let wit_pair t1 t2 = PairArgType (t1,t2)
-
-let in_gen t o = (t,Obj.repr o)
-let out_gen t (t',o) = if argument_type_eq t t' then Obj.magic o else failwith "out_gen"
-let genarg_tag (s,_) = s
-
-let has_type (t, v) u = argument_type_eq t u
-
-let unquote x = x
-
-type ('a,'b) abstract_argument_type = argument_type
 type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
 type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
 type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
 
-type ('a, 'b, 'c, 'l) cast = Obj.t
-
-let raw = Obj.obj
-let glb = Obj.obj
-let top = Obj.obj
-
-type ('r, 'l) unpacker =
-  { unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r }
-
-let unpack pack (t, obj) = pack.unpacker t (Obj.obj obj)
-
-(** Type transformers *)
-
-type ('r, 'l) list_unpacker =
-  { list_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
-    ('a list, 'b list, 'c list, 'l) cast -> 'r }
-
-let list_unpack pack (t, obj) = match t with
-| ListArgType t -> pack.list_unpacker t (Obj.obj obj)
-| _ -> failwith "out_gen"
-
-type ('r, 'l) opt_unpacker =
-  { opt_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
-    ('a option, 'b option, 'c option, 'l) cast -> 'r }
-
-let opt_unpack pack (t, obj) = match t with
-| OptArgType t -> pack.opt_unpacker t (Obj.obj obj)
-| _ -> failwith "out_gen"
-
-type ('r, 'l) pair_unpacker =
-  { pair_unpacker : 'a1 'a2 'b1 'b2 'c1 'c2.
-    ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
-    (('a1 * 'a2), ('b1 * 'b2), ('c1 * 'c2), 'l) cast -> 'r }
-
-let pair_unpack pack (t, obj) = match t with
-| PairArgType (t1, t2) -> pack.pair_unpacker t1 t2 (Obj.obj obj)
-| _ -> failwith "out_gen"
-
 (** Creating args *)
 
-let (arg0_map : Obj.t option String.Map.t ref) = ref String.Map.empty
+module type Param = sig type ('raw, 'glb, 'top) t end
+module ArgMap(M : Param) =
+struct
+  type _ pack = Pack : ('raw, 'glb, 'top) M.t -> ('raw * 'glb * 'top) pack
+  include ArgT.Map(struct type 'a t = 'a pack end)
+end
 
-let create_arg opt name =
-  if String.Map.mem name !arg0_map then
-    Errors.anomaly (str "generic argument already declared: " ++ str name)
-  else
-    let () = arg0_map := String.Map.add name (Obj.magic opt) !arg0_map in
-    ExtraArgType name
+let create_arg name =
+  match ArgT.name name with
+  | None -> ExtraArg (ArgT.create name)
+  | Some _ ->
+    CErrors.anomaly (str "generic argument already declared: " ++ str name)
 
 let make0 = create_arg
 
-let default_empty_value t =
-  let rec aux = function
-  | ListArgType _ -> Some (Obj.repr [])
-  | OptArgType _ -> Some (Obj.repr None)
-  | PairArgType(t1, t2) ->
-      (match aux t1, aux t2 with
-      | Some v1, Some v2 -> Some (Obj.repr (v1, v2))
-      | _ -> None)
-  | ExtraArgType s ->
-    String.Map.find s !arg0_map
-  | _ -> None in
-  match aux t with
-  | Some v -> Some (Obj.obj v)
-  | None -> None
-
 (** Registering genarg-manipulating functions *)
 
 module type GenObj =
@@ -182,54 +174,31 @@ end
 
 module Register (M : GenObj) =
 struct
-  let arg0_map =
-    ref (String.Map.empty : (Obj.t, Obj.t, Obj.t) M.obj String.Map.t)
+  module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end)
+  let arg0_map = ref GenMap.empty
 
   let register0 arg f = match arg with
-  | ExtraArgType s ->
-    if String.Map.mem s !arg0_map then
-      let msg = str M.name ++ str " function already registered: " ++ str s in
-      Errors.anomaly msg
+  | ExtraArg s ->
+    if GenMap.mem s !arg0_map then
+      let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) in
+      CErrors.anomaly msg
     else
-      arg0_map := String.Map.add s (Obj.magic f) !arg0_map
+      arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map
   | _ -> assert false
 
   let get_obj0 name =
-    try String.Map.find name !arg0_map
+    try
+      let GenMap.Pack obj = GenMap.find name !arg0_map in obj
     with Not_found ->
-      match M.default (ExtraArgType name) with
+      match M.default (ExtraArg name) with
       | None ->
-        Errors.anomaly (str M.name ++ str " function not found: " ++ str name)
+        CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name))
       | Some obj -> obj
 
   (** For now, the following function is quite dummy and should only be applied
       to an extra argument type, otherwise, it will badly fail. *)
   let obj t = match t with
-  | ExtraArgType s -> Obj.magic (get_obj0 s)
+  | ExtraArg s -> get_obj0 s
   | _ -> assert false
 
 end
-
-(** Hackish part *)
-
-let arg0_names = ref (String.Map.empty : string String.Map.t)
-(** We use this table to associate a name to a given witness, to use it with
-    the extension mechanism. This is REALLY ad-hoc, but I do not know how to
-    do so nicely either. *)
-
-let register_name0 t name = match t with
-| ExtraArgType s ->
-  let () = assert (not (String.Map.mem s !arg0_names)) in
-  arg0_names := String.Map.add s name !arg0_names
-| _ -> failwith "register_name0"
-
-let get_name0 name =
-  String.Map.find name !arg0_names
-
-module Unsafe =
-struct
-
-let inj tpe x = (tpe, x)
-let prj (_, x) = x
-
-end
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 671d96b7b..d7ad9b93b 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Generic arguments used by the extension mechanisms of several Coq ASTs. *)
+
 (** The route of a generic argument, from parsing to evaluation.
 In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
 
@@ -34,69 +36,57 @@ In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
 effective use
 {% \end{%}verbatim{% }%}
 
-To distinguish between the uninterpreted (raw), globalized and
+To distinguish between the uninterpreted, globalized and
 interpreted worlds, we annotate the type [generic_argument] by a
-phantom argument which is either [constr_expr], [glob_constr] or
-[constr].
+phantom argument.
 
-Transformation for each type :
-{% \begin{%}verbatim{% }%}
-tag                            raw open type            cooked closed type
-
-BoolArgType                    bool                      bool
-IntArgType                     int                       int
-IntOrVarArgType                int or_var                int
-StringArgType                  string (parsed w/ "")     string
-PreIdentArgType                string (parsed w/o "")    (vernac only)
-IdentArgType true              identifier                identifier
-IdentArgType false             identifier (pattern_ident) identifier
-IntroPatternArgType            intro_pattern_expr        intro_pattern_expr
-VarArgType                     identifier located        identifier
-RefArgType                     reference                 global_reference
-QuantHypArgType                quantified_hypothesis     quantified_hypothesis
-ConstrArgType                  constr_expr               constr
-ConstrMayEvalArgType           constr_expr may_eval      constr
-OpenConstrArgType              open_constr_expr          open_constr
-ConstrWithBindingsArgType      constr_expr with_bindings constr with_bindings
-BindingsArgType                constr_expr bindings      constr bindings
-List0ArgType of argument_type
-List1ArgType of argument_type
-OptArgType of argument_type
-ExtraArgType of string         '_a                      '_b
-{% \end{%}verbatim{% }%}
 *)
 
 (** {5 Generic types} *)
 
-type ('raw, 'glob, 'top) genarg_type
-(** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized
-    one, and ['top] the internalized one. *)
+module ArgT :
+sig
+  type ('a, 'b, 'c) tag
+  val eq : ('a1, 'b1, 'c1) tag -> ('a2, 'b2, 'c2) tag -> ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option
+  val repr : ('a, 'b, 'c) tag -> string
+  type any = Any : ('a, 'b, 'c) tag -> any
+  val name : string -> any option
+end
+
+(** Generic types. The first parameter is the OCaml lowest level, the second one
+    is the globalized level, and third one the internalized level. *)
+type (_, _, _) genarg_type =
+| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
+| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
+| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
+| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type ->
+  ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
 
 type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
 (** Alias for concision when the three types agree. *)
 
-val make0 : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type
+val make0 : string -> ('raw, 'glob, 'top) genarg_type
 (** Create a new generic type of argument: force to associate
     unique ML types at each of the three levels. *)
 
-val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type
+val create_arg : string -> ('raw, 'glob, 'top) genarg_type
 (** Alias for [make0]. *)
 
 (** {5 Specialized types} *)
 
 (** All of [rlevel], [glevel] and [tlevel] must be non convertible
-   to ensure the injectivity of the type inference from type
-   ['co generic_argument] to [('a,'co) abstract_argument_type];
-   this guarantees that, for 'co fixed, the type of
-   out_gen is monomorphic over 'a, hence type-safe
-*)
+    to ensure the injectivity of the GADT type inference. *)
 
-type rlevel
-type glevel
-type tlevel
+type rlevel = [ `rlevel ]
+type glevel = [ `glevel ]
+type tlevel = [ `tlevel ]
 
-type ('a, 'co) abstract_argument_type
-(** Type at level ['co] represented by an OCaml value of type ['a]. *)
+(** Generic types at a fixed level. The first parameter embeds the OCaml type
+    and the second one the level. *)
+type (_, _) abstract_argument_type =
+| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
+| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
+| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
 
 type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type
 (** Specialized type at raw level. *)
@@ -120,7 +110,7 @@ val topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
 
 (** {5 Generic arguments} *)
 
-type 'a generic_argument
+type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument
 (** A inhabitant of ['level generic_argument] is a inhabitant of some type at
     level ['level], together with the representation of this type. *)
 
@@ -141,66 +131,20 @@ val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool
 (** [has_type v t] tells whether [v] has type [t]. If true, it ensures that
     [out_gen t v] will not raise a dynamic type exception. *)
 
-(** {6 Destructors} *)
-
-type ('a, 'b, 'c, 'l) cast
-
-val raw : ('a, 'b, 'c, rlevel) cast -> 'a
-val glb : ('a, 'b, 'c, glevel) cast -> 'b
-val top : ('a, 'b, 'c, tlevel) cast -> 'c
-
-type ('r, 'l) unpacker =
-  { unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r }
-
-val unpack : ('r, 'l) unpacker -> 'l generic_argument -> 'r
-(** Existential-type destructors. *)
-
-(** {6 Manipulation of generic arguments}
-
-Those functions fail if they are applied to an argument which has not the right
-dynamic type. *)
-
-type ('r, 'l) list_unpacker =
-  { list_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
-    ('a list, 'b list, 'c list, 'l) cast -> 'r }
-
-val list_unpack : ('r, 'l) list_unpacker -> 'l generic_argument -> 'r
-
-type ('r, 'l) opt_unpacker =
-  { opt_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
-    ('a option, 'b option, 'c option, 'l) cast -> 'r }
-
-val opt_unpack : ('r, 'l) opt_unpacker -> 'l generic_argument -> 'r
-
-type ('r, 'l) pair_unpacker =
-  { pair_unpacker : 'a1 'a2 'b1 'b2 'c1 'c2.
-    ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
-    (('a1 * 'a2), ('b1 * 'b2), ('c1 * 'c2), 'l) cast -> 'r }
-
-val pair_unpack : ('r, 'l) pair_unpacker -> 'l generic_argument -> 'r
-
 (** {6 Type reification} *)
 
-type argument_type =
-  (** Basic types *)
-  | IntOrVarArgType
-  | IdentArgType
-  | VarArgType
-  (** Specific types *)
-  | GenArgType
-  | ConstrArgType
-  | ConstrMayEvalArgType
-  | QuantHypArgType
-  | OpenConstrArgType
-  | ConstrWithBindingsArgType
-  | BindingsArgType
-  | RedExprArgType
-  | ListArgType of argument_type
-  | OptArgType of argument_type
-  | PairArgType of argument_type * argument_type
-  | ExtraArgType of string
+type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type
+
+(** {6 Equalities} *)
 
 val argument_type_eq : argument_type -> argument_type -> bool
+val genarg_type_eq :
+  ('a1, 'b1, 'c1) genarg_type ->
+  ('a2, 'b2, 'c2) genarg_type ->
+  ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option
+val abstract_argument_type_eq :
+  ('a, 'l) abstract_argument_type -> ('b, 'l) abstract_argument_type ->
+  ('a, 'b) CSig.eq option
 
 val pr_argument_type : argument_type -> Pp.std_ppcmds
 (** Print a human-readable representation for a given type. *)
@@ -236,43 +180,13 @@ sig
 
 end
 
-(** {5 Basic generic type constructors} *)
+(** {5 Compatibility layer}
 
-(** {6 Parameterized types} *)
+The functions below are aliases for generic_type constructors.
+
+*)
 
 val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
 val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
 val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
   ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
-
-(** {5 Magic used by the parser} *)
-
-val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option
-
-val register_name0 : ('a, 'b, 'c) genarg_type -> string -> unit
-(** Used by the extension to give a name to types. The string should be the
-    absolute path of the argument witness, e.g.
-    [register_name0 wit_toto "MyArg.wit_toto"]. *)
-
-val get_name0 : string -> string
-(** Return the absolute path of a given witness. *)
-
-(** {5 Unsafe loophole} *)
-
-module Unsafe :
-sig
-
-(** Unsafe magic functions. Not for kids. This is provided here as a loophole to
-    escape this module. Do NOT use outside of the dedicated areas. NOT. EVER. *)
-
-val inj : argument_type -> Obj.t -> 'lev generic_argument
-(** Injects an object as generic argument. !!!BEWARE!!! only do this as
-    [inj tpe x] where:
-
-    1. [tpe] is the reification of a [('a, 'b, 'c) genarg_type];
-    2. [x] has type ['a], ['b] or ['c] according to the return level ['lev]. *)
-
-val prj : 'lev generic_argument -> Obj.t
-(** Recover the contents of a generic argument. *)
-
-end
diff --git a/lib/hMap.ml b/lib/hMap.ml
index ba6aad913..778c366fd 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -286,6 +286,8 @@ struct
     let m = Int.Map.find h s in
     Map.find k m
 
+  let get k s = try find k s with Not_found -> assert false
+
   let split k s = assert false (** Cannot be implemented efficiently *)
 
   let map f s =
@@ -329,4 +331,17 @@ struct
       Int.Map.map fs s
   end
 
+  module Monad(M : CMap.MonadS) =
+  struct
+    module IntM = Int.Map.Monad(M)
+    module ExtM = Map.Monad(M)
+
+    let fold f s accu =
+      let ff _ m accu = ExtM.fold f m accu in
+      IntM.fold ff s accu
+
+    let fold_left _ _ _ = assert false
+    let fold_right _ _ _ = assert false
+  end
+
 end
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 4a72b015c..4eaacf914 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -72,7 +72,7 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) =
 
   end
 
-(* A few usefull wrappers:
+(* A few useful wrappers:
  * takes as argument the function [generate] 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. *)
@@ -96,20 +96,6 @@ let recursive_hcons h f u =
   let () = loop := hrec in
   hrec
 
-(* 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.  *)
 
@@ -194,18 +180,3 @@ module Hobj = Make(
     let eq = 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.generate Hstring.hcons) ()
-let obj = register_hcons (recursive_hcons Hobj.generate Hobj.hcons) ()
-
-(* 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/hashset.ml b/lib/hashset.ml
index 04009fdf3..af33544dc 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -162,7 +162,7 @@ module Make (E : EqType) =
         t.hashes.(index) <- newhashes;
         if sz <= t.limit && newsz > t.limit then begin
           t.oversize <- t.oversize + 1;
-          for i = 0 to over_limit do test_shrink_bucket t done;
+          for _i = 0 to over_limit do test_shrink_bucket t done;
         end;
         if t.oversize > Array.length t.table / over_limit then resize t
       end else if Weak.check bucket i then begin
diff --git a/lib/heap.ml b/lib/heap.ml
index 187189fca..97ccadeba 100644
--- a/lib/heap.ml
+++ b/lib/heap.ml
@@ -62,8 +62,6 @@ module Functional(X : Ordered) = struct
 
   let empty = Leaf
 
-  let is_empty t = t = Leaf
-
   let rec add x = function
     | Leaf ->
         Node (Leaf, x, Leaf)
diff --git a/lib/iStream.ml b/lib/iStream.ml
index c9f4d4a11..26a666e17 100644
--- a/lib/iStream.ml
+++ b/lib/iStream.ml
@@ -14,11 +14,11 @@ type 'a node = ('a,'a t) u
 
 and 'a t = 'a node Lazy.t
 
-let empty = Lazy.lazy_from_val Nil
+let empty = Lazy.from_val Nil
 
-let cons x s = Lazy.lazy_from_val (Cons (x, s))
+let cons x s = Lazy.from_val (Cons (x, s))
 
-let thunk = Lazy.lazy_from_fun
+let thunk = Lazy.from_fun
 
 let rec make_node f s = match f s with
 | Nil -> Nil
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 6805ce491..8791f0741 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,9 +1,10 @@
-Errors
+CErrors
+CWarnings
 Bigint
-Dyn
 Segmenttree
 Unicodetable
 Unicode
+Minisys
 System
 CThread
 Spawn
diff --git a/lib/loc.ml b/lib/loc.ml
index afdab928c..0f9864a9a 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -8,7 +8,6 @@
 
 (* Locations management *)
 
-
 type t = {
   fname : string; (** filename *)
   line_nb : int; (** start line number *)
@@ -19,7 +18,7 @@ type t = {
   ep : int; (** end position *)
 }
 
-let create fname line_nb bol_pos (bp, ep) = {
+let create fname line_nb bol_pos bp ep = {
   fname = fname; line_nb = line_nb; bol_pos = bol_pos;
   line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; }
 
@@ -54,8 +53,6 @@ let merge loc1 loc2 =
 
 let unloc loc = (loc.bp, loc.ep)
 
-let represent loc = (loc.fname, loc.line_nb, loc.bol_pos, loc.bp, loc.ep)
-
 let dummy_loc = ghost
 let join_loc = merge
 
diff --git a/lib/loc.mli b/lib/loc.mli
index f39cd2670..c08e097a8 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -8,7 +8,15 @@
 
 (** {5 Basic types} *)
 
-type t
+type t = {
+  fname : string; (** filename *)
+  line_nb : int; (** start line number *)
+  bol_pos : int; (** position of the beginning of start line *)
+  line_nb_last : int; (** end line number *)
+  bol_pos_last : int; (** position of the beginning of end line *)
+  bp : int; (** start position *)
+  ep : int; (** end position *)
+}
 
 type 'a located = t * 'a
 (** Embed a location in a type *)
@@ -17,9 +25,9 @@ type 'a located = t * 'a
 
 (** This is inherited from CAMPL4/5. *)
 
-val create : string -> int -> int -> (int * int) -> t
+val create : string -> int -> int -> int -> int -> t
 (** Create a location from a filename, a line number, a position of the
-    beginning of the line and a pair of start and end position *)
+    beginning of the line, a start and end position *)
 
 val unloc : t -> int * int
 (** Return the start and end position of a location *)
@@ -35,9 +43,6 @@ val is_ghost : t -> bool
 
 val merge : t -> t -> t
 
-val represent : t -> (string * int * int * int * int)
-(** Return the arguments given in [create] *)
-
 (** {5 Located exceptions} *)
 
 val add_loc : Exninfo.info -> t -> Exninfo.info
diff --git a/lib/minisys.ml b/lib/minisys.ml
new file mode 100644
index 000000000..25e4d79c4
--- /dev/null
+++ b/lib/minisys.ml
@@ -0,0 +1,74 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Minisys regroups some code that used to be in System.
+    Unlike System, this module has no dependency and could
+    be used for initial compilation target such as coqdep_boot.
+    The functions here are still available in System thanks to
+    an include. For the signature, look at the top of system.mli
+*)
+
+(** Dealing with directories *)
+
+type unix_path = string (* path in unix-style, with '/' separator *)
+
+type file_kind =
+  | FileDir of unix_path * (* basename of path: *) string
+  | FileRegular of string (* basename of file *)
+
+(* Copy of Filename.concat but assuming paths to always be POSIX *)
+
+let (//) dirname filename =
+  let l = String.length dirname in
+  if l = 0 || dirname.[l-1] = '/'
+  then dirname ^ filename
+  else dirname ^ "/" ^ filename
+
+(* Excluding directories; We avoid directories starting with . as well
+   as CVS and _darcs and any subdirs given via -exclude-dir *)
+
+let skipped_dirnames = ref ["CVS"; "_darcs"]
+
+let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames
+
+let ok_dirname f =
+  not (f = "") && f.[0] != '.' &&
+  not (List.mem f !skipped_dirnames) (*&&
+  (match Unicode.ident_refutation f with None -> true | _ -> false)*)
+
+(* Check directory can be opened *)
+
+let exists_dir dir =
+  try Sys.is_directory dir with Sys_error _ -> false
+
+let check_unix_dir warn dir =
+  if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
+    (String.length dir > 2 && dir.[1] = ':' ||
+     String.contains dir '\\' ||
+     String.contains dir ';')
+  then warn ("assuming " ^ dir ^
+             " to be a Unix path even if looking like a Win32 path.")
+
+let apply_subdir f path name =
+  (* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
+  (* as well as skipped files like CVS, ... *)
+  if ok_dirname name then
+    let path = if path = "." then name else path//name in
+    match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with
+    | Unix.S_DIR -> f (FileDir (path,name))
+    | Unix.S_REG -> f (FileRegular name)
+    | _ -> ()
+
+let readdir dir = try Sys.readdir dir with any -> [||]
+
+let process_directory f path =
+  Array.iter (apply_subdir f path) (readdir path)
+
+let process_subdirectories f path =
+  let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
+  process_directory f path
diff --git a/lib/option.ml b/lib/option.ml
index 4ea613e4f..fbb883d30 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -41,8 +41,8 @@ let hash f = function
 
 exception IsNone
 
-(** [get x] returns [y] where [x] is [Some y]. It raises IsNone
-    if [x] equals [None]. *)
+(** [get x] returns [y] where [x] is [Some y].
+    @raise [IsNone] if [x] equals [None]. *)
 let get = function
   | Some y -> y
   | _ -> raise IsNone
diff --git a/lib/option.mli b/lib/option.mli
index 409dff9d3..5e085620e 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -34,8 +34,8 @@ val compare : ('a -> 'a -> int) -> 'a option -> 'a option -> int
 (** Lift a hash to option types. *)
 val hash : ('a -> int) -> 'a option -> int
 
-(** [get x] returns [y] where [x] is [Some y]. It raises IsNone
-    if [x] equals [None]. *)
+(** [get x] returns [y] where [x] is [Some y].
+    @raise IsNone if [x] equals [None]. *)
 val get : 'a option -> 'a
 
 (** [make x] returns [Some x]. *)
@@ -54,7 +54,7 @@ val flatten : 'a option option -> 'a option
 val append : 'a option -> 'a option -> 'a option
 
 
-(** {6 "Iterators"} ***)
+(** {6 "Iterators"} *)
 
 (** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing
     otherwise. *)
@@ -63,8 +63,8 @@ val iter : ('a -> unit) -> 'a option -> unit
 exception Heterogeneous
 
 (** [iter2 f x y] executes [f z w] if [x] equals [Some z] and [y] equals
-    [Some w]. It does nothing if both [x] and [y] are [None]. And raises
-    [Heterogeneous] otherwise. *)
+    [Some w]. It does nothing if both [x] and [y] are [None].
+    @raise Heterogeneous otherwise. *)
 val iter2 : ('a -> 'b -> unit) -> 'a option -> 'b option -> unit
 
 (** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *)
@@ -78,8 +78,8 @@ val smartmap : ('a -> 'a) -> 'a option -> 'a option
 val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b
 
 (** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w].
-    It is [a] if both [x] and [y] are [None]. Otherwise it raises
-    [Heterogeneous]. *)
+    It is [a] if both [x] and [y] are [None].
+    @raise Heterogeneous otherwise. *)
 val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a
 
 (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
@@ -91,7 +91,7 @@ val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option
 (** [cata f e x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *)
 val cata : ('a -> 'b) -> 'b -> 'a option -> 'b
 
-(** {6 More Specific Operations} ***)
+(** {6 More Specific Operations} *)
 
 (** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *)
 val default : 'a -> 'a option -> 'a
diff --git a/lib/pp.ml b/lib/pp.ml
index 4f50e3e19..7f4bc149d 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -51,37 +51,19 @@ sig
   val prj : t -> 'a key -> 'a option
 end =
 struct
-  (** See module {Dyn} for more details. *)
 
-  type t = int * Obj.t
+module Dyn = Dyn.Make(struct end)
 
-  type 'a key = int
-
-  let dyntab = ref (Int.Map.empty : string Int.Map.t)
-
-  let create (s : string) =
-    let hash = Hashtbl.hash s in
-    let () = assert (not (Int.Map.mem hash !dyntab)) in
-    let () = dyntab := Int.Map.add hash s !dyntab in
-    hash
-
-  let inj x h = (h, Obj.repr x)
-
-  let prj (nh, rv) h =
-    if Int.equal h nh then Some (Obj.magic rv)
-    else None
+type t = Dyn.t
+type 'a key = 'a Dyn.tag
+let create = Dyn.create
+let inj = Dyn.Easy.inj
+let prj = Dyn.Easy.prj
 
 end
 
 open Pp_control
 
-(* This should not be used outside of this file. Use
-   Flags.print_emacs instead. This one is updated when reading
-   command line options. This was the only way to make [Pp] depend on
-   an option without creating a circularity: [Flags] -> [Util] ->
-   [Pp] -> [Flags] *)
-let print_emacs = ref false
-
 (* The different kinds of blocks are:
    \begin{description}
    \item[hbox:] Horizontal block no line breaking;
@@ -215,6 +197,25 @@ let strbrk s =
     else if p = n then [] else [str (String.sub s p (n-p))]
   in List.fold_left (++) Glue.empty (aux 0 0)
 
+let pr_loc_pos loc =
+  if Loc.is_ghost loc then (str"<unknown>")
+  else
+    let loc = Loc.unloc loc in
+    int (fst loc) ++ str"-" ++ int (snd loc)
+
+let pr_loc loc =
+  if Loc.is_ghost loc then str"<unknown>" ++ fnl ()
+  else
+    let fname = loc.Loc.fname in
+    if CString.equal fname "" then
+      Loc.(str"Toplevel input, characters " ++ int loc.bp ++
+	   str"-" ++ int loc.ep ++ str":" ++ fnl ())
+    else
+      Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
+	   str", line " ++ int loc.line_nb ++ str", characters " ++
+	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
+	   str":" ++ fnl())
+
 let ismt = is_empty
 
 (* boxing commands *)
@@ -268,7 +269,7 @@ let rec pr_com ft s =
       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());
+  com_if ft (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))
@@ -297,29 +298,29 @@ let pp_dirs ?pp_tag ft =
         begin match tok with
         | Str_def s ->
           let n = utf8_length s in
-          com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s
+          com_if ft (Lazy.from_val()); Format.pp_print_as ft n s
         | Str_len (s, n) ->
-          com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s
+          com_if ft (Lazy.from_val()); Format.pp_print_as ft n s
         end
     | Ppcmd_box(bty,ss)       -> (* Prevent evaluation of the stream! *)
-        com_if ft (Lazy.lazy_from_val());
+        com_if ft (Lazy.from_val());
         pp_open_box bty ;
         if not (Format.over_max_boxes ()) then Glue.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_open_box bty      -> com_if ft (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))
+        com_if ft (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))
+        com_if ft (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))
+        com_if ft (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 ()))
+        com_if ft (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;*)
@@ -350,181 +351,30 @@ let pp_dirs ?pp_tag ft =
       let () = Format.pp_print_flush ft () in
       Exninfo.iraise reraise
 
-
-
-(* pretty print on stdout and stderr *)
-
-(* Special chars for emacs, to detect warnings inside goal output *)
-let emacs_quote_start = String.make 1 (Char.chr 254)
-let emacs_quote_end = String.make 1 (Char.chr 255)
-
-let emacs_quote_info_start = "<infomsg>"
-let emacs_quote_info_end = "</infomsg>"
-
-let emacs_quote g =
-  if !print_emacs then hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
-  else hov 0 g
-
-let emacs_quote_info g =
-  if !print_emacs then hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
-  else hov 0 g
-
-
 (* pretty printing functions WITHOUT FLUSH *)
 let pp_with ?pp_tag ft strm =
   pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm))
 
-let ppnl_with ft strm =
-  pp_dirs ft (Glue.atom (Ppdir_ppcmds (strm ++ fnl ())))
-
 (* pretty printing functions WITH FLUSH *)
 let msg_with ft strm =
   pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush))
 
-let msgnl_with ft strm =
-  pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(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     x = pp_with   !err_ft x
-let pperrnl   x = ppnl_with !err_ft x
-let message   s = ppnl      (str s)
-let pp_flush  x = Format.pp_print_flush !std_ft x
-let pperr_flush x = Format.pp_print_flush !err_ft x
-let flush_all () =
-  flush stderr; flush stdout; pp_flush (); pperr_flush ()
-
-(* pretty printing functions WITH FLUSH *)
-let msg x = msg_with !std_ft x
-let msgnl x = msgnl_with !std_ft x
-let msgerr x = msg_with !err_ft x
-let msgerrnl x = msgnl_with !err_ft x
-
-(* Logging management *)
-
-type message_level =  Feedback.message_level =
-  | Debug of string
-  | Info
-  | Notice
-  | Warning
-  | Error
-
-type message = Feedback.message = {
-  message_level : message_level;
-  message_content : string;
-}
-
-let of_message = Feedback.of_message
-let to_message = Feedback.to_message
-let is_message = Feedback.is_message
-
-type logger = message_level -> std_ppcmds -> unit
-
-let make_body info s =
-  emacs_quote (hov 0 (info ++ spc () ++ s))
-
-let debugbody strm = emacs_quote_info (hov 0 (str "Debug:" ++ spc () ++ strm))
-let warnbody strm = make_body (str "Warning:") strm
-let errorbody strm = make_body (str "Error:") strm
-let infobody strm = emacs_quote_info strm
-
-let std_logger ~id:_ level msg = match level with
-| Debug _ -> msgnl (debugbody msg)
-| Info -> msgnl (hov 0 msg)
-| Notice -> msgnl msg
-| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) ()
-| Error -> msgnl_with !err_ft (errorbody msg)
-
-let emacs_logger ~id:_ level mesg = match level with
-| Debug _ -> msgnl (debugbody mesg)
-| Info -> msgnl (infobody mesg)
-| Notice -> msgnl mesg
-| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody mesg)) ()
-| Error -> msgnl_with !err_ft (errorbody mesg)
-
-let logger = ref std_logger
-
-let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger
-let make_pp_nonemacs() = print_emacs:=false; logger := std_logger
-
-let ft_logger old_logger ft ~id level mesg = match level with
-  | Debug _ -> msgnl_with ft (debugbody mesg)
-  | Info -> msgnl_with ft (infobody mesg)
-  | Notice -> msgnl_with ft mesg
-  | Warning -> old_logger ~id:id level mesg
-  | Error -> old_logger ~id:id level mesg
-
-let with_output_to_file fname func input =
-  let old_logger = !logger in
-  let channel = open_out (String.concat "." [fname; "out"]) in
-  logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
-  try
-    let output = func input in
-    logger := old_logger;
-    close_out channel;
-    output
-  with reraise ->
-    let reraise = Backtrace.add_backtrace reraise in
-    logger := old_logger;
-    close_out channel;
-    Exninfo.iraise reraise
-
-let feedback_id = ref (Feedback.Edit 0)
-let feedback_route = ref Feedback.default_route
-
 (* If mixing some output and a goal display, please use msg_warning,
    so that interfaces (proofgeneral for example) can easily dispatch
    them to different windows. *)
 
-let msg_info x = !logger ~id:!feedback_id Info x
-let msg_notice x = !logger ~id:!feedback_id Notice x
-let msg_warning x = !logger ~id:!feedback_id Warning x
-let msg_error x = !logger ~id:!feedback_id Error x
-let msg_debug x = !logger ~id:!feedback_id (Debug "_") x
-
-let set_logger l = logger := (fun ~id:_ lvl msg -> l lvl msg)
-
-let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg
-
-(** Feedback *)
-
-let feeder = ref ignore
-let set_id_for_feedback ?(route=Feedback.default_route) i =
-  feedback_id := i; feedback_route := route
-let feedback ?state_id ?edit_id ?route what =
-  !feeder {
-     Feedback.contents = what;
-     Feedback.route = Option.default !feedback_route route;
-     Feedback.id =
-       match state_id, edit_id with
-       | Some id, _ -> Feedback.State id
-       | None, Some eid -> Feedback.Edit eid
-       | None, None -> !feedback_id;
-  }
-let set_feeder f = feeder := f
-let get_id_for_feedback () = !feedback_id, !feedback_route
-
-(** Utility *)
-
+(** Output to a string formatter *)
 let string_of_ppcmds c =
-  msg_with Format.str_formatter c;
+  Format.fprintf Format.str_formatter "@[%a@]" msg_with c;
   Format.flush_str_formatter ()
 
-let log_via_feedback () = logger := (fun ~id lvl msg ->
-  !feeder {
-     Feedback.contents = Feedback.Message {
-       message_level = lvl;
-       message_content = string_of_ppcmds msg };
-     Feedback.route = !feedback_route;
-     Feedback.id = id })
-
 (* Copy paste from Util *)
 
 let pr_comma () = str "," ++ spc ()
 let pr_semicolon () = str ";" ++ spc ()
 let pr_bar () = str "|" ++ spc ()
 let pr_arg pr x = spc () ++ pr x
+let pr_non_empty_arg pr x = let pp = pr x in if ismt pp then mt () else spc () ++ pr x
 let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
 let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x
 
@@ -607,3 +457,4 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
 let prvect elem v = prvect_with_sep mt elem v
 
 let surround p = hov 1 (str"(" ++ p ++ str")")
+
diff --git a/lib/pp.mli b/lib/pp.mli
index 98219636b..3bd560812 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,32 +6,24 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Modify pretty printing functions behavior for emacs ouput (special
-   chars inserted at some places). This function should called once in
-   module [Options], that's all. *)
-val make_pp_emacs:unit -> unit
-val make_pp_nonemacs:unit -> unit
-
-val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
-
 (** Pretty-printers. *)
 
 type std_ppcmds
 
 (** {6 Formatting commands} *)
 
-val str  : string -> std_ppcmds
+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 ismt : std_ppcmds -> bool
-
-val comment : int -> 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 ismt  : std_ppcmds -> bool
+
+val comment  : int -> std_ppcmds
 val comments : ((int * int) * string) list ref
 
 (** {6 Manipulation commands} *)
@@ -100,87 +92,10 @@ sig
   (** Project an object from a tag. *)
 end
 
-type tag_handler = Tag.t -> Format.tag
-
 val tag : Tag.t -> std_ppcmds -> std_ppcmds
 val open_tag : Tag.t -> std_ppcmds
 val close_tag : unit -> std_ppcmds
 
-(** {6 Sending messages to the user} *)
-type message_level = Feedback.message_level =
-  | Debug of string
-  | Info
-  | Notice
-  | Warning
-  | Error
-
-type message = Feedback.message = {
-  message_level : message_level;
-  message_content : string;
-}
-
-type logger = message_level -> std_ppcmds -> unit
-
-(** {6 output functions}
-
-[msg_notice] do not put any decoration on output by default. If
-possible don't mix it with goal output (prefer msg_info or
-msg_warning) so that interfaces can dispatch outputs easily. Once all
-interfaces use the xml-like protocol this constraint can be
-relaxed. *)
-(* Should we advertise these functions more? Should they be the ONLY
-   allowed way to output something? *)
-
-val msg_info : std_ppcmds -> unit
-(** Message that displays information, usually in verbose mode, such as [Foobar
-    is defined] *)
-
-val msg_notice : std_ppcmds -> unit
-(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
-
-val msg_warning : std_ppcmds -> unit
-(** Message indicating that something went wrong, but without serious
-    consequences. *)
-
-val msg_error : std_ppcmds -> unit
-(** Message indicating that something went really wrong, though still
-    recoverable; otherwise an exception would have been raised. *)
-
-val msg_debug : std_ppcmds -> unit
-(** For debugging purposes *)
-
-val std_logger : logger
-(** Standard logging function *)
-
-val set_logger : logger -> unit
-
-val log_via_feedback : unit -> unit
-
-val of_message : message -> Xml_datatype.xml
-val to_message : Xml_datatype.xml -> message
-val is_message : Xml_datatype.xml -> bool
-
-
-(** {6 Feedback sent, even asynchronously, to the user interface} *)
-
-(* This stuff should be available to most of the system, line msg_* above.
- * But I'm unsure this is the right place, especially for the global edit_id.
- *
- * Morally the parser gets a string and an edit_id, and gives back an AST.
- * Feedbacks during the parsing phase are attached to this edit_id.
- * The interpreter assigns an exec_id to the ast, and feedbacks happening
- * during interpretation are attached to the exec_id.
- * Only one among state_id and edit_id can be provided. *)
-
-val feedback :
-  ?state_id:Feedback.state_id -> ?edit_id:Feedback.edit_id ->
-  ?route:Feedback.route_id -> Feedback.feedback_content -> unit
-
-val set_id_for_feedback :
-  ?route:Feedback.route_id -> Feedback.edit_or_state_id -> unit
-val set_feeder : (Feedback.feedback -> unit) -> unit
-val get_id_for_feedback : unit -> Feedback.edit_or_state_id * Feedback.route_id
-
 (** {6 Utilities} *)
 
 val string_of_ppcmds : std_ppcmds -> string
@@ -199,6 +114,9 @@ val pr_bar : unit -> std_ppcmds
 val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
 (** Adds a space in front of its argument. *)
 
+val pr_non_empty_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
+(** Adds a space in front of its argument if non empty. *)
+
 val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
 (** Inner object preceded with a space if [Some], nothing otherwise. *)
 
@@ -248,31 +166,15 @@ val surround : std_ppcmds -> std_ppcmds
 
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 
-(** {6 Low-level pretty-printing functions {% \emph{%}without flush{% }%}. } *)
-
-val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
-
-(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
+val pr_loc : Loc.t -> std_ppcmds
 
-(** These functions are low-level interface to printing and should not be used
-    in usual code. Consider using the [msg_*] function family instead. *)
+(** {6 Low-level pretty-printing functions with and without flush} *)
 
-val pp : std_ppcmds -> unit
-val ppnl : std_ppcmds -> unit
-val pperr : std_ppcmds -> unit
-val pperrnl : std_ppcmds -> unit
-val pperr_flush : unit -> unit
-val pp_flush : unit -> unit
-val flush_all: unit -> unit
-
-(** {6 Deprecated functions} *)
-
-(** DEPRECATED. Do not use in newly written code. *)
+(** FIXME: These ignore the logging settings and call [Format] directly *)
+type tag_handler = Tag.t -> Format.tag
 
-val msg_with : Format.formatter -> std_ppcmds -> unit
+(** [msg_with fmt pp] Print [pp] to [fmt] and flush [fmt]  *)
+val msg_with :                        Format.formatter -> std_ppcmds -> unit
 
-val msg : std_ppcmds -> unit
-val msgnl : std_ppcmds -> unit
-val msgerr : std_ppcmds -> unit
-val msgerrnl : std_ppcmds -> unit
-val message : string -> unit       (** = pPNL *)
+(** [msg_with fmt pp] Print [pp] to [fmt] and don't flush [fmt]  *)
+val pp_with  : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
index bb73fbdf5..ecfaa822c 100644
--- a/lib/ppstyle.ml
+++ b/lib/ppstyle.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+module String = CString
 
 type t = string
 (** We use the concatenated string, with dots separating each string. We
@@ -107,8 +107,11 @@ let pp_tag t = match Pp.Tag.prj t tag with
 | None -> ""
 | Some key -> key
 
+let clear_tag_fn = ref (fun () -> ())
+
 let init_color_output () =
   let push_tag, pop_tag, clear_tag = make_style_stack !tags in
+  clear_tag_fn := clear_tag;
   let tag_handler = {
     Format.mark_open_tag = push_tag;
     Format.mark_close_tag = pop_tag;
@@ -116,34 +119,24 @@ let init_color_output () =
     Format.print_close_tag = ignore;
   } in
   let open Pp_control in
-  let () = Format.pp_set_mark_tags !std_ft true in
-  let () = Format.pp_set_mark_tags !err_ft true in
-  let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in
-  let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in
+  Format.pp_set_mark_tags !std_ft true;
+  Format.pp_set_mark_tags !err_ft true;
+  Format.pp_set_formatter_tag_functions !std_ft tag_handler;
+  Format.pp_set_formatter_tag_functions !err_ft tag_handler
+
+let color_msg ?loc ?header ft strm =
   let pptag = tag in
   let open Pp in
-  let msg ?header ft strm =
-    let strm = match header with
-    | None -> hov 0 strm
+  let ploc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
+  let strm = match header with
+    | None -> hov 0 (ploc ++ strm)
     | Some (h, t) ->
       let tag = Pp.Tag.inj t pptag in
       let h = Pp.tag tag (str h ++ str ":") in
-      hov 0 (h ++ spc () ++ strm)
-    in
-    pp_with ~pp_tag ft strm;
-    Format.pp_print_newline ft ();
-    Format.pp_print_flush ft ();
-    (** In case something went wrong, we reset the stack *)
-    clear_tag ();
-  in
-  let logger level strm = match level with
-  | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm
-  | Info -> msg !std_ft strm
-  | Notice -> msg !std_ft strm
-  | Warning ->
-    let header = ("Warning", warning_tag) in
-    Flags.if_warn (fun () -> msg ~header !err_ft strm) ()
-  | Error -> msg ~header:("Error", error_tag) !err_ft strm
+      hov 0 (ploc ++ h ++ spc () ++ strm)
   in
-  let () = set_logger logger in
-  ()
+  pp_with ~pp_tag ft strm;
+  Format.pp_print_newline ft ();
+  Format.pp_print_flush ft ();
+  (** In case something went wrong, we reset the stack *)
+  !clear_tag_fn ()
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
index 97b5869f9..b07fcd5d4 100644
--- a/lib/ppstyle.mli
+++ b/lib/ppstyle.mli
@@ -11,7 +11,8 @@
 
 (** {5 Style tags} *)
 
-type t
+type t = string
+
 (** Style tags *)
 
 val make : ?style:Terminal.style -> string list -> t
@@ -46,12 +47,11 @@ val dump : unit -> (t * Terminal.style option) list
 (** {5 Setting color output} *)
 
 val init_color_output : unit -> unit
-(** Once called, all tags defined here will use their current style when
-    printed. To this end, this function redefines the loggers used when sending
-    messages to the user. The program will in particular use the formatters
-    {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages,
-    with additional syle information provided by this module. Be careful this is
-    not compatible with the Emacs mode! *)
+
+val color_msg : ?loc:Loc.t -> ?header:string * Format.tag ->
+  Format.formatter -> Pp.std_ppcmds -> unit
+(** {!color_msg ?header fmt pp} will format according to the tags
+     defined in this file *)
 
 val pp_tag : Pp.tag_handler
 (** Returns the name of a style tag that is understandable by the formatters
diff --git a/lib/profile.ml b/lib/profile.ml
index 2350cd43a..0910db3fe 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -260,7 +260,7 @@ let time_overhead_B_C () =
       let _dw = dummy_spent_alloc () in
       let _dt = get_time () in
       ()
-    with e when Errors.noncritical e -> assert false
+    with e when CErrors.noncritical e -> assert false
   done;
   let after = get_time () in
   let beforeloop =  get_time () in
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index 6cc48c874..e7646fb79 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -25,7 +25,7 @@ let new_counter ~name a ~incr ~build =
     (* - in the main process there is a race condition between slave
          managers (that are threads) and the main thread, hence the mutex *)
     if Flags.async_proofs_is_worker () then
-      Errors.anomaly(Pp.str"Slave processes must install remote counters");
+      CErrors.anomaly(Pp.str"Slave processes must install remote counters");
     Mutex.lock m; let x = f () in Mutex.unlock m;
     build x in
   let mk_thsafe_remote_getter f () =
@@ -33,7 +33,7 @@ let new_counter ~name a ~incr ~build =
   let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in
   let installer f =
     if not (Flags.async_proofs_is_worker ()) then
-      Errors.anomaly(Pp.str"Only slave processes can install a remote counter");
+      CErrors.anomaly(Pp.str"Only slave processes can install a remote counter");
     getter := mk_thsafe_remote_getter f in
   (fun () -> !getter ()), installer
 
diff --git a/lib/richpp.ml b/lib/richpp.ml
index 453df43de..a98273edb 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -163,4 +163,34 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
   in
   node xml
 
+type richpp = xml
+
+let repr xml = xml
+let richpp_of_xml xml = xml
+let richpp_of_string s = PCData s
+
+let richpp_of_pp pp =
+  let annotate t = match Pp.Tag.prj t Ppstyle.tag with
+  | None -> None
+  | Some key -> Some (Ppstyle.repr key)
+  in
+  let rec drop = function
+  | PCData s -> [PCData s]
+  | Element (_, annotation, cs) ->
+    let cs = List.concat (List.map drop cs) in
+    match annotation.annotation with
+    | None -> cs
+    | Some s -> [Element (String.concat "." s, [], cs)]
+  in
+  let xml = rich_pp annotate pp in
+  Element ("_", [], drop xml)
+
+let raw_print xml =
+  let buf = Buffer.create 1024 in
+  let rec print = function
+  | PCData s -> Buffer.add_string buf s
+  | Element (_, _, cs) -> List.iter print cs
+  in
+  let () = print xml in
+  Buffer.contents buf
 
diff --git a/lib/richpp.mli b/lib/richpp.mli
index 05c16621b..287d265a8 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -39,3 +39,26 @@ val xml_of_rich_pp :
   ('annotation -> (string * string) list) ->
   'annotation located Xml_datatype.gxml ->
   Xml_datatype.xml
+
+(** {5 Enriched text} *)
+
+type richpp
+(** Type of text with style annotations *)
+
+val richpp_of_pp : Pp.std_ppcmds -> richpp
+(** Extract style information from formatted text *)
+
+val richpp_of_xml : Xml_datatype.xml -> richpp
+(** Do not use outside of dedicated areas *)
+
+val richpp_of_string : string -> richpp
+(** Make a styled text out of a normal string *)
+
+val repr : richpp -> Xml_datatype.xml
+(** Observe the styled text as XML *)
+
+(** {5 Debug/Compat} *)
+
+(** Represent the semi-structured document as a string, dropping any additional
+    information. *)
+val raw_print : richpp -> string
diff --git a/lib/serialize.ml b/lib/serialize.ml
deleted file mode 100644
index 79a79dd4e..000000000
--- a/lib/serialize.ml
+++ /dev/null
@@ -1,116 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Xml_datatype
-
-exception Marshal_error
-
-(** Utility functions *)
-
-let rec get_attr attr = function
-  | [] -> raise Not_found
-  | (k, v) :: l when CString.equal k attr -> v
-  | _ :: l -> get_attr attr l
-
-let massoc x l =
-  try get_attr x l
-  with Not_found -> raise Marshal_error
-
-let constructor t c args = Element (t, ["val", c], args)
-let do_match t mf = function
-  | Element (s, attrs, args) when CString.equal s t ->
-      let c = massoc "val" attrs in
-      mf c args
-  | _ -> raise Marshal_error
-
-let singleton = function
-  | [x] -> x
-  | _ -> raise Marshal_error
-
-let raw_string = function
-  | [] -> ""
-  | [PCData s] -> s
-  | _ -> raise Marshal_error
-
-(** Base types *)
-
-let of_unit () = Element ("unit", [], [])
-let to_unit : xml -> unit = function
-  | Element ("unit", [], []) -> ()
-  | _ -> raise Marshal_error
-
-let of_bool (b : bool) : xml =
-  if b then constructor "bool" "true" []
-  else constructor "bool" "false" []
-let to_bool : xml -> bool = do_match "bool" (fun s _ -> match s with
-  | "true" -> true
-  | "false" -> false
-  | _ -> raise Marshal_error)
-
-let of_list (f : 'a -> xml) (l : 'a list) =
-  Element ("list", [], List.map f l)
-let to_list (f : xml -> 'a) : xml -> 'a list = function
-  | Element ("list", [], l) -> List.map f l
-  | _ -> raise Marshal_error
-
-let of_option (f : 'a -> xml) : 'a option -> xml = function
-  | None -> Element ("option", ["val", "none"], [])
-  | Some x -> Element ("option", ["val", "some"], [f x])
-let to_option (f : xml -> 'a) : xml -> 'a option = function
-  | Element ("option", ["val", "none"], []) -> None
-  | Element ("option", ["val", "some"], [x]) -> Some (f x)
-  | _ -> raise Marshal_error
-
-let of_string (s : string) : xml = Element ("string", [], [PCData s])
-let to_string : xml -> string = function
-  | Element ("string", [], l) -> raw_string l
-  | _ -> raise Marshal_error
-
-let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)])
-let to_int : xml -> int = function
-  | Element ("int", [], [PCData s]) ->
-    (try int_of_string s with Failure _ -> raise Marshal_error)
-  | _ -> raise Marshal_error
-
-let of_pair (f : 'a -> xml) (g : 'b -> xml) (x : 'a * 'b) : xml =
-  Element ("pair", [], [f (fst x); g (snd x)])
-let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function
-  | Element ("pair", [], [x; y]) -> (f x, g y)
-  | _ -> raise Marshal_error
-
-let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = function
-  | CSig.Inl x -> Element ("union", ["val","in_l"], [f x])
-  | CSig.Inr x -> Element ("union", ["val","in_r"], [g x])
-let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) CSig.union = function
-  | Element ("union", ["val","in_l"], [x]) -> CSig.Inl (f x)
-  | Element ("union", ["val","in_r"], [x]) -> CSig.Inr (g x)
-  | _ -> raise Marshal_error
-
-(** More elaborate types *)
-
-let of_edit_id i = Element ("edit_id",["val",string_of_int i],[])
-let to_edit_id = function
-  | Element ("edit_id",["val",i],[]) ->
-      let id = int_of_string i in
-      assert (id <= 0 );
-      id
-  | _ -> raise Marshal_error
-
-let of_loc loc =
-  let start, stop = Loc.unloc loc in
-  Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[])
-let to_loc xml =
-  match xml with
-  | Element ("loc", l,[]) ->
-      (try
-        let start = massoc "start" l in
-        let stop = massoc "stop" l in
-        Loc.make_loc (int_of_string start, int_of_string stop)
-      with Not_found | Invalid_argument _ -> raise Marshal_error)
-  | _ -> raise Marshal_error
-
diff --git a/lib/serialize.mli b/lib/serialize.mli
deleted file mode 100644
index 2a8e53163..000000000
--- a/lib/serialize.mli
+++ /dev/null
@@ -1,37 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Xml_datatype
-
-exception Marshal_error
-
-val massoc: string -> (string * string) list -> string
-val constructor: string -> string -> xml list -> xml
-val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b
-val singleton: 'a list -> 'a
-val raw_string: xml list -> string
-val of_unit: unit -> xml
-val to_unit: xml -> unit
-val of_bool: bool -> xml
-val to_bool: xml -> bool
-val of_list: ('a -> xml) -> 'a list -> xml
-val to_list: (xml -> 'a) -> xml -> 'a list
-val of_option: ('a -> xml) -> 'a option -> xml
-val to_option: (xml -> 'a) -> xml -> 'a option
-val of_string: string -> xml
-val to_string: xml -> string
-val of_int: int -> xml
-val to_int: xml -> int
-val of_pair: ('a -> xml) -> ('b -> xml) -> 'a * 'b -> xml
-val to_pair: (xml -> 'a) -> (xml -> 'b) -> xml -> 'a * 'b
-val of_union: ('a -> xml) -> ('b -> xml) -> ('a, 'b) CSig.union -> xml
-val to_union: (xml -> 'a) -> (xml -> 'b) -> xml -> ('a, 'b) CSig.union
-val of_edit_id: int -> xml
-val to_edit_id: xml -> int
-val of_loc : Loc.t -> xml
-val to_loc : xml -> Loc.t
diff --git a/lib/spawn.ml b/lib/spawn.ml
index fda4b4239..479176973 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -43,7 +43,7 @@ module type MainLoopModel = sig
 end
 
 (* Common code *)
-let assert_ b s = if not b then Errors.anomaly (Pp.str s)
+let assert_ b s = if not b then CErrors.anomaly (Pp.str s)
 
 (* According to http://caml.inria.fr/mantis/view.php?id=5325
  * you can't use the same socket for both writing and reading (may change
@@ -78,20 +78,6 @@ let accept (sr,sw) =
   set_binary_mode_out cout true;
   (csr, csw), cin, cout
 
-let handshake cin cout =
-  try
-    output_value cout (Hello (proto_version,Unix.getpid ())); flush cout;
-    match input_value cin with
-    | Hello(v, pid) when v = proto_version ->
-        prerr_endline (Printf.sprintf "Handshake with %d OK" pid);
-        pid
-    | _ -> raise (Failure "handshake protocol")
-  with
-  | Failure s | Invalid_argument s | Sys_error s ->
-      pr_err ("Handshake failed: "  ^ s); raise (Failure "handshake")
-  | End_of_file ->
-      pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
-
 let spawn_sock env prog args =
   let main_sock, main_sock_name = mk_socket_channel () in
   let extra = [| prog; "-main-channel"; main_sock_name |] in
@@ -206,7 +192,7 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
         let live = callback cl ~read_all:(fun () -> ML.read_all gchan) in
         if not live then kill p;
         live
-      with e when Errors.noncritical e ->
+      with e when CErrors.noncritical e ->
         pr_err ("Async reader raised: " ^ (Printexc.to_string e));
         kill p;
         false) gchan
diff --git a/lib/stateid.ml b/lib/stateid.ml
index 59cf206e2..500581a39 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Xml_datatype
-
 type t = int
 let initial = 1
 let dummy = 0
@@ -15,20 +13,14 @@ let fresh, in_range =
   let cur = ref initial in
   (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur)
 let to_string = string_of_int
-let of_int id = assert(in_range id); id
+let of_int id =
+  (* Coqide too to parse ids too, but cannot check if they are valid.
+   * Hence we check for validity only if we are an ide slave. *)
+  if !Flags.ide_slave then assert (in_range id);
+  id
 let to_int id = id
 let newer_than id1 id2 = id1 > id2
 
-let of_xml = function
-  | Element ("state_id",["val",i],[]) ->
-      let id = int_of_string i in
-      (* Coqide too to parse ids too, but cannot check if they are valid.
-       * Hence we check for validity only if we are an ide slave. *)
-      if !Flags.ide_slave then assert(in_range id);
-      id
-  | _ -> raise (Invalid_argument "to_state_id")
-let to_xml i = Element ("state_id",["val",string_of_int i],[])
-
 let state_id_info : (t * t) Exninfo.t = Exninfo.make ()
 let add exn ?(valid = initial) id =
   Exninfo.add exn state_id_info (valid, id)
@@ -37,7 +29,13 @@ let get exn = Exninfo.get exn state_id_info
 let equal = Int.equal
 let compare = Int.compare
 
-module Set = Set.Make(struct type t = int let compare = compare end)
+module Self = struct
+ type t = int
+ let compare = compare
+ let equal = equal
+end
+
+module Set = Set.Make(Self)
 
 type ('a,'b) request = {
   exn_info : t * t;
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 2c12c30c3..cd8fddf0c 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -6,26 +6,23 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Xml_datatype
-
 type t
 
 val equal : t -> t -> bool
 val compare : t -> t -> int
 
-module Set : Set.S with type elt = t
+module Self : Map.OrderedType with type t = t
+module Set : Set.S with type elt = t and type t = Set.Make(Self).t
 
 val initial : t
 val dummy : t
 val fresh : unit -> t
 val to_string : t -> string
+
 val of_int : int -> t
 val to_int : t -> int
-val newer_than : t -> t -> bool
 
-(* XML marshalling *)
-val to_xml : t -> xml
-val of_xml : xml -> t
+val newer_than : t -> t -> bool
 
 (* Attaches to an exception the concerned state id, plus an optional
  * state id that is a valid state id before the error.
diff --git a/lib/system.ml b/lib/system.ml
index b4b3882d3..af9aa5c07 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -9,40 +9,33 @@
 (* $Id$ *)
 
 open Pp
-open Errors
 open Util
 
-(* All subdirectories, recursively *)
+include Minisys
 
-let exists_dir dir =
-  try Sys.is_directory dir with Sys_error _ -> false
+(** Returns the list of all recursive subdirectories of [root] in
+    depth-first search, with sons ordered as on the file system;
+    warns if [root] does not exist *)
 
-let skipped_dirnames = ref ["CVS"; "_darcs"]
-
-let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
-
-let ok_dirname f =
-  not (String.is_empty f) && f.[0] != '.' &&
-  not (String.List.mem f !skipped_dirnames) &&
-  (match Unicode.ident_refutation f with None -> true | _ -> false)
-
-let readdir dir = try Sys.readdir dir with any -> [||]
+let warn_cannot_open_dir =
+  CWarnings.create ~name:"cannot-open-dir" ~category:"filesystem"
+  (fun dir -> str ("Cannot open directory " ^ dir))
 
 let all_subdirs ~unix_path:root =
   let l = ref [] in
   let add f rel = l := (f, rel) :: !l in
-  let rec traverse dir rel =
-    Array.iter (fun f ->
-      if ok_dirname f then
-	let file = Filename.concat dir f in
-        if exists_dir file then begin
-          let newrel = rel @ [f] in
-	  add file newrel;
-	  traverse file newrel
-        end)
-      (readdir dir)
+  let rec traverse path rel =
+    let f = function
+      | FileDir (path,f) ->
+	  let newrel = rel @ [f] in
+	  add path newrel;
+	  traverse path newrel
+      | _ -> ()
+    in process_directory f path
   in
-  if exists_dir root then traverse root [];
+  check_unix_dir (fun s -> Feedback.msg_warning (str s)) root;
+  if exists_dir root then traverse root []
+  else warn_cannot_open_dir root;
   List.rev !l
 
 (* Caching directory contents for efficient syntactic equality of file
@@ -63,20 +56,22 @@ let make_dir_table dir =
   Array.fold_left filter_dotfiles StrSet.empty (readdir dir)
 
 let exists_in_dir_respecting_case dir bf =
-  let contents, cached =
-    try StrMap.find dir !dirmap, true with Not_found ->
+  let cache_dir dir =
     let contents = make_dir_table dir in
     dirmap := StrMap.add dir contents !dirmap;
-    contents, false in
+    contents in
+  let contents, fresh =
+    try
+      (* in batch mode, assume the directory content is still fresh *)
+      StrMap.find dir !dirmap, !Flags.batch_mode
+    with Not_found ->
+      (* in batch mode, we are not yet sure the directory exists *)
+      if !Flags.batch_mode && not (exists_dir dir) then StrSet.empty, true
+      else cache_dir dir, true in
   StrSet.mem bf contents ||
-    if cached then begin
+    not fresh &&
       (* rescan, there is a new file we don't know about *)
-      let contents = make_dir_table dir in
-      dirmap := StrMap.add dir contents !dirmap;
-      StrSet.mem bf contents
-    end
-    else
-      false
+      StrSet.mem bf (cache_dir dir)
 
 let file_exists_respecting_case path f =
   (* This function ensures that a file with expected lowercase/uppercase
@@ -86,26 +81,29 @@ let file_exists_respecting_case path f =
     let df = Filename.dirname f in
     (String.equal df "." || aux df)
     && exists_in_dir_respecting_case (Filename.concat path df) bf
-  in Sys.file_exists (Filename.concat path f) && aux f
+  in (!Flags.batch_mode || Sys.file_exists (Filename.concat path f)) && aux f
 
 let rec search paths test =
   match paths with
   | [] -> []
   | lpe :: rem -> test lpe @ search rem test
 
+let warn_ambiguous_file_name =
+  CWarnings.create ~name:"ambiguous-file-name" ~category:"filesystem"
+    (fun (filename,l,f) -> str filename ++ str " has been found in" ++ spc () ++
+                hov 0 (str "[ " ++
+                         hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
+                                               (fun (lpe,_) -> str lpe) l)
+                       ++ str " ];") ++ fnl () ++
+                str "loading " ++ str f)
+
+
 let where_in_path ?(warn=true) path filename =
   let check_and_warn l = match l with
   | [] -> raise Not_found
   | (lpe, f) :: l' ->
     let () = match l' with
-    | _ :: _ when warn ->
-      msg_warning
-        (str filename ++ str " has been found in" ++ spc () ++
-          hov 0 (str "[ " ++
-            hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
-              (fun (lpe,_) -> str lpe) l)
-            ++ str " ];") ++ fnl () ++
-          str "loading " ++ str f)
+    | _ :: _ when warn -> warn_ambiguous_file_name (filename,l,f)
     | _ -> ()
     in
     (lpe, f)
@@ -134,7 +132,7 @@ let find_file_in_path ?(warn=true) paths filename =
       let root = Filename.dirname filename in
       root, filename
     else
-      errorlabstrm "System.find_file_in_path"
+      CErrors.errorlabstrm "System.find_file_in_path"
 	(hov 0 (str "Can't find file" ++ spc () ++ str filename))
   else
     (* the name is considered to be the transcription as a relative
@@ -142,7 +140,7 @@ let find_file_in_path ?(warn=true) paths filename =
        to be locate respecting case *)
     try where_in_path ~warn paths filename
     with Not_found ->
-      errorlabstrm "System.find_file_in_path"
+      CErrors.errorlabstrm "System.find_file_in_path"
 	(hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
 		str "on loadpath"))
 
@@ -150,27 +148,34 @@ let is_in_path lpath filename =
   try ignore (where_in_path ~warn:false lpath filename); true
   with Not_found -> false
 
+let warn_path_not_found =
+  CWarnings.create ~name:"path-not-found" ~category:"filesystem"
+  (fun () -> str "system variable PATH not found")
+
 let is_in_system_path filename =
   try
     let lpath = CUnix.path_to_list (Sys.getenv "PATH") in
     is_in_path lpath filename
   with Not_found ->
-    msg_warning (str "system variable PATH not found");
+    warn_path_not_found ();
     false
 
 let open_trapping_failure name =
   try open_out_bin name
-  with e when Errors.noncritical e ->
-    errorlabstrm "System.open" (str "Can't open " ++ str name)
+  with e when CErrors.noncritical e ->
+    CErrors.errorlabstrm "System.open" (str "Can't open " ++ str name)
+
+let warn_cannot_remove_file =
+  CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem"
+  (fun filename -> str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
 let try_remove filename =
   try Sys.remove filename
-  with e when Errors.noncritical e ->
-    msg_warning
-      (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
+  with e when CErrors.noncritical e ->
+    warn_cannot_remove_file filename
 
 let error_corrupted file s =
-  errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
+  CErrors.errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
 
 let input_binary_int f ch =
   try input_binary_int ch
@@ -243,11 +248,11 @@ let extern_state magic filename val_0 =
       marshal_out channel val_0;
       close_out channel
     with reraise ->
-      let reraise = Errors.push reraise in
+      let reraise = CErrors.push reraise in
       let () = try_remove filename in
       iraise reraise
   with Sys_error s ->
-    errorlabstrm "System.extern_state" (str "System error: " ++ str s)
+    CErrors.errorlabstrm "System.extern_state" (str "System error: " ++ str s)
 
 let intern_state magic filename =
   try
@@ -256,12 +261,12 @@ let intern_state magic filename =
     close_in channel;
     v
   with Sys_error s ->
-    errorlabstrm "System.intern_state" (str "System error: " ++ str s)
+    CErrors.errorlabstrm "System.intern_state" (str "System error: " ++ str s)
 
 let with_magic_number_check f a =
   try f a
   with Bad_magic_number {filename=fname;actual=actual;expected=expected} ->
-    errorlabstrm "with_magic_number_check"
+    CErrors.errorlabstrm "with_magic_number_check"
     (str"File " ++ str fname ++ strbrk" has bad magic number " ++
     int actual ++ str" (expected " ++ int expected ++ str")." ++
     spc () ++
@@ -295,13 +300,13 @@ let with_time time f x =
     let y = f x in
     let tend = get_time() in
     let msg2 = if time then "" else " (successful)" in
-    msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     y
   with e ->
     let tend = get_time() in
     let msg = if time then "" else "Finished failing transaction in " in
     let msg2 = if time then "" else " (failure)" in
-    msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
 
 let process_id () =
diff --git a/lib/system.mli b/lib/system.mli
index fa675a4f0..4dbb3695d 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -8,14 +8,46 @@
 
 (** {5 Coqtop specific system utilities} *)
 
+(** {6 Directories} *)
+
+type unix_path = string (* path in unix-style, with '/' separator *)
+
+type file_kind =
+  | FileDir of unix_path * (* basename of path: *) string
+  | FileRegular of string (* basename of file *)
+
+val (//) : unix_path -> string -> unix_path
+
+val exists_dir : unix_path -> bool
+
+(** [check_unix_dir warn path] calls [warn] with an appropriate
+     message if [path] looks does not look like a Unix path on Windows *)
+
+val check_unix_dir : (string -> unit) -> unix_path -> unit
+
+(** [exclude_search_in_dirname path] excludes [path] when processing
+    directories *)
+
+val exclude_directory : unix_path -> unit
+
+(** [process_directory f path] applies [f] on contents of directory
+    [path]; fails with Unix_error if the latter does not exists; skips
+    all files or dirs starting with "." *)
+
+val process_directory : (file_kind -> unit) -> unix_path -> unit
+
+(** [process_subdirectories f path] applies [f path/file file] on each
+    [file] of the directory [path]; fails with Unix_error if the
+    latter does not exists; kips all files or dirs starting with "." *)
+
+val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit
+
 (** {6 Files and load paths} *)
 
 (** Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
     [directory]), the root path and the path relative to the root. *)
 
-val exclude_search_in_dirname : string -> unit
-
 val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list
 val is_in_path : CUnix.load_path -> string -> bool
 val is_in_system_path : string -> bool
@@ -24,8 +56,6 @@ val where_in_path :
 val where_in_path_rex :
   CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list
 
-val exists_dir : string -> bool
-
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
 
diff --git a/lib/unicode.ml b/lib/unicode.ml
index 0dc4238ee..dc852d981 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -18,7 +18,7 @@ exception Unsupported
    to simplify the masking process. (This choice seems to be a good
    trade-off between speed and space after some benchmarks.) *)
 
-(* A 256ko table, initially filled with zeros. *)
+(* A 256 KiB table, initially filled with zeros. *)
 let table = Array.make (1 lsl 17) 0
 
 (* Associate a 2-bit pattern to each status at position [i].
@@ -147,6 +147,11 @@ let utf8_of_unicode n =
       s
     end
 
+(* If [s] is some UTF-8 encoded string
+   and [i] is a position of some UTF-8 character within [s]
+   then [next_utf8 s i] returns [(j,n)] where:
+   - [j] indicates the position of the next UTF-8 character
+   - [n] represents the UTF-8 character at index [i] *)
 let next_utf8 s i =
   let err () = invalid_arg "utf8" in
   let l = String.length s - i in
@@ -256,3 +261,73 @@ let ascii_of_ident s =
         (Buffer.add_char out s.[!i]; incr i)
     done;
     Buffer.contents out
+
+(* 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 *)
+
+(** FIXME: duplicate code with Pp *)
+
+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
+
+(* Variant of String.sub for UTF8 character positions *)
+let utf8_sub s start_u len_u =
+  let len_b = String.length s
+  and end_u = start_u + len_u
+  and cnt = ref 0
+  and nc = ref 0
+  and p = ref 0 in
+  let start_b = ref len_b in
+  while !p < len_b && !cnt < end_u do
+    if !cnt <= start_u then start_b := !p ;
+    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_b && !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 ;
+  let end_b = !p in
+  String.sub s !start_b (end_b - !start_b)
diff --git a/lib/unicode.mli b/lib/unicode.mli
index 00211164f..1f8bd44ee 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -10,17 +10,21 @@
 
 type status = Letter | IdentPart | Symbol
 
+(** This exception is raised when UTF-8 the input string contains unsupported UTF-8 characters. *)
 exception Unsupported
 
-(** Classify a unicode char into 3 classes, or raise [Unsupported] *)
+(** Classify a unicode char into 3 classes.
+    @raise Unsupported if the input string contains unsupported UTF-8 characters. *)
 val classify : int -> status
 
-(** Check whether a given string be used as a legal identifier.
-    - [None] means yes
-    - [Some (b,s)] means no, with explanation [s] and severity [b] *)
+(** Return [None] if a given string can be used as a (Coq) identifier.
+    Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity.
+    @raise Unsupported if the input string contains unsupported UTF-8 characters. *)
 val ident_refutation : string -> (bool * string) option
 
-(** First char of a string, converted to lowercase *)
+(** First char of a string, converted to lowercase
+    @raise Unsupported if the input string contains unsupported UTF-8 characters.
+    @raise Assert_failure if the input string is empty. *)
 val lowercase_first_char : string -> string
 
 (** Return [true] if all UTF-8 characters in the input string are just plain
@@ -36,3 +40,9 @@ val ascii_of_ident : string -> string
 
 (** Validate an UTF-8 string *)
 val is_utf8 : string -> bool
+
+(** Return the length of a valid UTF-8 string. *)
+val utf8_length : string -> int
+
+(** Variant of {!String.sub} for UTF-8 strings. *)
+val utf8_sub : string -> int -> int -> string
diff --git a/lib/util.ml b/lib/util.ml
index a20dba0fc..009dfbe1c 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -87,7 +87,13 @@ let matrix_transpose mat =
 
 let identity x = x
 
-let compose f g x = f (g x)
+(** Function composition: the mathematical [∘] operator.
+
+    So [g % f] is a synonym for [fun x -> g (f x)].
+
+    Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))].
+ *)
+let (%) f g x = f (g x)
 
 let const x _ = x
 
@@ -124,10 +130,26 @@ let delayed_force f = f ()
 
 type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
+type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq
+
+module Union =
+struct
+  let map f g = function
+    | Inl a -> Inl (f a)
+    | Inr b -> Inr (g b)
+
+  (** Lifting equality onto union types. *)
+  let equal f g x y = match x, y with
+    | Inl x, Inl y -> f x y
+    | Inr x, Inr y -> g x y
+    | _, _ -> false
+
+  let fold_left f g a = function
+    | Inl y -> f a y
+    | Inr y -> g a y
+end
 
-let map_union f g = function
-  | Inl a -> Inl (f a)
-  | Inr b -> Inr (g b)
+let map_union = Union.map
 
 type iexn = Exninfo.iexn
 
diff --git a/lib/util.mli b/lib/util.mli
index 4156af672..6bed7e355 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -83,7 +83,15 @@ val matrix_transpose : 'a list list -> 'a list list
 (** {6 Functions. } *)
 
 val identity : 'a -> 'a
-val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+
+(** Function composition: the mathematical [∘] operator.
+
+    So [g % f] is a synonym for [fun x -> g (f x)].
+
+    Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))].
+*)
+val (%) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+
 val const : 'a -> 'b -> 'a
 val iterate : ('a -> 'a) -> int -> 'a -> 'a
 val repeat : int -> ('a -> unit) -> 'a -> unit
@@ -106,10 +114,20 @@ val iraise : iexn -> 'a
 type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
 (** Union type *)
 
+module Union :
+sig
+  val map : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
+  val equal : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a, 'b) union -> ('a, 'b) union -> bool
+  val fold_left : ('c -> 'a -> 'c) -> ('c -> 'b -> 'c) -> 'c -> ('a, 'b) union -> 'c
+end
+
 val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
+(** Alias for [Union.map] *)
 
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 (** Used for browsable-until structures. *)
 
+type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq
+
 val open_utf8_file_in : string -> in_channel
 (** Open an utf-8 encoded file and skip the byte-order mark if any. *)
diff --git a/lib/xml_lexer.mli b/lib/xml_lexer.mli
deleted file mode 100644
index e61cb055f..000000000
--- a/lib/xml_lexer.mli
+++ /dev/null
@@ -1,44 +0,0 @@
-(*
- * Xml Light, an small Xml parser/printer with DTD support.
- * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License as published by the Free Software Foundation; either
- * version 2.1 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this library; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
- *)
-
-type error =
-	| EUnterminatedComment
-	| EUnterminatedString
-	| EIdentExpected
-	| ECloseExpected
-	| ENodeExpected
-	| EAttributeNameExpected
-	| EAttributeValueExpected
-	| EUnterminatedEntity
-
-exception Error of error
-
-type token =
-	| Tag of string * (string * string) list * bool
-	| PCData of string
-	| Endtag of string
-	| Eof
-
-type pos = int * int * int * int
-
-val init : Lexing.lexbuf -> unit 
-val close : unit -> unit
-val token : Lexing.lexbuf -> token
-val pos : Lexing.lexbuf -> pos
-val restore : pos -> unit
diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll
deleted file mode 100644
index 290f2c89a..000000000
--- a/lib/xml_lexer.mll
+++ /dev/null
@@ -1,317 +0,0 @@
-{(*
- * Xml Light, an small Xml parser/printer with DTD support.
- * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License as published by the Free Software Foundation; either
- * version 2.1 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this library; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
- *)
-
-open Lexing
-
-type error =
-        | EUnterminatedComment
-        | EUnterminatedString
-        | EIdentExpected
-        | ECloseExpected
-        | ENodeExpected
-        | EAttributeNameExpected
-        | EAttributeValueExpected
-        | EUnterminatedEntity
-
-exception Error of error
-
-type pos = int * int * int * int
-
-type token =
-        | Tag of string * (string * string) list * bool
-        | PCData of string
-        | Endtag of string
-        | Eof
-
-let last_pos = ref 0
-and current_line = ref 0
-and current_line_start = ref 0
-
-let tmp = Buffer.create 200
-
-let idents = Hashtbl.create 0
-
-let _ = begin
-        Hashtbl.add idents "nbsp;" " ";
-        Hashtbl.add idents "gt;" ">";
-        Hashtbl.add idents "lt;" "<";
-        Hashtbl.add idents "amp;" "&";
-        Hashtbl.add idents "apos;" "'";
-        Hashtbl.add idents "quot;" "\"";
-end
-
-let init lexbuf =
-        current_line := 1;
-        current_line_start := lexeme_start lexbuf;
-        last_pos := !current_line_start
-
-let close lexbuf =
-        Buffer.reset tmp
-
-let pos lexbuf =
-        !current_line , !current_line_start ,
-        !last_pos ,
-        lexeme_start lexbuf
-
-let restore (cl,cls,lp,_) =
-        current_line := cl;
-        current_line_start := cls;
-        last_pos := lp
-
-let newline lexbuf =
-        incr current_line;
-        last_pos := lexeme_end lexbuf;
-        current_line_start := !last_pos
-
-let error lexbuf e =
-        last_pos := lexeme_start lexbuf;
-        raise (Error e)
-
-}
-
-let newline = ['\n']
-let break = ['\r']
-let space = [' ' '\t']
-let identchar =  ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-' '.']
-let ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar*
-let entitychar = ['A'-'Z' 'a'-'z']
-let pcchar = [^ '\r' '\n' '<' '>' '&']
-
-rule token = parse
-        | newline | (newline break) | break
-                {
-                        newline lexbuf;
-                        PCData "\n"
-                }
-        | "<!--"
-                {
-                        last_pos := lexeme_start lexbuf;
-                        comment lexbuf;
-                        token lexbuf
-                }
-        | "<?"
-                {
-                        last_pos := lexeme_start lexbuf;
-                        header lexbuf;
-                        token lexbuf;
-                }
-        | '<' space* '/' space*
-                {
-                        last_pos := lexeme_start lexbuf;
-                        let tag = ident_name lexbuf in
-                        ignore_spaces lexbuf;
-                        close_tag lexbuf;
-                        Endtag tag
-                }
-        | '<' space*
-                {
-                        last_pos := lexeme_start lexbuf;
-                        let tag = ident_name lexbuf in
-                        ignore_spaces lexbuf;
-                        let attribs, closed = attributes lexbuf in
-                        Tag(tag, attribs, closed)
-                }
-        | "&#"
-                {
-                        last_pos := lexeme_start lexbuf;
-                        Buffer.reset tmp;
-                        Buffer.add_string tmp (lexeme lexbuf);
-                        PCData (pcdata lexbuf)
-                }
-        | '&'
-                {
-                        last_pos := lexeme_start lexbuf;
-                        Buffer.reset tmp;
-                        Buffer.add_string tmp (entity lexbuf);
-                        PCData (pcdata lexbuf)
-                }
-        | pcchar+
-                {
-                        last_pos := lexeme_start lexbuf;
-                        Buffer.reset tmp;
-                        Buffer.add_string tmp (lexeme lexbuf);
-                        PCData (pcdata lexbuf)
-                }
-        | eof { Eof }
-        | _
-                { error lexbuf ENodeExpected }
-
-and ignore_spaces = parse
-        | newline | (newline break) | break
-                {
-                        newline lexbuf;
-                        ignore_spaces lexbuf
-                }
-        | space +
-                { ignore_spaces lexbuf }
-        | ""
-                { () }
-
-and comment = parse
-        | newline | (newline break) | break
-                {
-                        newline lexbuf;
-                        comment lexbuf
-                }
-        | "-->"
-                { () }
-        | eof
-                { raise (Error EUnterminatedComment) }
-        | _
-                { comment lexbuf }
-
-and header = parse
-        | newline | (newline break) | break
-                {
-                        newline lexbuf;
-                        header lexbuf
-                }
-        | "?>"
-                { () }
-        | eof
-                { error lexbuf ECloseExpected }
-        | _
-                { header lexbuf }
-
-and pcdata = parse
-        | newline | (newline break) | break
-                {
-                        Buffer.add_char tmp '\n';
-                        newline lexbuf;
-                        pcdata lexbuf
-                }
-        | pcchar+
-                {
-                        Buffer.add_string tmp (lexeme lexbuf);
-                        pcdata lexbuf
-                }
-        | "&#"
-                {
-                        Buffer.add_string tmp (lexeme lexbuf);
-                        pcdata lexbuf;
-                }
-        | '&'
-                {
-                        Buffer.add_string tmp (entity lexbuf);
-                        pcdata lexbuf
-                }
-        | ""
-                { Buffer.contents tmp }
-
-and entity = parse
-        | entitychar+ ';'
-                {
-                        let ident = lexeme lexbuf in
-                        try
-                                Hashtbl.find idents (String.lowercase ident)
-                        with
-                                Not_found -> "&" ^ ident
-                }
-        | _ | eof
-                { raise (Error EUnterminatedEntity) }
-
-and ident_name = parse
-        | ident
-                { lexeme lexbuf }
-        | _ | eof
-                { error lexbuf EIdentExpected }
-
-and close_tag = parse
-        | '>'
-                { () }
-        | _ | eof
-                { error lexbuf ECloseExpected }
-
-and attributes = parse
-        | '>'
-                { [], false }
-        | "/>"
-                { [], true }
-        | "" (* do not read a char ! *)
-                {
-                        let key = attribute lexbuf in
-                        let data = attribute_data lexbuf in
-                        ignore_spaces lexbuf;
-                        let others, closed = attributes lexbuf in
-                        (key, data) :: others, closed
-                }
-
-and attribute = parse
-        | ident
-                { lexeme lexbuf }
-        | _ | eof
-                { error lexbuf EAttributeNameExpected }
-
-and attribute_data = parse
-        | space* '=' space* '"'
-                {
-                        Buffer.reset tmp;
-                        last_pos := lexeme_end lexbuf;
-                        dq_string lexbuf
-                }
-        | space* '=' space* '\''
-                {
-                        Buffer.reset tmp;
-                        last_pos := lexeme_end lexbuf;
-                        q_string lexbuf
-                }
-        | _ | eof
-                { error lexbuf EAttributeValueExpected }
-
-and dq_string = parse
-        | '"'
-                { Buffer.contents tmp }
-        | '\\' [ '"' '\\' ]
-                {
-                        Buffer.add_char tmp (lexeme_char lexbuf 1);
-                        dq_string lexbuf
-                }
-        | '&'
-                {
-                        Buffer.add_string tmp (entity lexbuf);
-                        dq_string lexbuf
-                }
-        | eof
-                { raise (Error EUnterminatedString) }
-        | _
-                {
-                        Buffer.add_char tmp (lexeme_char lexbuf 0);
-                        dq_string lexbuf
-                }
-
-and q_string = parse
-        | '\''
-                { Buffer.contents tmp }
-        | '\\' [ '\'' '\\' ]
-                {
-                        Buffer.add_char tmp (lexeme_char lexbuf 1);
-                        q_string lexbuf
-                }
-        | '&'
-                {
-                        Buffer.add_string tmp (entity lexbuf);
-                        q_string lexbuf
-                }
-        | eof
-                { raise (Error EUnterminatedString) }
-        | _
-                {
-                        Buffer.add_char tmp (lexeme_char lexbuf 0);
-                        q_string lexbuf
-                }
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
deleted file mode 100644
index 8db3f9e8b..000000000
--- a/lib/xml_parser.ml
+++ /dev/null
@@ -1,232 +0,0 @@
-(*
- * Xml Light, an small Xml parser/printer with DTD support.
- * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
- * Copyright (C) 2003 Jacques Garrigue
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License as published by the Free Software Foundation; either
- * version 2.1 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this library; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
- *)
-
-open Printf
-open Xml_datatype
-
-type xml = Xml_datatype.xml
-
-type error_pos = {
-  eline : int;
-  eline_start : int;
-  emin : int;
-  emax : int;
-}
-
-type error_msg =
-  | UnterminatedComment
-  | UnterminatedString
-  | UnterminatedEntity
-  | IdentExpected
-  | CloseExpected
-  | NodeExpected
-  | AttributeNameExpected
-  | AttributeValueExpected
-  | EndOfTagExpected of string
-  | EOFExpected
-  | Empty
-
-type error = error_msg * error_pos
-
-exception Error of error
-
-exception File_not_found of string
-
-type t = {
-  mutable check_eof : bool;
-  mutable concat_pcdata : bool;
-  source : Lexing.lexbuf;
-  stack : Xml_lexer.token Stack.t;
-}
-
-type source =
-  | SChannel of in_channel
-  | SString of string
-  | SLexbuf of Lexing.lexbuf
-
-exception Internal_error of error_msg
-exception NoMoreData
-
-let xml_error = ref (fun _ -> assert false)
-let file_not_found = ref (fun _ -> assert false)
-
-let is_blank s =
-  let len = String.length s in
-  let break = ref true in
-  let i = ref 0 in
-  while !break && !i < len do
-    let c = s.[!i] in
-    (* no '\r' because we replaced them in the lexer *)
-    if c = ' ' || c = '\n' || c = '\t' then incr i
-    else break := false
-  done;
-  !i = len
-
-let _raises e f =
-  xml_error := e;
-  file_not_found := f
-
-let make source =
-  let source = match source with
-    | SChannel chan -> Lexing.from_channel chan
-    | SString s -> Lexing.from_string s
-    | SLexbuf lexbuf -> lexbuf
-  in
-  let () = Xml_lexer.init source in
-  {
-    check_eof = false;
-    concat_pcdata = true;
-    source = source;
-    stack = Stack.create ();
-  }
-
-let check_eof p v = p.check_eof <- v
-
-let pop s =
-  try
-    Stack.pop s.stack
-  with
-      Stack.Empty ->
-        Xml_lexer.token s.source
-
-let push t s =
-  Stack.push t s.stack
-
-let canonicalize l =
-  let has_elt = List.exists (function Element _ -> true | _ -> false) l in
-  if has_elt then List.filter (function PCData s -> not (is_blank s) | _ -> true) l
-  else l
-
-let rec read_xml do_not_canonicalize s =
-  let rec read_node s =
-    match pop s with
-      | Xml_lexer.PCData s -> PCData s
-      | Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, [])
-      | Xml_lexer.Tag (tag, attr, false) ->
-        let elements = read_elems tag s in
-        let elements =
-          if do_not_canonicalize then elements else canonicalize elements
-        in
-        Element (tag, attr, elements)
-      | t ->
-        push t s;
-        raise NoMoreData
-
-  and read_elems tag s =
-    let elems = ref [] in
-    (try
-       while true do
-         let node = read_node s in
-         match node, !elems with
-           | PCData c , (PCData c2) :: q ->
-             elems := PCData (c2 ^ c) :: q
-           | _, l ->
-             elems := node :: l
-       done
-     with
-         NoMoreData -> ());
-    match pop s with
-      | Xml_lexer.Endtag s when s = tag -> List.rev !elems
-      | t -> raise (Internal_error (EndOfTagExpected tag))
-  in
-  match read_node s with
-    | (Element _) as node ->
-      node
-    | PCData c ->
-      if is_blank c then
-        read_xml do_not_canonicalize s
-      else
-        raise (Xml_lexer.Error Xml_lexer.ENodeExpected)
-
-let convert = function
-  | Xml_lexer.EUnterminatedComment -> UnterminatedComment
-  | Xml_lexer.EUnterminatedString -> UnterminatedString
-  | Xml_lexer.EIdentExpected -> IdentExpected
-  | Xml_lexer.ECloseExpected -> CloseExpected
-  | Xml_lexer.ENodeExpected -> NodeExpected
-  | Xml_lexer.EAttributeNameExpected -> AttributeNameExpected
-  | Xml_lexer.EAttributeValueExpected -> AttributeValueExpected
-  | Xml_lexer.EUnterminatedEntity ->      UnterminatedEntity
-
-let error_of_exn xparser = function
-  | NoMoreData when pop xparser = Xml_lexer.Eof -> Empty
-  | NoMoreData -> NodeExpected
-  | Internal_error e -> e
-  | Xml_lexer.Error e -> convert e
-  | e ->
-    (*let e = Errors.push e in: We do not record backtrace here. *)
-    raise e
-
-let do_parse do_not_canonicalize xparser =
-  try
-    Xml_lexer.init xparser.source;
-    let x = read_xml do_not_canonicalize xparser in
-    if xparser.check_eof && pop xparser <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
-    Xml_lexer.close ();
-    x
-  with any ->
-    Xml_lexer.close ();
-    raise (!xml_error (error_of_exn xparser any) xparser.source)
-
-let parse ?(do_not_canonicalize=false) p =
-  do_parse do_not_canonicalize p
-
-let error_msg = function
-  | UnterminatedComment -> "Unterminated comment"
-  | UnterminatedString -> "Unterminated string"
-  | UnterminatedEntity -> "Unterminated entity"
-  | IdentExpected -> "Ident expected"
-  | CloseExpected -> "Element close expected"
-  | NodeExpected -> "Xml node expected"
-  | AttributeNameExpected -> "Attribute name expected"
-  | AttributeValueExpected -> "Attribute value expected"
-  | EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag
-  | EOFExpected -> "End of file expected"
-  | Empty -> "Empty"
-
-let error (msg,pos) =
-  if pos.emin = pos.emax then
-    sprintf "%s line %d character %d" (error_msg msg) pos.eline
-      (pos.emin - pos.eline_start)
-  else
-    sprintf "%s line %d characters %d-%d" (error_msg msg) pos.eline
-      (pos.emin - pos.eline_start) (pos.emax - pos.eline_start)
-
-let line e = e.eline
-
-let range e =
-  e.emin - e.eline_start , e.emax - e.eline_start
-
-let abs_range e =
-  e.emin , e.emax
-
-let pos source =
-  let line, lstart, min, max = Xml_lexer.pos source in
-  {
-    eline = line;
-    eline_start = lstart;
-    emin = min;
-    emax = max;
-  }
-
-let () = _raises (fun x p ->
-        (* local cast : Xml.error_msg -> error_msg *)
-  Error (x, pos p))
-  (fun f -> File_not_found f)
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
deleted file mode 100644
index ac2eab352..000000000
--- a/lib/xml_parser.mli
+++ /dev/null
@@ -1,106 +0,0 @@
-(*
- * Xml Light, an small Xml parser/printer with DTD support.
- * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License as published by the Free Software Foundation; either
- * version 2.1 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this library; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
- *)
-
-(** Xml Light Parser
-
- While basic parsing functions can be used in the {!Xml} module, this module
- is providing a way to create, configure and run an Xml parser.
-
-*)
-
-
-(** An Xml node is either
-        [Element (tag-name, attributes, children)] or [PCData text] *)
-type xml = Xml_datatype.xml
-
-(** Abstract type for an Xml parser. *)
-type t
-
-(** {6:exc Xml Exceptions} *)
-
-(** Several exceptions can be raised when parsing an Xml document : {ul
-        {li {!Xml.Error} is raised when an xml parsing error occurs. the
-                {!Xml.error_msg} tells you which error occurred during parsing
-                and the {!Xml.error_pos} can be used to retrieve the document
-                location where the error occurred at.}
-        {li {!Xml.File_not_found} is raised when an error occurred while
-                opening a file with the {!Xml.parse_file} function.}
-        }
- *)
-
-type error_pos
-
-type error_msg =
-        | UnterminatedComment
-        | UnterminatedString
-        | UnterminatedEntity
-        | IdentExpected
-        | CloseExpected
-        | NodeExpected
-        | AttributeNameExpected
-        | AttributeValueExpected
-        | EndOfTagExpected of string
-        | EOFExpected
-        | Empty
-
-type error = error_msg * error_pos
-
-exception Error of error
-
-exception File_not_found of string
-
-(** Get a full error message from an Xml error. *)
-val error : error -> string
-
-(** Get the Xml error message as a string. *)
-val error_msg : error_msg -> string
-
-(** Get the line the error occurred at. *)
-val line : error_pos -> int
-
-(** Get the relative character range (in current line) the error occurred at.*)
-val range : error_pos -> int * int
-
-(** Get the absolute character range the error occurred at. *)
-val abs_range : error_pos -> int * int
-
-val pos : Lexing.lexbuf -> error_pos
-
-(** Several kind of resources can contain Xml documents. *)
-type source =
-| SChannel of in_channel
-| SString of string
-| SLexbuf of Lexing.lexbuf
-
-(** This function returns a new parser with default options. *)
-val make : source -> t
-
-(** When a Xml document is parsed, the parser may check that the end of the
- document is reached, so for example parsing ["<A/><B/>"] will fail instead
- of returning only the A element. You can turn on this check by setting
- [check_eof] to [true] {i (by default, check_eof is false, unlike
- in the original Xmllight)}. *)
-val check_eof : t -> bool -> unit
-
-(** Once the parser is configured, you can run the parser on a any kind
-    of xml document source to parse its contents into an Xml data structure.
-
-    When [do_not_canonicalize] is set, the XML document is given as
-    is, without trying to remove blank PCDATA elements. *)
-val parse : ?do_not_canonicalize:bool -> t -> xml
diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml
deleted file mode 100644
index e7e4d0ceb..000000000
--- a/lib/xml_printer.ml
+++ /dev/null
@@ -1,145 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Xml_datatype
-
-type xml = Xml_datatype.xml
-
-type target = TChannel of out_channel | TBuffer of Buffer.t
-
-type t = target
-
-let make x = x
-
-let buffer_pcdata tmp text =
-  let output = Buffer.add_string tmp in
-  let output' = Buffer.add_char tmp in
-  let l = String.length text in
-  for p = 0 to l-1 do
-    match text.[p] with
-      | ' ' -> output "&nbsp;";
-      | '>' -> output "&gt;"
-      | '<' -> output "&lt;"
-      | '&' ->
-        if p < l - 1 && text.[p + 1] = '#' then
-          output' '&'
-        else
-          output "&amp;"
-      | '\'' -> output "&apos;"
-      | '"' -> output "&quot;"
-      | c -> output' c
-  done
-
-let buffer_attr tmp (n,v) =
-  let output = Buffer.add_string tmp in
-  let output' = Buffer.add_char tmp in
-  output' ' ';
-  output n;
-  output "=\"";
-  let l = String.length v in
-  for p = 0 to l - 1 do
-    match v.[p] with
-      | '\\' -> output "\\\\"
-      | '"' -> output "\\\""
-      | '<' -> output "&lt;"
-      | '&' -> output "&amp;"
-      | c -> output' c
-  done;
-  output' '"'
-
-let to_buffer tmp x =
-  let pcdata = ref false in
-  let output = Buffer.add_string tmp in
-  let output' = Buffer.add_char tmp in
-  let rec loop = function
-    | Element (tag,alist,[]) ->
-      output' '<';
-      output tag;
-      List.iter (buffer_attr tmp) alist;
-      output "/>";
-      pcdata := false;
-    | Element (tag,alist,l) ->
-      output' '<';
-      output tag;
-      List.iter (buffer_attr tmp) alist;
-      output' '>';
-      pcdata := false;
-      List.iter loop l;
-      output "</";
-      output tag;
-      output' '>';
-      pcdata := false;
-    | PCData text ->
-      if !pcdata then output' ' ';
-      buffer_pcdata tmp text;
-      pcdata := true;
-  in
-  loop x
-
-let pcdata_to_string s =
-  let b = Buffer.create 13 in
-  buffer_pcdata b s;
-  Buffer.contents b
-
-let to_string x =
-  let b = Buffer.create 200 in
-  to_buffer b x;
-  Buffer.contents b
-
-let to_string_fmt x =
-  let tmp = Buffer.create 200 in
-  let output = Buffer.add_string tmp in
-  let output' = Buffer.add_char tmp in
-  let rec loop ?(newl=false) tab = function
-    | Element (tag, alist, []) ->
-      output tab;
-      output' '<';
-      output tag;
-      List.iter (buffer_attr tmp) alist;
-      output "/>";
-      if newl then output' '\n';
-    | Element (tag, alist, [PCData text]) ->
-      output tab;
-      output' '<';
-      output tag;
-      List.iter (buffer_attr tmp) alist;
-      output ">";
-      buffer_pcdata tmp text;
-      output "</";
-      output tag;
-      output' '>';
-      if newl then output' '\n';
-    | Element (tag, alist, l) ->
-      output tab;
-      output' '<';
-      output tag;
-      List.iter (buffer_attr tmp) alist;
-      output ">\n";
-      List.iter (loop ~newl:true (tab^"  ")) l;
-      output tab;
-      output "</";
-      output tag;
-      output' '>';
-      if newl then output' '\n';
-    | PCData text ->
-      buffer_pcdata tmp text;
-      if newl then output' '\n';
-  in
-  loop "" x;
-  Buffer.contents tmp
-
-let print t xml =
-  let tmp, flush = match t with
-    | TChannel oc ->
-      let b = Buffer.create 200 in
-      b, (fun () -> Buffer.output_buffer oc b; flush oc)
-    | TBuffer b ->
-      b, (fun () -> ())
-  in
-  to_buffer tmp xml;
-  flush ()
diff --git a/lib/xml_printer.mli b/lib/xml_printer.mli
deleted file mode 100644
index f24f51fff..000000000
--- a/lib/xml_printer.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-type xml = Xml_datatype.xml
-
-type t
-type target = TChannel of out_channel | TBuffer of Buffer.t
-
-val make : target -> t
-
-(** Print the xml data structure to a source into a compact xml string (without
- any user-readable formating ). *)
-val print : t -> xml -> unit
-
-(** Print the xml data structure into a compact xml string (without
- any user-readable formating ). *)
-val to_string : xml -> string
-
-(** Print the xml data structure into an user-readable string with
- tabs and lines break between different nodes. *)
-val to_string_fmt : xml -> string
-
-(** Print PCDATA as a string by escaping XML entities. *)
-val pcdata_to_string : string -> string