Imported Upstream version 8.6upstream/8.6

68 files changed, 1780 insertions, 2303 deletions

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index f7bd81f8..0f0f09aa 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -17,6 +17,10 @@ let version = 1
 
 let oc = ref None
 
+let chop_extension f =
+  if check_suffix f ".v" then chop_extension f
+  else f
+
 let aux_file_name_for vfile =
   dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux"
 
@@ -25,9 +29,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 +91,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 127827ab..86e322b7 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/ephemeron.ml b/lib/cEphemeron.ml
index a38ea11e..a38ea11e 100644
--- a/lib/ephemeron.ml
+++ b/lib/cEphemeron.ml
diff --git a/lib/ephemeron.mli b/lib/cEphemeron.mli
index 1200e4e2..1200e4e2 100644
--- a/lib/ephemeron.mli
+++ b/lib/cEphemeron.mli
diff --git a/lib/errors.ml b/lib/cErrors.ml
index c1d224df..5c56192f 100644
--- a/lib/errors.ml
+++ b/lib/cErrors.ml
@@ -16,6 +16,23 @@ let push = Backtrace.add_backtrace
 
 exception Anomaly of string option * std_ppcmds (* System errors *)
 
+(* XXX: To move to common tagging functions in Pp, blocked on tag
+ * system cleanup as we cannot define generic error tags now.
+ *
+ * Anyways, tagging should not happen here, but in the specific
+ * listener to the msg_* stuff.
+ *)
+let tag_err_str s = tag Ppstyle.(Tag.inj error_tag tag) (str s) ++ spc ()
+let err_str       = tag_err_str "Error:"
+let ann_str       = tag_err_str "Anomaly:"
+
+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)
 
@@ -86,7 +103,9 @@ let print_backtrace e = match Backtrace.get_backtrace e with
 
 let print_anomaly askreport e =
   if askreport then
-    hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.")
+    hov 0 (ann_str ++ raw_anomaly e ++ spc () ++
+           strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
+           str ".")
   else
     hov 0 (raw_anomaly e)
 
@@ -106,7 +125,7 @@ let iprint_no_report (e, info) =
 
 let _ = register_handler begin function
   | UserError(s, pps) ->
-    hov 0 (str "Error: " ++ where (Some s) ++ pps)
+    hov 0 (err_str ++ where (Some s) ++ pps)
   | _ -> raise Unhandled
 end
 
@@ -137,5 +156,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 e5dad93f..e5dad93f 100644
--- a/lib/errors.mli
+++ b/lib/cErrors.mli
diff --git a/lib/cList.ml b/lib/cList.ml
index 0ac372d8..c8283e3c 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,[])
@@ -567,19 +601,35 @@ let filter2 f l1 l2 =
   filter2_loop f c1 c2 l1 l2;
   (c1.tail, c2.tail)
 
-let rec map_filter f = function
-  | [] -> []
-  | x::l ->
-      let l' = map_filter f l in
-      match f x with None -> l' | Some y -> y::l'
+let rec map_filter_loop f p = function
+  | [] -> ()
+  | x :: l ->
+    match f x with
+    | None -> map_filter_loop f p l
+    | Some y ->
+      let c = { head = y; tail = [] } in
+      p.tail <- cast c;
+      map_filter_loop f c l
+
+let map_filter f l =
+  let c = { head = Obj.magic 0; tail = [] } in
+  map_filter_loop f c l;
+  c.tail
 
-let map_filter_i f =
-  let rec aux i = function
-    | [] -> []
-    | x::l ->
-      let l' = aux (succ i) l in
-        match f i x with None -> l' | Some y -> y::l'
-  in aux 0
+let rec map_filter_i_loop f i p = function
+  | [] -> ()
+  | x :: l ->
+    match f i x with
+    | None -> map_filter_i_loop f (succ i) p l
+    | Some y ->
+      let c = { head = y; tail = [] } in
+      p.tail <- cast c;
+      map_filter_i_loop f (succ i) c l
+
+let map_filter_i f l =
+  let c = { head = Obj.magic 0; tail = [] } in
+  map_filter_i_loop f 0 c l;
+  c.tail
 
 let rec filter_with filter l = match filter, l with
 | [], [] -> []
@@ -638,12 +688,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 19eeb250..bc8749b4 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 665e1a21..ba0873ff 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
@@ -26,10 +34,17 @@ sig
   val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
   val smartmap : ('a -> 'a) -> 'a t -> 'a t
   val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
+  val height : 'a t -> int
   module Unsafe :
   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) :
@@ -43,10 +58,17 @@ sig
   val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
   val smartmap : ('a -> 'a) -> 'a map -> 'a map
   val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map
+  val height : 'a map -> int
   module Unsafe :
   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
@@ -148,6 +170,10 @@ struct
     if l == l' && r == r' && v == v' then s
     else map_inj (MNode (l', k, v', r', h))
 
+  let height s = match map_prj s with
+  | MEmpty -> 0
+  | MNode (_, _, _, _, h) -> h
+
   module Unsafe =
   struct
 
@@ -159,10 +185,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 2f243da8..2838b374 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. *)
@@ -51,6 +61,9 @@ sig
   val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
   (** As [mapi] but tries to preserve sharing. *)
 
+  val height : 'a t -> int
+  (** An indication of the logarithmic size of a map *)
+
   module Unsafe :
   sig
     val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
@@ -59,6 +72,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/cSet.ml b/lib/cSet.ml
index 3eeff29f..037cdc35 100644
--- a/lib/cSet.ml
+++ b/lib/cSet.ml
@@ -57,7 +57,7 @@ struct
     open Hashset.Combine
     type t = set
     type u = M.t -> M.t
-    let equal s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 [])
+    let eq s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 [])
     let hash s = Set.fold (fun v accu -> combine (H.hash v) accu) s 0
     let hashcons = umap
   end
diff --git a/lib/cSig.mli b/lib/cSig.mli
index e095c82c..151cfbdc 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 00000000..cc2463e2
--- /dev/null
+++ b/lib/cWarnings.ml
@@ -0,0 +1,188 @@
+(************************************************************************)
+(*  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 refine_loc = function
+  | None when not (Loc.is_ghost !current_loc) -> Some !current_loc
+  | loc -> loc
+
+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 ->
+              begin match refine_loc loc with
+              | Some loc -> CErrors.user_err_loc (loc,"_",pp x)
+              | None -> CErrors.errorlabstrm "_" (pp x)
+              end
+           | Enabled ->
+              let msg =
+                pp x ++ spc () ++ str "[" ++ str name ++ str "," ++
+                  str category ++ str "]"
+              in
+              let loc = refine_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 -> ()
+
+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 set_category_status ~name status =
+  let names = Hashtbl.find categories name in
+  List.iter (fun name -> set_warning_status name status) names
+
+let is_all_keyword name = CString.equal name "all"
+let is_none_keyword s = CString.equal s "none"
+
+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 string_of_flag (status,name) =
+  match status with
+  | AsError -> "+" ^ name
+  | Disabled -> "-" ^ name
+  | Enabled -> name
+
+let string_of_flags flags =
+  String.concat "," (List.map string_of_flag flags)
+
+let set_status ~name status =
+  if is_all_keyword name then
+    set_all_warnings_status status
+  else
+    try
+      set_category_status ~name status
+    with Not_found ->
+         try
+           set_warning_status ~name status
+         with Not_found -> ()
+
+let split_flags s =
+  let reg = Str.regexp "[ ,]+" in Str.split reg s
+
+let check_warning ~silent (_status,name) =
+  is_all_keyword name ||
+  Hashtbl.mem categories name ||
+  Hashtbl.mem warnings name ||
+  (if not silent then warn_unknown_warning name; false)
+
+(** [cut_before_all_rev] removes all flags subsumed by a later occurrence of the
+    "all" flag, and reverses the list. *)
+let rec cut_before_all_rev acc = function
+  | [] -> acc
+  | (_status,name as w) :: warnings ->
+     cut_before_all_rev (w :: if is_all_keyword name then [] else acc) warnings
+
+let cut_before_all_rev warnings = cut_before_all_rev [] warnings
+
+(** [uniquize_flags_rev] removes flags that are subsumed by later occurrences of
+    themselves or their categories, and reverses the list. *)
+let uniquize_flags_rev flags =
+  let rec aux acc visited = function
+    | (_,name as flag)::flags ->
+       if CString.Set.mem name visited then aux acc visited flags else
+         let visited =
+           try
+             let warnings = Hashtbl.find categories name in
+             List.fold_left (fun v w -> CString.Set.add w v) visited warnings
+           with Not_found ->
+             visited
+         in
+         aux (flag::acc) (CString.Set.add name visited) flags
+    | [] -> acc
+  in aux [] CString.Set.empty flags
+
+(** [normalize_flags] removes unknown or redundant warnings. If [silent] is
+    true, it emits a warning when an unknown warning is met. *)
+let normalize_flags ~silent warnings =
+  let warnings = List.filter (check_warning ~silent) warnings in
+  let warnings = cut_before_all_rev warnings in
+  uniquize_flags_rev warnings
+
+let flags_of_string s = List.map parse_flag (split_flags s)
+
+let normalize_flags_string s =
+  if is_none_keyword s then s
+  else
+    let flags = flags_of_string s in
+    let flags = normalize_flags ~silent:false flags in
+    string_of_flags flags
+
+let rec parse_warnings items =
+  CList.iter (fun (status, name) -> set_status ~name status) items
+
+(* For compatibility, we accept "none" *)
+let parse_flags s =
+  if is_none_keyword s then begin
+      Flags.make_warn false;
+      set_all_warnings_status Disabled;
+      "none"
+    end
+  else begin
+      Flags.make_warn true;
+      let flags = flags_of_string s in
+      let flags = normalize_flags ~silent:true flags in
+      parse_warnings flags;
+      string_of_flags flags
+    end
+
+let set_flags s =
+  reset_default_warnings (); let s = parse_flags s in flags := s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
new file mode 100644
index 00000000..3f6cee31
--- /dev/null
+++ b/lib/cWarnings.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*  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
+
+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 get_flags : unit -> string
+val set_flags : string -> unit
+
+(** Cleans up a user provided warnings status string, e.g. removing unknown
+    warnings (in which case a warning is emitted) or subsumed warnings . *)
+val normalize_flags_string : string -> string
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 9c9607ab..1e33173e 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 04b32870..65d1442a 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 c040d8b0..448b11a1 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 679e3fdf..89ce5283 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 d95b6f09..90a42859 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 587db115..aa7bddf2 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 cce0c6bc..44b3ee35 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,189 @@ 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 ?pp_tag fmt strm = msg_with ?pp_tag fmt (strm ++ fnl ())
+
+(* 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 = tag Ppstyle.(Tag.inj debug_tag   tag) (str "Debug:")   ++ spc ()
+let info_str = mt ()
+let warn_str = tag Ppstyle.(Tag.inj warning_tag tag) (str "Warning:") ++ spc ()
+let  err_str = tag Ppstyle.(Tag.inj error_tag   tag) (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 ?pp_tag ?loc level msg = match level with
+  | Debug   -> msgnl_with ?pp_tag !std_ft (make_body dbg  dbg_str ?loc msg)
+  | Info    -> msgnl_with ?pp_tag !std_ft (make_body dbg info_str ?loc msg)
+  | Notice  -> msgnl_with ?pp_tag !std_ft msg
+  | Warning -> Flags.if_warn (fun () ->
+               msgnl_with ?pp_tag !err_ft (make_body err warn_str ?loc msg)) ()
+  | Error   -> msgnl_with ?pp_tag !err_ft (make_body err  err_str ?loc msg)
+
+(* We provide a generic clear_log_backend callback for backends
+   wanting to do clenaup after the print.
+*)
+let std_logger_tag     = ref None
+let std_logger_cleanup = ref (fun () -> ())
+
+let std_logger ?loc level msg =
+  gen_logger (fun x -> x) (fun x -> x) ?pp_tag:!std_logger_tag ?loc level msg;
+  !std_logger_cleanup ()
+
+(* Rules for emacs:
+   - Debug/info: emacs_quote_info
+   - Warning/Error: emacs_quote_err
+   - Notice: unquoted
+
+  Note the inconsistency.
+ *)
+let emacs_logger = gen_logger emacs_quote_info emacs_quote_err ?pp_tag:None
+
+(** Color logging. Moved from pp_style, it may need some more refactoring  *)
+
+(** Not thread-safe. We should put a lock somewhere if we print from
+    different threads. Do we? *)
+let make_style_stack () =
+  (** Default tag is to reset everything *)
+  let empty = Terminal.make () in
+  let default_tag = Terminal.({
+      fg_color = Some `DEFAULT;
+      bg_color = Some `DEFAULT;
+      bold = Some false;
+      italic = Some false;
+      underline = Some false;
+      negative = Some false;
+    })
+  in
+  let style_stack = ref [] in
+  let peek () = match !style_stack with
+  | []      -> default_tag  (** Anomalous case, but for robustness *)
+  | st :: _ -> st
+  in
+  let push tag =
+    let style = match Ppstyle.get_style tag with
+      | None    -> empty
+      | Some st -> st
+    in
+    (** Use the merging of the latest tag and the one being currently pushed.
+    This may be useful if for instance the latest tag changes the background and
+    the current one the foreground, so that the two effects are additioned. *)
+    let style = Terminal.merge (peek ()) style in
+    style_stack := style :: !style_stack;
+    Terminal.eval style
+  in
+  let pop _ = match !style_stack with
+  | []       -> (** Something went wrong, we fallback *)
+                Terminal.eval default_tag
+  | _ :: rem -> style_stack := rem;
+                Terminal.eval (peek ())
+  in
+  let clear () = style_stack := [] in
+  push, pop, clear
+
+let init_color_output () =
+  let open Pp_control in
+  let push_tag, pop_tag, clear_tag = make_style_stack () in
+  std_logger_cleanup := clear_tag;
+  std_logger_tag     := Some Ppstyle.pp_tag;
+  let tag_handler = {
+    Format.mark_open_tag   = push_tag;
+    Format.mark_close_tag  = pop_tag;
+    Format.print_open_tag  = ignore;
+    Format.print_close_tag = ignore;
+  } 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 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 feeders = ref []
+let add_feeder f = feeders := f :: !feeders
+
+let debug_feeder = function
+  | { contents = Message (Debug, loc, pp) } ->
+       msg_debug ?loc (Pp.str (Richpp.raw_print pp))
+  | _ -> ()
+
+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 =
+  let m = {
+     contents = what;
+     route = Option.default !feedback_route route;
+     id    = Option.default !feedback_id id;
+  } in
+  List.iter (fun f -> f m) !feeders
+
+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 16286762..5160bd5b 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
+
+(** [init_color_output ()] Enable color in the std_logger *)
+val init_color_output : unit -> unit
+
+(** [feedback_logger] will produce feedback messages instead IO events *)
+val feedback_logger : logger
+val emacs_logger    : logger
+
+
+(** [add_feeder] feeders observe the feedback *)
+val add_feeder : (feedback -> unit) -> unit
+
+(** Prints feedback messages of kind Message(Debug,_) using msg_debug *)
+val debug_feeder : feedback -> 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 2c23ec98..0e2f7e5a 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 [ "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,31 +108,37 @@ 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
-| Current, Current -> false
-| V8_3, V8_2 -> true
-| V8_4, (V8_2 | V8_3) -> true
-| Current, (V8_2 | V8_3 | V8_4) -> true
-
+let version_compare v1 v2 = match v1, v2 with
+| V8_2, V8_2 -> 0
+| V8_2, (V8_3 | V8_4 | V8_5 | Current) -> -1
+| V8_3, V8_2 -> 1
+| V8_3, V8_3 -> 0
+| V8_3, (V8_4 | V8_5 | Current) -> -1
+| V8_4, (V8_2 | V8_3) -> 1
+| V8_4, V8_4 -> 0
+| V8_4, (V8_5 | Current) -> -1
+| V8_5, (V8_2 | V8_3 | V8_4) -> 1
+| V8_5, V8_5 -> 0
+| V8_5, Current -> -1
+| Current, Current -> 0
+| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> 1
+
+let version_strictly_greater v = version_compare !compat_version v > 0
 let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
   | V8_2 -> "8.2"
   | V8_3 -> "8.3"
   | V8_4 -> "8.4"
+  | V8_5 -> "8.5"
   | Current -> "current"
 
 (* Translate *)
 let beautify = ref false
-let make_beautify f = beautify := f
-let do_beautify () = !beautify
 let beautify_file = ref false
 
 (* Silent / Verbose *)
@@ -164,7 +175,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 +206,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 +228,8 @@ let native_compiler = ref false
 let print_mod_uid = ref false
 
 let tactic_context_compat = ref false
+let profile_ltac = ref false
+let profile_ltac_cutoff = ref 2.0
 
 let dump_bytecode = ref false
 let set_dump_bytecode = (:=) dump_bytecode
diff --git a/lib/flags.mli b/lib/flags.mli
index ab06eda3..89760264 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,15 +62,14 @@ 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_compare : compat_version -> compat_version -> int
 val version_strictly_greater : compat_version -> bool
 val version_less_or_equal : compat_version -> bool
 val pr_version : compat_version -> string
 
 val beautify : bool ref
-val make_beautify : bool -> unit
-val do_beautify : unit -> bool
 val beautify_file : bool ref
 
 val make_silent : bool -> unit
@@ -90,6 +94,7 @@ val is_universe_polymorphism : unit -> bool
 val make_polymorphic_flag : bool -> unit
 val use_polymorphic_flag : unit -> bool
 
+val warn : bool ref
 val make_warn : bool -> unit
 val if_warn : ('a -> unit) -> 'a -> unit
 
@@ -122,8 +127,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
 
@@ -142,6 +147,9 @@ 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
+val profile_ltac_cutoff : float 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 5cd2beba..ea0382a6 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,11 +59,11 @@ 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 =
-  | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) Ephemeron.key
+  | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) CEphemeron.key
   | Finished of 'a
 
 and 'a computation = 'a comput ref
@@ -70,13 +71,13 @@ and 'a computation = 'a comput ref
 let unnamed = "unnamed"
 
 let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x =
-  ref (Ongoing (name, Ephemeron.create (uuid, f, Pervasives.ref x)))
+  ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x)))
 let get x =
   match !x with
   | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None))
   | Ongoing (name, x) ->
-      try let uuid, fix, c = Ephemeron.get x in name, uuid, fix, c
-      with Ephemeron.InvalidKey ->
+      try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c
+      with CEphemeron.InvalidKey ->
         name, UUID.invalid, id, ref (Exn (NotHere name, Exninfo.null))
 
 type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn  ]
@@ -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 58f0a71a..114c5917 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 cba54c11..05c828d5 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 671d96b7..d7ad9b93 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 ba6aad91..ea76e742 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -68,34 +68,91 @@ struct
         Int.Map.update h m s
     with Not_found -> s
 
+  let height s = Int.Map.height s
+
+  let is_smaller s1 s2 = height s1 <= height s2 + 3
+
+  (** Assumes s1 << s2 *)
+  let fast_union s1 s2 =
+    let fold h s accu =
+      try Int.Map.modify h (fun _ s' -> Set.fold Set.add s s') accu
+      with Not_found -> Int.Map.add h s accu
+    in
+    Int.Map.fold fold s1 s2
+
   let union s1 s2 =
-    let fu _ m1 m2 = match m1, m2 with
-    | None, None -> None
-    | (Some _ as m), None | None, (Some _ as m) -> m
-    | Some m1, Some m2 -> Some (Set.union m1 m2)
+    if is_smaller s1 s2 then fast_union s1 s2
+    else if is_smaller s2 s1 then fast_union s2 s1
+    else
+      let fu _ m1 m2 = match m1, m2 with
+      | None, None -> None
+      | (Some _ as m), None | None, (Some _ as m) -> m
+      | Some m1, Some m2 -> Some (Set.union m1 m2)
+      in
+      Int.Map.merge fu s1 s2
+
+  (** Assumes s1 << s2 *)
+  let fast_inter s1 s2 =
+    let fold h s accu =
+      try
+        let s' = Int.Map.find h s2 in
+        let si = Set.filter (fun e -> Set.mem e s') s in
+        if Set.is_empty si then accu
+        else Int.Map.add h si accu
+     with Not_found -> accu
     in
-    Int.Map.merge fu s1 s2
+    Int.Map.fold fold s1 Int.Map.empty
 
   let inter s1 s2 =
-    let fu _ m1 m2 = match m1, m2 with
-    | None, None -> None
-    | Some _, None | None, Some _ -> None
-    | Some m1, Some m2 ->
-      let m = Set.inter m1 m2 in
-      if Set.is_empty m then None else Some m
+    if is_smaller s1 s2 then fast_inter s1 s2
+    else if is_smaller s2 s1 then fast_inter s2 s1
+    else
+      let fu _ m1 m2 = match m1, m2 with
+      | None, None -> None
+      | Some _, None | None, Some _ -> None
+      | Some m1, Some m2 ->
+        let m = Set.inter m1 m2 in
+        if Set.is_empty m then None else Some m
+      in
+      Int.Map.merge fu s1 s2
+
+  (** Assumes s1 << s2 *)
+  let fast_diff_l s1 s2 =
+    let fold h s accu =
+      try
+        let s' = Int.Map.find h s2 in
+        let si = Set.filter (fun e -> not (Set.mem e s')) s in
+        if Set.is_empty si then accu
+        else Int.Map.add h si accu
+     with Not_found -> Int.Map.add h s accu
     in
-    Int.Map.merge fu s1 s2
+    Int.Map.fold fold s1 Int.Map.empty
+
+  (** Assumes s2 << s1 *)
+  let fast_diff_r s1 s2 =
+    let fold h s accu =
+      try
+        let s' = Int.Map.find h accu in
+        let si = Set.filter (fun e -> not (Set.mem e s)) s' in
+        if Set.is_empty si then Int.Map.remove h accu
+        else Int.Map.update h si accu
+     with Not_found -> accu
+    in
+    Int.Map.fold fold s2 s1
 
   let diff s1 s2 =
-    let fu _ m1 m2 = match m1, m2 with
-    | None, None -> None
-    | (Some _ as m), None -> m
-    | None, Some _ -> None
-    | Some m1, Some m2 ->
-      let m = Set.diff m1 m2 in
-      if Set.is_empty m then None else Some m
-    in
-    Int.Map.merge fu s1 s2
+    if is_smaller s1 s2 then fast_diff_l s1 s2
+    else if is_smaller s2 s2 then fast_diff_r s1 s2
+    else
+      let fu _ m1 m2 = match m1, m2 with
+      | None, None -> None
+      | (Some _ as m), None -> m
+      | None, Some _ -> None
+      | Some m1, Some m2 ->
+        let m = Set.diff m1 m2 in
+        if Set.is_empty m then None else Some m
+      in
+      Int.Map.merge fu s1 s2
 
   let compare s1 s2 = Int.Map.compare Set.compare s1 s2
 
@@ -286,6 +343,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 =
@@ -322,6 +381,8 @@ struct
     let fs m = Map.smartmapi f m in
     Int.Map.smartmap fs s
 
+  let height s = Int.Map.height s
+
   module Unsafe =
   struct
     let map f s =
@@ -329,4 +390,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 144d9513..4eaacf91 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -15,7 +15,7 @@
  *   of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...).
  * [hashcons u x] is a function that hash-cons the sub-structures of x using
  *   the hash-consing functions u provides.
- * [equal] is a comparison function. It is allowed to use physical equality
+ * [eq] is a comparison function. It is allowed to use physical equality
  *   on the sub-terms hash-consed by the hashcons function.
  * [hash] is the hash function given to the Hashtbl.Make function
  *
@@ -27,7 +27,7 @@ module type HashconsedType =
     type t
     type u
     val hashcons :  u -> t -> t
-    val equal : t -> t -> bool
+    val eq : t -> t -> bool
     val hash : t -> int
   end
 
@@ -53,7 +53,7 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) =
 
     (* We create the type of hashtables for t, with our comparison fun.
      * An invariant is that the table never contains two entries equals
-     * w.r.t (=), although the equality on keys is X.equal. This is
+     * w.r.t (=), although the equality on keys is X.eq. This is
      * granted since we hcons the subterms before looking up in the table.
      *)
     module Htbl = Hashset.Make(X)
@@ -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.  *)
 
@@ -124,7 +110,7 @@ module Hlist (D:HashedType) =
       let hashcons (hrec,hdata) = function
         | x :: l -> hdata x :: hrec l
         | l -> l
-      let equal l1 l2 =
+      let eq l1 l2 =
         l1 == l2 ||
           match l1, l2 with
           | [], [] -> true
@@ -144,7 +130,7 @@ module Hstring = Make(
     type t = string
     type u = unit
     let hashcons () s =(* incr accesstr;*) s
-    external equal : string -> string -> bool = "caml_string_equal" "noalloc"
+    external eq : string -> string -> bool = "caml_string_equal" "noalloc"
     (** Copy from CString *)
     let rec hash len s i accu =
       if i = len then accu
@@ -191,21 +177,6 @@ module Hobj = Make(
     type t = Obj.t
     type u = (Obj.t -> Obj.t) * unit
     let hashcons (hrec,_) = hash_obj hrec
-    let equal = comp_obj
+    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/hashcons.mli b/lib/hashcons.mli
index 04754ba1..150899ce 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -14,9 +14,9 @@ module type HashconsedType =
   sig
     (** {6 Generic hashconsing signature}
 
-        Given an equivalence relation [equal], a hashconsing function is a
+        Given an equivalence relation [eq], a hashconsing function is a
         function that associates the same canonical element to two elements
-        related by [equal]. Usually, the element chosen is canonical w.r.t.
+        related by [eq]. Usually, the element chosen is canonical w.r.t.
         physical equality [(==)], so as to reduce memory consumption and
         enhance efficiency of equality tests.
 
@@ -32,15 +32,15 @@ module type HashconsedType =
         Usually a tuple of functions. *)
     val hashcons :  u -> t -> t
     (** The actual hashconsing function, using its fist argument to recursively
-        hashcons substructures. It should be compatible with [equal], that is
-        [equal x (hashcons f x) = true]. *)
-    val equal : t -> t -> bool
+        hashcons substructures. It should be compatible with [eq], that is
+        [eq x (hashcons f x) = true]. *)
+    val eq : t -> t -> bool
     (** A comparison function. It is allowed to use physical equality
         on the sub-terms hashconsed by the [hashcons] function, but it should be
         insensible to shallow copy of the compared object. *)
     val hash : t -> int
     (** A hash function passed to the underlying hashtable structure. [hash]
-        should be compatible with [equal], i.e. if [equal x y = true] then
+        should be compatible with [eq], i.e. if [eq x y = true] then
         [hash x = hash y]. *)
   end
 
diff --git a/lib/hashset.ml b/lib/hashset.ml
index 6fb78f9a..af33544d 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -16,7 +16,7 @@
 
 module type EqType = sig
   type t
-  val equal : t -> t -> bool
+  val eq : t -> t -> bool
 end
 
 type statistics = {
@@ -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
@@ -183,7 +183,7 @@ module Make (E : EqType) =
       if i >= sz then ifnotfound index
       else if h = hashes.(i) then begin
         match Weak.get bucket i with
-        | Some v when E.equal v d -> v
+        | Some v when E.eq v d -> v
         | _ -> loop (i + 1)
       end else loop (i + 1)
     in
diff --git a/lib/hashset.mli b/lib/hashset.mli
index 05d4fe37..733c8962 100644
--- a/lib/hashset.mli
+++ b/lib/hashset.mli
@@ -16,7 +16,7 @@
 
 module type EqType = sig
   type t
-  val equal : t -> t -> bool
+  val eq : t -> t -> bool
 end
 
 type statistics = {
diff --git a/lib/heap.ml b/lib/heap.ml
index 187189fc..97ccadeb 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 c9f4d4a1..26a666e1 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 f3f6ad8f..8791f074 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
@@ -15,6 +16,6 @@ Rtree
 Heap
 Unionfind
 Genarg
-Ephemeron
+CEphemeron
 Future
 RemoteCounter
diff --git a/lib/loc.ml b/lib/loc.ml
index afdab928..0f9864a9 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 f39cd267..c08e097a 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 00000000..f15021c6
--- /dev/null
+++ b/lib/minisys.ml
@@ -0,0 +1,66 @@
+(************************************************************************)
+(*  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 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/monad.ml b/lib/monad.ml
index a1714a41..2e55e969 100644
--- a/lib/monad.ml
+++ b/lib/monad.ml
@@ -64,6 +64,9 @@ module type ListS = sig
       its second argument in a tail position. *)
   val iter : ('a -> unit t) -> 'a list -> unit t
 
+  (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
+  val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
+
 
   (** {6 Two-list iterators} *)
 
@@ -138,6 +141,14 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct
       | a::b::l -> f a >> f b >> iter f l
 
 
+    let rec map_filter f = function
+      | [] -> return []
+      | a::l ->
+        f a >>= function
+        | None -> map_filter f l
+        | Some b ->
+          map_filter f l >>= fun filtered ->
+          return (b::filtered)
 
     let rec fold_left2 r f x l1 l2 =
       match l1,l2 with
diff --git a/lib/monad.mli b/lib/monad.mli
index c8655efa..f7de71f5 100644
--- a/lib/monad.mli
+++ b/lib/monad.mli
@@ -66,6 +66,9 @@ module type ListS = sig
       its second argument in a tail position. *)
   val iter : ('a -> unit t) -> 'a list -> unit t
 
+  (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
+  val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
+
 
   (** {6 Two-list iterators} *)
 
diff --git a/lib/option.ml b/lib/option.ml
index 4ea613e4..fbb883d3 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 409dff9d..5e085620 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 4f50e3e1..f3bb4753 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;
@@ -95,17 +77,6 @@ let print_emacs = ref false
    \end{description}
  *)
 
-let comments = ref []
-
-let rec split_com comacc acc pos = function
-    [] -> comments := List.rev acc; comacc
-  | ((b,e),c as com)::coms ->
-      (* Take all comments that terminates before pos, or begin exactly
-         at pos (used to print comments attached after an expression) *)
-      if e<=pos || pos=b then split_com (c::comacc) acc pos coms
-      else  split_com comacc (com::acc) pos coms
-
-
 type block_type =
   | Pp_hbox of int
   | Pp_vbox of int
@@ -129,7 +100,7 @@ type 'a ppcmd_token =
   | Ppcmd_open_box of block_type
   | Ppcmd_close_box
   | Ppcmd_close_tbox
-  | Ppcmd_comment of int
+  | Ppcmd_comment of string list
   | Ppcmd_open_tag of Tag.t
   | Ppcmd_close_tag
 
@@ -195,7 +166,7 @@ let tab () = Glue.atom(Ppcmd_set_tab)
 let fnl () = Glue.atom(Ppcmd_force_newline)
 let pifb () = Glue.atom(Ppcmd_print_if_broken)
 let ws n = Glue.atom(Ppcmd_white_space n)
-let comment n = Glue.atom(Ppcmd_comment n)
+let comment l = Glue.atom(Ppcmd_comment l)
 
 (* derived commands *)
 let mt () = Glue.empty
@@ -215,6 +186,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 *)
@@ -253,32 +243,15 @@ let qstring s = str "\"" ++ str (escape_string s) ++ str "\""
 let qs = qstring
 let quote s = h 0 (str "\"" ++ s ++ str "\"")
 
-(* This flag tells if the last printed comment ends with a newline, to
-  avoid empty lines *)
-let com_eol = ref false
-
-let com_brk ft = com_eol := false
-let com_if ft f =
-  if !com_eol then (com_eol := false; Format.pp_force_newline ft ())
-  else Lazy.force f
-
 let rec pr_com ft s =
   let (s1,os) =
     try
       let n = String.index s '\n' in
       String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1))
     with Not_found -> s,None in
-  com_if ft (Lazy.lazy_from_val());
-(*  let s1 =
-    if String.length s1 <> 0 && s1.[0] = ' ' then
-      (Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1))
-    else s1 in*)
   Format.pp_print_as ft (utf8_length s1) s1;
   match os with
-      Some s2 ->
-        if Int.equal (String.length s2) 0 then (com_eol := true)
-        else
-          (Format.pp_force_newline ft (); pr_com ft s2)
+      Some s2 -> Format.pp_force_newline ft (); pr_com ft s2
     | None -> ()
 
 type tag_handler = Tag.t -> Format.tag
@@ -297,34 +270,24 @@ 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
+          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
+          Format.pp_print_as ft n s
         end
     | Ppcmd_box(bty,ss)       -> (* Prevent evaluation of the stream! *)
-        com_if ft (Lazy.lazy_from_val());
         pp_open_box bty ;
         if not (Format.over_max_boxes ()) then 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      -> pp_open_box bty
     | Ppcmd_close_box         -> Format.pp_close_box ft ()
     | Ppcmd_close_tbox        -> Format.pp_close_tbox ft ()
-    | Ppcmd_white_space n     ->
-        com_if ft (Lazy.lazy_from_fun (fun()->Format.pp_print_break ft n 0))
-    | Ppcmd_print_break(m,n)  ->
-        com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_break ft m n))
+    | Ppcmd_white_space n     -> Format.pp_print_break ft n 0
+    | Ppcmd_print_break(m,n)  -> Format.pp_print_break ft m n
     | Ppcmd_set_tab           -> Format.pp_set_tab ft ()
-    | Ppcmd_print_tbreak(m,n) ->
-        com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_tbreak ft m n))
-    | Ppcmd_force_newline     ->
-        com_brk ft; Format.pp_force_newline ft ()
-    | Ppcmd_print_if_broken   ->
-        com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_if_newline ft ()))
-    | Ppcmd_comment i         ->
-        let coms = split_com [] [] i !comments in
-(*        Format.pp_open_hvbox ft 0;*)
-        List.iter (pr_com ft) coms(*;
-        Format.pp_close_box ft ()*)
+    | Ppcmd_print_tbreak(m,n) -> Format.pp_print_tbreak ft m n
+    | Ppcmd_force_newline     -> Format.pp_force_newline ft ()
+    | Ppcmd_print_if_broken   -> Format.pp_print_if_newline ft ()
+    | Ppcmd_comment coms      -> List.iter (pr_com ft) coms
     | Ppcmd_open_tag tag ->
       begin match pp_tag with
       | None -> ()
@@ -338,193 +301,41 @@ let pp_dirs ?pp_tag ft =
   in
   let pp_dir = function
     | Ppdir_ppcmds cmdstream -> Glue.iter pp_cmd cmdstream
-    | Ppdir_print_newline    ->
-        com_brk ft; Format.pp_print_newline ft ()
+    | Ppdir_print_newline    -> Format.pp_print_newline ft ()
     | Ppdir_print_flush      -> Format.pp_print_flush ft ()
   in
   fun (dirstream : _ ppdirs) ->
     try
-      Glue.iter pp_dir dirstream; com_brk ft
+      Glue.iter pp_dir dirstream
     with reraise ->
       let reraise = Backtrace.add_backtrace reraise in
       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
+let msg_with ?pp_tag ft strm =
+  pp_dirs ?pp_tag ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush))
 
 (* 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 ?pp_tag:None) 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 +418,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 2508779e..8342a983 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,33 +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 comments : ((int * int) * string) list ref
+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  : string list -> std_ppcmds
 
 (** {6 Manipulation commands} *)
 
@@ -100,87 +91,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 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. *)
-
-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 +113,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 +165,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 ?pp_tag fmt pp] Print [pp] to [fmt] and flush [fmt]  *)
+val msg_with : ?pp_tag:tag_handler -> 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 ?pp_tag 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 bb73fbdf..aa47c516 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
@@ -56,41 +56,6 @@ let default = Terminal.({
 
 let empty = Terminal.make ()
 
-let make_style_stack style_tags =
-  (** Not thread-safe. We should put a lock somewhere if we print from
-      different threads. Do we? *)
-  let style_stack = ref [] in
-  let peek () = match !style_stack with
-  | [] -> default (** Anomalous case, but for robustness *)
-  | st :: _ -> st
-  in
-  let push tag =
-    let style =
-      try
-        begin match String.Map.find tag style_tags with
-        | None -> empty
-        | Some st -> st
-        end
-      with Not_found -> empty
-    in
-    (** Use the merging of the latest tag and the one being currently pushed.
-    This may be useful if for instance the latest tag changes the background and
-    the current one the foreground, so that the two effects are additioned. *)
-    let style = Terminal.merge (peek ()) style in
-    let () = style_stack := style :: !style_stack in
-    Terminal.eval style
-  in
-  let pop _ = match !style_stack with
-  | [] ->
-    (** Something went wrong, we fallback *)
-    Terminal.eval default
-  | _ :: rem ->
-    let () = style_stack := rem in
-    Terminal.eval (peek ())
-  in
-  let clear () = style_stack := [] in
-  push, pop, clear
-
 let error_tag =
   let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in
   make ~style ["message"; "error"]
@@ -106,44 +71,3 @@ let debug_tag =
 let pp_tag t = match Pp.Tag.prj t tag with
 | None -> ""
 | Some key -> key
-
-let init_color_output () =
-  let push_tag, pop_tag, clear_tag = make_style_stack !tags in
-  let tag_handler = {
-    Format.mark_open_tag = push_tag;
-    Format.mark_close_tag = pop_tag;
-    Format.print_open_tag = ignore;
-    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
-  let pptag = tag in
-  let open Pp in
-  let msg ?header ft strm =
-    let strm = match header with
-    | None -> hov 0 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
-  in
-  let () = set_logger logger in
-  ()
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
index 97b5869f..d9fd7576 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
@@ -43,15 +44,7 @@ val parse_config : string -> unit
 val dump : unit -> (t * Terminal.style option) list
 (** Recover the list of known tags together with their current style. *)
 
-(** {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! *)
+(** {5 Color output} *)
 
 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 2350cd43..d620fe69 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -146,9 +146,9 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
    number of allocated bytes may exceed the maximum integer capacity
    (2^31 on 32-bits architectures);  therefore, allocation is measured
    by small steps, total allocations are computed by adding elementary
-   measures and carries are controled from step to step *)
+   measures and carries are controlled from step to step *)
 
-(* Unix measure of time is approximative and shoitt delays are often
+(* Unix measure of time is approximate and short delays are often
    unperceivable; therefore, total times are measured in one (big)
    step to avoid rounding errors and to get the best possible
    approximation.
@@ -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
@@ -358,7 +358,7 @@ let declare_profile name =
   prof_table := (name,e)::!prof_table;
   e
 
-(* Default initialisation, may be overriden *)
+(* Default initialization, may be overridden *)
 let _ = init_profile ()
 
 (******************************)
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index 3f198259..e7646fb7 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -20,19 +20,21 @@ let new_counter ~name a ~incr ~build =
   let data = ref (ref a) in
   counters := (name, Obj.repr data) :: !counters;
   let m = Mutex.create () in
-  let mk_thsafe_getter f () =
+  let mk_thsafe_local_getter f () =
     (* - slaves must use a remote counter getter, not this one! *)
     (* - 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 getter = ref(mk_thsafe_getter (fun () -> !data := incr !!data; !!data)) in
+  let mk_thsafe_remote_getter f () =
+    Mutex.lock m; let x = f () in Mutex.unlock m; x in
+  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");
-    getter := f in
+      CErrors.anomaly(Pp.str"Only slave processes can install a remote counter");
+    getter := mk_thsafe_remote_getter f in
   (fun () -> !getter ()), installer
 
 let backup () = !counters
diff --git a/lib/richpp.ml b/lib/richpp.ml
index 453df43d..a98273ed 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 05c16621..287d265a 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 79a79dd4..00000000
--- 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 2a8e5316..00000000
--- 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 4d35ded9..47917697 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
@@ -220,10 +206,13 @@ let stats { oob_req; oob_resp; alive } =
   input_value oob_resp
 
 let rec wait p =
-  try snd (Unix.waitpid [] p.pid)
-  with
-  | Unix.Unix_error (Unix.EINTR, _, _) -> wait p
-  | Unix.Unix_error _ -> Unix.WEXITED 0o400
+  (* On windows kill is not reliable, so wait may never return. *) 
+  if Sys.os_type = "Unix" then 
+    try snd (Unix.waitpid [] p.pid)
+    with
+    | Unix.Unix_error (Unix.EINTR, _, _) -> wait p
+    | Unix.Unix_error _ -> Unix.WEXITED 0o400
+  else Unix.WEXITED 0o400
 
 end
 
@@ -267,8 +256,13 @@ let stats { oob_req; oob_resp; alive } =
   flush oob_req;
   let RespStats g = input_value oob_resp in g
 
-let wait { pid = unixpid } =
-  try snd (Unix.waitpid [] unixpid)
-  with Unix.Unix_error _ -> Unix.WEXITED 0o400
+let rec wait p =
+  (* On windows kill is not reliable, so wait may never return. *) 
+  if Sys.os_type = "Unix" then 
+    try snd (Unix.waitpid [] p.pid)
+    with
+    | Unix.Unix_error (Unix.EINTR, _, _) -> wait p
+    | Unix.Unix_error _ -> Unix.WEXITED 0o400
+  else Unix.WEXITED 0o400
 
 end
diff --git a/lib/stateid.ml b/lib/stateid.ml
index 59cf206e..ae25735c 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,29 +13,29 @@ 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 =
+let add exn ~valid id =
   Exninfo.add exn state_id_info (valid, id)
 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 2c12c30c..1d87a343 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -6,32 +6,28 @@
 (*         *       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.
- * Backtracking to the valid id is safe.
- * The initial_state_id is assumed to be safe. *)
-val add : Exninfo.info -> ?valid:t -> t -> Exninfo.info
+ * Backtracking to the valid id is safe. *)
+val add : Exninfo.info -> valid:t -> t -> Exninfo.info
 val get : Exninfo.info -> (t * t) option
 
 type ('a,'b) request = {
diff --git a/lib/system.ml b/lib/system.ml
index 9bdcecef..4b99de70 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -9,38 +9,32 @@
 (* $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 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 Sys.is_directory file then begin
-          let newrel = rel @ [f] in
-	  add file newrel;
-	  traverse file newrel
-        end)
-      (Sys.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 [];
+  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
@@ -58,23 +52,25 @@ let dirmap = ref StrMap.empty
 
 let make_dir_table dir =
   let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
-  Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir 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
@@ -84,26 +80,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)
@@ -132,7 +131,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
@@ -140,7 +139,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"))
 
@@ -148,25 +147,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 =
-  let path = try Sys.getenv "PATH"
-             with Not_found -> error "system variable PATH not found" in
-  let lpath = CUnix.path_to_list path in
-  is_in_path lpath filename
+  try
+    let lpath = CUnix.path_to_list (Sys.getenv "PATH") in
+    is_in_path lpath filename
+  with 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
@@ -210,7 +218,8 @@ let skip_in_segment f ch =
   seek_in ch stop;
   stop, digest_in f ch
 
-exception Bad_magic_number of string
+type magic_number_error = {filename: string; actual: int; expected: int}
+exception Bad_magic_number of magic_number_error
 
 let raw_extern_state magic filename =
   let channel = open_trapping_failure filename in
@@ -220,8 +229,12 @@ let raw_extern_state magic filename =
 let raw_intern_state magic filename =
   try
     let channel = open_in_bin filename in
-    if not (Int.equal (input_binary_int filename channel) magic) then
-      raise (Bad_magic_number filename);
+    let actual_magic = input_binary_int filename channel in
+    if not (Int.equal actual_magic magic) then
+        raise (Bad_magic_number {
+            filename=filename;
+            actual=actual_magic;
+            expected=magic});
     channel
   with
   | End_of_file -> error_corrupted filename "premature end of file"
@@ -234,11 +247,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
@@ -247,13 +260,15 @@ 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 fname ->
-    errorlabstrm "with_magic_number_check"
-    (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++
+  with Bad_magic_number {filename=fname;actual=actual;expected=expected} ->
+    CErrors.errorlabstrm "with_magic_number_check"
+    (str"File " ++ str fname ++ strbrk" has bad magic number " ++
+    int actual ++ str" (expected " ++ int expected ++ str")." ++
+    spc () ++
     strbrk "It is corrupted or was compiled with another version of Coq.")
 
 (* Time stamps. *)
@@ -284,13 +299,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 062c8ea8..21436909 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -8,14 +8,41 @@
 
 (** {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
+
+(** [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 +51,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
 
@@ -34,9 +59,11 @@ val file_exists_respecting_case : string -> string -> bool
 (** {6 I/O functions } *)
 (** Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
-  when the check fails, with the full file name. *)
+  when the check fails, with the full file name and expected/observed magic
+  numbers. *)
 
-exception Bad_magic_number of string
+type magic_number_error = {filename: string; actual: int; expected: int}
+exception Bad_magic_number of magic_number_error
 
 val raw_extern_state : int -> string -> out_channel
 
diff --git a/lib/unicode.ml b/lib/unicode.ml
index 1765e93d..ced5e258 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -8,9 +8,7 @@
 
 (** Unicode utilities *)
 
-type status = Letter | IdentPart | Symbol
-
-exception Unsupported
+type status = Letter | IdentPart | Symbol | Unknown
 
 (* The following table stores classes of Unicode characters that
    are used by the lexer. There are 3 different classes so 2 bits are
@@ -18,7 +16,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].
@@ -29,6 +27,7 @@ let mask i = function
   | Letter    -> 1 lsl ((i land 7) lsl 1) (* 01 *)
   | IdentPart -> 2 lsl ((i land 7) lsl 1) (* 10 *)
   | Symbol    -> 3 lsl ((i land 7) lsl 1) (* 11 *)
+  | Unknown   -> 0 lsl ((i land 7) lsl 1) (* 00 *)
 
 (* Helper to reset 2 bits in a word. *)
 let reset_mask i =
@@ -55,7 +54,7 @@ let lookup x =
     if      v = 1 then Letter
     else if v = 2 then IdentPart
     else if v = 3 then Symbol
-    else raise Unsupported
+    else Unknown
 
 (* [classify] discriminates between 3 different kinds of
    symbols based on the standard unicode classification (extracted from
@@ -147,6 +146,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
@@ -168,6 +172,13 @@ let next_utf8 s i =
        (c land 0x3F) lsl 6 + (d land 0x3F)
   else err ()
 
+let is_utf8 s =
+  let rec check i =
+    let (off, _) = next_utf8 s i in
+    check (i + off)
+  in
+  try check 0 with End_of_input -> true | Invalid_argument _ -> false
+
 (* Check the well-formedness of an identifier *)
 
 let initial_refutation j n s =
@@ -203,7 +214,6 @@ let ident_refutation s =
         |x -> x
   with
   | End_of_input -> Some (true,"The empty string is not an identifier.")
-  | Unsupported -> Some (true,s^": unsupported character in utf8 sequence.")
   | Invalid_argument _ -> Some (true,s^": invalid utf8 sequence.")
 
 let lowercase_unicode =
@@ -228,14 +238,94 @@ let is_basic_ascii s =
   !ok
 
 let ascii_of_ident s =
-  if is_basic_ascii s then s else
-    let i = ref 0 and out = ref "" in
-    begin try while true do
+  let len = String.length s in
+  let has_UU i =
+    i+2 < len && s.[i]='_' && s.[i+1]='U' && s.[i+2]='U'
+  in
+  let i = ref 0 in
+  while !i < len && Char.code s.[!i] < 128 && not (has_UU !i) do
+    incr i
+  done;
+  if !i = len then s else
+    let out = Buffer.create (2*len) in
+    Buffer.add_substring out s 0 !i;
+    while !i < len do
       let j, n = next_utf8 s !i in
-      out :=
-        if n >= 128
-        then Printf.sprintf "%s__U%04x_" !out n
-        else Printf.sprintf "%s%c" !out s.[!i];
-      i := !i + j
-    done with End_of_input -> () end;
-    !out
+      if n >= 128 then
+        (Printf.bprintf out "_UU%04x_" n; i := !i + j)
+      else if has_UU !i then
+        (Buffer.add_string out "_UUU"; i := !i + 3)
+      else
+        (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 520203d4..2609e196 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -8,21 +8,35 @@
 
 (** Unicode utilities *)
 
-type status = Letter | IdentPart | Symbol
+type status = Letter | IdentPart | Symbol | Unknown
 
-exception Unsupported
-
-(** Classify a unicode char into 3 classes, or raise [Unsupported] *)
+(** Classify a unicode char into 3 classes or unknown. *)
 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. *)
 val ident_refutation : string -> (bool * string) option
 
-(** First char of a string, converted to lowercase *)
+(** First char of a string, converted to lowercase
+    @raise Assert_failure if the input string is empty. *)
 val lowercase_first_char : string -> string
 
-(** For extraction, turn a unicode string into an ascii-only one *)
+(** Return [true] if all UTF-8 characters in the input string are just plain
+    ASCII characters. Returns [false] otherwise. *)
 val is_basic_ascii : string -> bool
+
+(** [ascii_of_ident s] maps UTF-8 string to a string composed solely from ASCII
+    characters. The non-ASCII characters are translated to ["_UUxxxx_"] where
+    {i xxxx} is the Unicode index of the character in hexadecimal (from four
+    to six hex digits). To avoid potential name clashes, any preexisting
+    substring ["_UU"] is turned into ["_UUU"]. *)
 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 a20dba0f..009dfbe1 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 4156af67..6bed7e35 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 e61cb055..00000000
--- 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 290f2c89..00000000
--- 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 8db3f9e8..00000000
--- 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 ac2eab35..00000000
--- 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 e7e4d0ce..00000000
--- 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 f24f51ff..00000000
--- 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