37 files changed, 544 insertions, 251 deletions

diff --git a/lib/cList.ml b/lib/cList.ml
index 0ac372d8d8..bd3e09b5b2 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -48,6 +48,7 @@ sig
   val filteri :
     (int -> 'a -> bool) -> 'a list -> 'a list
   val smartfilter : ('a -> bool) -> '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
@@ -375,6 +376,12 @@ let rec smartfilter f l = match l with
           else h :: tl'
         else tl'
 
+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)
@@ -638,12 +645,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 19eeb2509a..1487f67a37 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -94,6 +94,8 @@ sig
   (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
     [f ai = true], then [smartfilter f l == 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). *)
 
diff --git a/lib/cMap.ml b/lib/cMap.ml
index cf590d96c3..876f847365 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -12,6 +12,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 =
@@ -30,6 +37,12 @@ sig
   sig
     val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
   end
+  module Monad(M : MonadS) :
+  sig
+    val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+    val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+    val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+  end
 end
 
 module MapExt (M : Map.OrderedType) :
@@ -47,6 +60,12 @@ sig
   sig
     val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map
   end
+  module Monad(MS : MonadS) :
+  sig
+    val fold : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t
+    val fold_left : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t
+    val fold_right : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t
+  end
 end =
 struct
   (** This unsafe module is a way to access to the actual implementations of
@@ -159,6 +178,29 @@ 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) =
diff --git a/lib/cMap.mli b/lib/cMap.mli
index 23d3801e08..cd3d2f5b19 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 =
@@ -59,6 +66,14 @@ sig
         i.e.: for all (k : key) (x : 'a), compare (fst (f k x)) k = 0. *)
   end
 
+  module Monad(M : MonadS) :
+  sig
+    val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+    val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+    val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+  end
+  (** Fold operators parameterized by any monad. *)
+
 end
 
 module Make(M : Map.OrderedType) : ExtS with
diff --git a/lib/cSig.mli b/lib/cSig.mli
index 2a8bda2936..796e58cbfb 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
@@ -45,3 +47,5 @@ sig
 end
 (** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml
     documentation for more information. *)
+
+module type EmptyS = sig end
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 7ff1d29359..1770df1993 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -8,6 +8,7 @@ Hashcons
 CSet
 CMap
 Int
+Dyn
 HMap
 Option
 Store
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 056b687313..826cfaf8db 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -6,12 +6,24 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Pp
-
+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
+val dump : unit -> (int * string) list
+end
+
+module Make(M : CSig.EmptyS) =
+struct
 (* Dynamics, programmed with DANGER !!! *)
 
-type t = int * Obj.t
+type 'a tag = int
+
+type t = Dyn : 'a tag * 'a -> t
 
 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 +36,21 @@ 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 pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2
+    let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in
+    assert false
 
 let dump () = Int.Map.bindings !dyntab
+
+end
\ No newline at end of file
diff --git a/lib/dyn.mli b/lib/dyn.mli
index cac912aca1..28587859e1 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -8,10 +8,16 @@
 
 (** Dynamics. Use with extreme care. Not for kids. *)
 
-type t
+module type S =
+sig
+type 'a tag
+type t = Dyn : 'a tag * 'a -> t
 
-val create : string -> ('a -> t) * (t -> 'a)
-val tag : t -> string
-val has_tag : t -> string -> bool
-val pointer_equal : t -> t -> bool
+val create : string -> 'a tag
+val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+val repr : 'a tag -> string
 val dump : unit -> (int * string) list
+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 2b8af917fa..512114d5dc 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 b62b9f28a9..7c20c035a5 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/feedback.ml b/lib/feedback.ml
index a5e16ea04c..1726da2fdb 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -18,7 +18,7 @@ type message_level =
 
 type message = {
   message_level : message_level;
-  message_content : string;
+  message_content : xml;
 }
 
 let of_message_level = function
@@ -39,12 +39,12 @@ let to_message_level =
 
 let of_message msg =
   let lvl = of_message_level msg.message_level in
-  let content = Serialize.of_string msg.message_content in
+  let content = Serialize.of_xml 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 }
+      message_content = Serialize.to_xml content }
   | _ -> raise Serialize.Marshal_error
 
 let is_message = function
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 52a0e9fe6f..38c867f5b5 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -18,7 +18,7 @@ type message_level =
 
 type message = {
   message_level : message_level;
-  message_content : string;
+  message_content : xml;
 }
 
 val of_message : message -> xml
diff --git a/lib/flags.ml b/lib/flags.ml
index ab4ac03f80..96415ed263 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -101,18 +101,20 @@ let we_are_parsing = ref false
 (* Current means no particular compatibility consideration.
    For correct comparisons, this constructor should remain the last one. *)
 
-type compat_version = V8_2 | V8_3 | V8_4 | Current
+type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current
 
 let compat_version = ref Current
 
 let version_strictly_greater v = match !compat_version, v with
-| V8_2, (V8_2 | V8_3 | V8_4 | Current) -> false
-| V8_3, (V8_3 | V8_4 | Current) -> false
-| V8_4, (V8_4 | Current) -> false
+| V8_2, (V8_2 | V8_3 | V8_4 | V8_5 | Current) -> false
+| V8_3, (V8_3 | V8_4 | V8_5 | Current) -> false
+| V8_4, (V8_4 | V8_5 | Current) -> false
+| V8_5, (V8_5 | Current) -> false
 | Current, Current -> false
 | V8_3, V8_2 -> true
 | V8_4, (V8_2 | V8_3) -> true
-| Current, (V8_2 | V8_3 | V8_4) -> true
+| V8_5, (V8_2 | V8_3 | V8_4) -> true
+| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> true
 
 let version_less_or_equal v = not (version_strictly_greater v)
 
@@ -120,6 +122,7 @@ let pr_version = function
   | V8_2 -> "8.2"
   | V8_3 -> "8.3"
   | V8_4 -> "8.4"
+  | V8_5 -> "8.5"
   | Current -> "current"
 
 (* Translate *)
@@ -193,9 +196,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
diff --git a/lib/flags.mli b/lib/flags.mli
index 8e37136560..cb92e1462d 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -55,7 +55,7 @@ val raw_print : bool ref
 val record_print : bool ref
 val univ_print : bool ref
 
-type compat_version = V8_2 | V8_3 | V8_4 | Current
+type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current
 val compat_version : compat_version ref
 val version_strictly_greater : compat_version -> bool
 val version_less_or_equal : compat_version -> bool
@@ -120,8 +120,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
 
diff --git a/lib/future.ml b/lib/future.ml
index 78a158264b..b6012ed207 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 ->
@@ -58,7 +59,7 @@ type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computat
 and 'a comp =
   | Delegated of (unit -> unit)
   | Closure of (unit -> 'a)
-  | Val of 'a * Dyn.t option
+  | Val of 'a * freeze option
   | Exn of Exninfo.iexn  (* Invariant: this exception is always "fixed" as in fix_exn *)
 
 and 'a comput =
diff --git a/lib/future.mli b/lib/future.mli
index adc15e49c7..29b71b70a8 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 42458ecb31..6108c15555 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -9,37 +9,67 @@
 open Pp
 open Util
 
+module Dyn = Dyn.Make(struct end)
+
+module Val =
+struct
+
+  type 'a typ = 'a Dyn.tag
+
+  type _ tag =
+  | Base : 'a typ -> 'a tag
+  | List : 'a tag -> 'a list tag
+  | Opt : 'a tag -> 'a option tag
+  | Pair : 'a tag * 'b tag -> ('a * 'b) tag
+
+  type t = Dyn : 'a tag * 'a -> t
+
+  let rec eq : type a b. a tag -> b tag -> (a, b) CSig.eq option =
+  fun t1 t2 -> match t1, t2 with
+  | Base t1, Base t2 -> Dyn.eq t1 t2
+  | List t1, List t2 ->
+    begin match eq t1 t2 with
+    | None -> None
+    | Some Refl -> Some Refl
+    end
+  | Opt t1, Opt t2 ->
+    begin match eq t1 t2 with
+    | None -> None
+    | Some Refl -> Some Refl
+    end
+  | Pair (t1, u1), Pair (t2, u2) ->
+    begin match eq t1 t2 with
+    | None -> None
+    | Some Refl ->
+      match eq u1 u2 with
+      | None -> None
+      | Some Refl -> Some Refl
+    end
+  | _ -> None
+
+  let rec repr : type a. a tag -> std_ppcmds = function
+  | Base t -> str (Dyn.repr t)
+  | List t -> repr t ++ spc () ++ str "list"
+  | Opt t -> repr t ++ spc () ++ str "option"
+  | Pair (t1, t2) -> str "(" ++ repr t1 ++ str " * " ++ repr t2 ++ str ")"
+
+end
+
 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) ->
@@ -48,17 +78,9 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
 | _ -> 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) ->
@@ -145,13 +167,22 @@ let pair_unpack pack (t, obj) = match t with
 
 (** Creating args *)
 
-let (arg0_map : Obj.t option String.Map.t ref) = ref String.Map.empty
+type load = {
+  nil : Obj.t option;
+  dyn : Obj.t Val.tag;
+}
+
+let (arg0_map : load String.Map.t ref) = ref String.Map.empty
+
+let cast_tag : 'a Val.tag -> 'b Val.tag = Obj.magic
 
-let create_arg opt name =
+let create_arg opt ?dyn 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
+    let dyn = match dyn with None -> Val.Base (Dyn.create name) | Some dyn -> cast_tag dyn in
+    let obj = { nil = Option.map Obj.repr opt; dyn; } in
+    let () = arg0_map := String.Map.add name obj !arg0_map in
     ExtraArgType name
 
 let make0 = create_arg
@@ -165,12 +196,73 @@ let default_empty_value t =
       | Some v1, Some v2 -> Some (Obj.repr (v1, v2))
       | _ -> None)
   | ExtraArgType s ->
-    String.Map.find s !arg0_map
+    (String.Map.find s !arg0_map).nil
   | _ -> None in
   match aux t with
   | Some v -> Some (Obj.obj v)
   | None -> None
 
+(** Beware: keep in sync with the corresponding types *)
+let base_create n = Val.Base (Dyn.create n)
+let ident_T = base_create "ident"
+let genarg_T = base_create "genarg"
+let constr_T = base_create "constr"
+
+let rec val_tag = function
+| IdentArgType -> cast_tag ident_T
+| VarArgType -> cast_tag ident_T
+  (** Must ensure that toplevel types of Var and Ident agree! *)
+| ConstrArgType -> cast_tag constr_T
+| ExtraArgType s -> cast_tag (String.Map.find s !arg0_map).dyn
+| ListArgType t -> cast_tag (Val.List (val_tag t))
+| OptArgType t -> cast_tag (Val.Opt (val_tag t))
+| PairArgType (t1, t2) -> cast_tag (Val.Pair (val_tag t1, val_tag t2))
+
+exception CastError of argument_type * Val.t
+
+let prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
+  let Val.Dyn (t', x) = v in
+  match Val.eq t t' with
+  | None -> None
+  | Some Refl -> Some x
+
+let try_prj wit v = match prj (val_tag wit) v with
+| None -> raise (CastError (wit, v))
+| Some x -> x
+
+let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a =
+fun wit v -> match unquote wit with
+| IdentArgType
+| VarArgType
+| ConstrArgType
+| ExtraArgType _ -> try_prj wit v
+| ListArgType t ->
+  let Val.Dyn (tag, v) = v in
+  begin match tag with
+  | Val.List tag ->
+    let map x = val_cast t (Val.Dyn (tag, x)) in
+    Obj.magic (List.map map v)
+  | _ ->  raise (CastError (wit, Val.Dyn (tag, v)))
+  end
+| OptArgType t ->
+  let Val.Dyn (tag, v) = v in
+  begin match tag with
+  | Val.Opt tag ->
+    let map x = val_cast t (Val.Dyn (tag, x)) in
+    Obj.magic (Option.map map v)
+  | _ ->  raise (CastError (wit, Val.Dyn (tag, v)))
+  end
+| PairArgType (t1, t2) ->
+  let Val.Dyn (tag, v) = v in
+  begin match tag with
+  | Val.Pair (tag1, tag2) ->
+    let (v1, v2) = v in
+    let v1 = Val.Dyn (tag1, v1) in
+    let v2 = Val.Dyn (tag2, v2) in
+    Obj.magic (val_cast t1 v1, val_cast t2 v2)
+  | _ ->  raise (CastError (wit, Val.Dyn (tag, v)))
+  end
+
 (** Registering genarg-manipulating functions *)
 
 module type GenObj =
@@ -225,11 +317,3 @@ let register_name0 t name = match t with
 
 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 a269f92774..674ee97ae8 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -72,14 +72,35 @@ 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 Val :
+sig
+  type 'a typ
+
+  type _ tag =
+  | Base : 'a typ -> 'a tag
+  | List : 'a tag -> 'a list tag
+  | Opt : 'a tag -> 'a option tag
+  | Pair : 'a tag * 'b tag -> ('a * 'b) tag
+
+  type t = Dyn : 'a tag * 'a -> t
+
+  val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+  val repr: 'a tag -> Pp.std_ppcmds
+
+end
+(** Dynamic types for toplevel values. While the generic types permit to relate
+    objects at various levels of interpretation, toplevel values are wearing
+    their own type regardless of where they came from. This allows to use the
+    same runtime representation for several generic types. *)
+
 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 : 'raw option -> ?dyn:'top Val.tag -> 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 : 'raw option -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
 (** Alias for [make0]. *)
 
 (** {5 Specialized types} *)
@@ -179,27 +200,30 @@ type ('r, 'l) pair_unpacker =
 
 val pair_unpack : ('r, 'l) pair_unpacker -> 'l generic_argument -> 'r
 
+(** {6 Dynamic toplevel values} *)
+
+val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag
+(** Retrieve the dynamic type associated to a toplevel genarg. Only works for
+    ground generic arguments. *)
+
+val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a
+
 (** {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
 
+exception CastError of argument_type * Val.t
+(** Exception raised by {!val_cast} *)
+
 val argument_type_eq : argument_type -> argument_type -> bool
 
 val pr_argument_type : argument_type -> Pp.std_ppcmds
@@ -256,23 +280,3 @@ val register_name0 : ('a, 'b, 'c) genarg_type -> string -> unit
 
 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 f902eded03..b5fc523150 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -329,4 +329,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 46ba0b6285..eeaaf2f7fc 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -72,7 +72,7 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) =
 
   end
 
-(* A few usefull wrappers:
+(* A few useful wrappers:
  * takes as argument the function [generate] above and build a function of type
  * u -> t -> t that creates a fresh table each time it is applied to the
  * sub-hcons functions. *)
@@ -96,20 +96,6 @@ let recursive_hcons h f u =
   let () = loop := hrec in
   hrec
 
-(* A set of global hashcons functions *)
-let hashcons_resets = ref []
-let init() = List.iter (fun f -> f()) !hashcons_resets
-
-(* [register_hcons h u] registers the hcons function h, result of the above
- *   wrappers. It returns another hcons function that always uses the same
- *   table, which can be reinitialized by init()
- *)
-let register_hcons h u =
-  let hf = ref (h u) in
-  let reset() = hf := h u in
-  hashcons_resets := reset :: !hashcons_resets;
-  (fun x -> !hf x)
-
 (* Basic hashcons modules for string and obj. Integers do not need be
    hashconsed.  *)
 
@@ -194,18 +180,3 @@ module Hobj = Make(
     let equal = comp_obj
     let hash = Hashtbl.hash
   end)
-
-(* Hashconsing functions for string and obj. Always use the same
- * global tables. The latter can be reinitialized with init()
- *)
-(* string : string -> string *)
-(* obj : Obj.t -> Obj.t *)
-let string = register_hcons (simple_hcons Hstring.generate Hstring.hcons) ()
-let obj = register_hcons (recursive_hcons Hobj.generate Hobj.hcons) ()
-
-(* The unsafe polymorphic hashconsing function *)
-let magic_hash (c : 'a) =
-  init();
-  let r = obj (Obj.repr c) in
-  init();
-  (Obj.magic r : 'a)
diff --git a/lib/hashset.ml b/lib/hashset.ml
index 1ca6cc6418..0009ac6506 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -162,7 +162,7 @@ module Make (E : EqType) =
         t.hashes.(index) <- newhashes;
         if sz <= t.limit && newsz > t.limit then begin
           t.oversize <- t.oversize + 1;
-          for i = 0 to over_limit do test_shrink_bucket t done;
+          for _i = 0 to over_limit do test_shrink_bucket t done;
         end;
         if t.oversize > Array.length t.table / over_limit then resize t
       end else if Weak.check bucket i then begin
diff --git a/lib/heap.ml b/lib/heap.ml
index a19bc0d1c3..5682b87bb6 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/lib.mllib b/lib/lib.mllib
index f3f6ad8fc7..a9181c51c1 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,6 +1,5 @@
 Errors
 Bigint
-Dyn
 Segmenttree
 Unicodetable
 Unicode
diff --git a/lib/option.ml b/lib/option.ml
index 9ea1a76982..2f6e8365bb 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 d9ad0e119f..4a8114177f 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 4ed4b17791..a1913c98f7 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -51,25 +51,18 @@ 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 x k = Dyn.Dyn (k, x)
+let prj : type a. t -> a key -> a option = fun dyn k ->
+  let Dyn.Dyn (k', x) = dyn in
+  match Dyn.eq k k' with
+  | None -> None
+  | Some CSig.Refl -> Some x
 
 end
 
@@ -412,7 +405,7 @@ type message_level =  Feedback.message_level =
 
 type message = Feedback.message = {
   message_level : message_level;
-  message_content : string;
+  message_content : Xml_datatype.xml;
 }
 
 let of_message = Feedback.of_message
@@ -511,11 +504,11 @@ let string_of_ppcmds c =
   msg_with Format.str_formatter c;
   Format.flush_str_formatter ()
 
-let log_via_feedback () = logger := (fun ~id lvl msg ->
+let log_via_feedback printer = logger := (fun ~id lvl msg ->
   !feeder {
      Feedback.contents = Feedback.Message {
        message_level = lvl;
-       message_content = string_of_ppcmds msg };
+       message_content = printer msg };
      Feedback.route = !feedback_route;
      Feedback.id = id })
 
diff --git a/lib/pp.mli b/lib/pp.mli
index 3b1123a9dc..d034e67617 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -116,7 +116,7 @@ type message_level = Feedback.message_level =
 
 type message = Feedback.message = {
   message_level : message_level;
-  message_content : string;
+  message_content : Xml_datatype.xml;
 }
 
 type logger = message_level -> std_ppcmds -> unit
@@ -154,7 +154,7 @@ val std_logger : logger
 
 val set_logger : logger -> unit
 
-val log_via_feedback : unit -> unit
+val log_via_feedback : (std_ppcmds -> Xml_datatype.xml) -> unit
 
 val of_message : message -> Xml_datatype.xml
 val to_message : Xml_datatype.xml -> message
diff --git a/lib/richpp.ml b/lib/richpp.ml
index c4a9c39d5a..fff989ce0a 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -163,4 +163,38 @@ 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
+
+let of_richpp x = Element ("richpp", [], [x])
+let to_richpp xml = match xml with
+| Element ("richpp", [], [x]) -> x
+| _ -> raise Serialize.Marshal_error
diff --git a/lib/richpp.mli b/lib/richpp.mli
index a0d3c374b2..7e4b58c9a6 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -39,3 +39,29 @@ 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 Serialization} *)
+
+val of_richpp : richpp -> Xml_datatype.xml
+val to_richpp : Xml_datatype.xml -> richpp
+
+(** 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
index aa2e3f02a4..b14bfb2833 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -114,3 +114,7 @@ let to_loc xml =
       with Not_found | Invalid_argument _ -> raise Marshal_error)
   | _ -> raise Marshal_error
 
+let of_xml x = Element ("xml", [], [x])
+let to_xml xml = match xml with
+| Element ("xml", [], [x]) -> x
+| _ -> raise Marshal_error
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 34d3e054cd..f4eac5a6b9 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -35,3 +35,5 @@ val of_edit_id: int -> xml
 val to_edit_id: xml -> int
 val of_loc : Loc.t -> xml
 val to_loc : xml -> Loc.t
+val of_xml : xml -> xml
+val to_xml : xml -> xml
diff --git a/lib/system.ml b/lib/system.ml
index a902229609..31e9861d3a 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -12,35 +12,83 @@ open Pp
 open Errors
 open Util
 
-(* All subdirectories, recursively *)
+(** Dealing with directories *)
 
-let exists_dir dir =
-  try Sys.is_directory dir with Sys_error _ -> false
+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_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
+let exclude_directory 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)
+  not (f = "") && f.[0] != '.' &&
+  not (List.mem f !skipped_dirnames) (*&&
+  (match Unicode.ident_refutation f with None -> true | _ -> false)*)
+
+(* Check directory can be opened *)
+
+let exists_dir dir =
+  try Sys.is_directory dir with Sys_error _ -> false
+
+let check_unix_dir warn dir =
+  if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
+    (String.length dir > 2 && dir.[1] = ':' ||
+     String.contains dir '\\' ||
+     String.contains dir ';')
+  then warn ("assuming " ^ dir ^
+             " to be a Unix path even if looking like a Win32 path.")
+
+let apply_subdir f path name =
+  (* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
+  (* as well as skipped files like CVS, ... *)
+  if ok_dirname name then
+    let path = if path = "." then name else path//name in
+    match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with
+    | Unix.S_DIR -> f (FileDir (path,name))
+    | Unix.S_REG -> f (FileRegular name)
+    | _ -> ()
+
+let process_directory f path =
+  Array.iter (apply_subdir f path) (Sys.readdir path)
+
+let process_subdirectories f path =
+  let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
+  process_directory f path
+
+(** 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 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 [];
+  check_unix_dir (fun s -> msg_warning (str s)) root;
+  if exists_dir root then traverse root []
+  else msg_warning (str ("Cannot open " ^ root));
   List.rev !l
 
 (* Caching directory contents for efficient syntactic equality of file
@@ -61,20 +109,22 @@ let make_dir_table dir =
   Array.fold_left filter_dotfiles StrSet.empty (Sys.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,7 +134,7 @@ 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
diff --git a/lib/system.mli b/lib/system.mli
index c2d64fe0d0..7a91e005c6 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -8,14 +8,46 @@
 
 (** {5 Coqtop specific system utilities} *)
 
+(** {6 Directories} *)
+
+type unix_path = string (* path in unix-style, with '/' separator *)
+
+type file_kind =
+  | FileDir of unix_path * (* basename of path: *) string
+  | FileRegular of string (* basename of file *)
+
+val (//) : unix_path -> string -> unix_path
+
+val exists_dir : unix_path -> bool
+
+(** [check_unix_dir warn path] calls [warn] with an appropriate
+     message if [path] looks does not look like a Unix path on Windows *)
+
+val check_unix_dir : (string -> unit) -> unix_path -> unit
+
+(** [exclude_search_in_dirname path] excludes [path] when processing
+    directories *)
+
+val exclude_directory : unix_path -> unit
+
+(** [process_directory f path] applies [f] on contents of directory
+    [path]; fails with Unix_error if the latter does not exists; skips
+    all files or dirs starting with "." *)
+
+val process_directory : (file_kind -> unit) -> unix_path -> unit
+
+(** [process_subdirectories f path] applies [f path/file file] on each
+    [file] of the directory [path]; fails with Unix_error if the
+    latter does not exists; kips all files or dirs starting with "." *)
+
+val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit
+
 (** {6 Files and load paths} *)
 
 (** Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
     [directory]), the root path and the path relative to the root. *)
 
-val exclude_search_in_dirname : string -> unit
-
 val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list
 val is_in_path : CUnix.load_path -> string -> bool
 val is_in_system_path : string -> bool
@@ -24,8 +56,6 @@ val where_in_path :
 val where_in_path_rex :
   CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list
 
-val exists_dir : string -> bool
-
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
 
diff --git a/lib/unicode.ml b/lib/unicode.ml
index 1765e93dcd..05998bb804 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -18,7 +18,7 @@ exception Unsupported
    to simplify the masking process. (This choice seems to be a good
    trade-off between speed and space after some benchmarks.) *)
 
-(* A 256ko table, initially filled with zeros. *)
+(* A 256 KiB table, initially filled with zeros. *)
 let table = Array.make (1 lsl 17) 0
 
 (* Associate a 2-bit pattern to each status at position [i].
@@ -147,6 +147,11 @@ let utf8_of_unicode n =
       s
     end
 
+(* If [s] is some UTF-8 encoded string
+   and [i] is a position of some UTF-8 character within [s]
+   then [next_utf8 s i] returns [(j,n)] where:
+   - [j] indicates the position of the next UTF-8 character
+   - [n] represents the UTF-8 character at index [i] *)
 let next_utf8 s i =
   let err () = invalid_arg "utf8" in
   let l = String.length s - i in
diff --git a/lib/unicode.mli b/lib/unicode.mli
index 098f6c919d..eb75f00c28 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -10,19 +10,29 @@
 
 type status = Letter | IdentPart | Symbol
 
+(** This exception is raised when UTF-8 the input string contains unsupported UTF-8 characters. *)
 exception Unsupported
 
-(** Classify a unicode char into 3 classes, or raise [Unsupported] *)
+(** Classify a unicode char into 3 classes.
+    @raise Unsupported if the input string contains unsupported UTF-8 characters. *)
 val classify : int -> status
 
-(** Check whether a given string be used as a legal identifier.
-    - [None] means yes
-    - [Some (b,s)] means no, with explanation [s] and severity [b] *)
+(** Return [None] if a given string can be used as a (Coq) identifier.
+    Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity.
+    @raise Unsupported if the input string contains unsupported UTF-8 characters. *)
 val ident_refutation : string -> (bool * string) option
 
-(** First char of a string, converted to lowercase *)
+(** First char of a string, converted to lowercase
+    @raise Unsupported if the input string contains unsupported UTF-8 characters.
+    @raise Assert_failure if the input string is empty. *)
 val lowercase_first_char : string -> string
 
-(** 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.
+    Those UTF-8 characters which do not have their ASCII counterparts are
+    translated to ["__Uxxxx_"] where {i xxxx} are four hexadecimal digits.
+    @raise Unsupported if the input string contains unsupported UTF-8 characters. *)
 val ascii_of_ident : string -> string
diff --git a/lib/util.ml b/lib/util.ml
index a20dba0fc4..b67539918d 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -124,6 +124,7 @@ 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
 
 let map_union f g = function
   | Inl a -> Inl (f a)
diff --git a/lib/util.mli b/lib/util.mli
index 1dc405fcbe..0ce6cc6603 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -111,5 +111,7 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
 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. *)