Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

96 files changed, 1036 insertions, 695 deletions

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index c9018c9ee9..f7bd81f85d 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -42,6 +42,8 @@ module M = Map.Make(String)
 type data = string M.t
 type aux_file = data H.t
 
+let contents x = x
+
 let empty_aux_file = H.empty
 
 let get aux loc key = M.find key (H.find (Loc.unloc loc) aux)
diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index e340fc6547..127827ab6a 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -13,6 +13,10 @@ val get : aux_file -> Loc.t -> string -> string
 val empty_aux_file : aux_file
 val set : aux_file -> Loc.t -> string -> string -> aux_file
 
+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 stop_aux_file : unit -> unit 
 val recording : unit -> bool
diff --git a/lib/bigint.ml b/lib/bigint.ml
index e739c7a112..e95604ffc0 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/bigint.mli b/lib/bigint.mli
index 02e3c1ad55..e5525f164e 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/ephemeron.ml b/lib/cEphemeron.ml
index b36904ca64..a38ea11e10 100644
--- a/lib/ephemeron.ml
+++ b/lib/cEphemeron.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/ephemeron.mli b/lib/cEphemeron.mli
index 195b23db31..1200e4e208 100644
--- a/lib/ephemeron.mli
+++ b/lib/cEphemeron.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/cList.ml b/lib/cList.ml
index 0ac372d8d8..ba592d13f3 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -48,6 +48,8 @@ sig
   val filteri :
     (int -> 'a -> bool) -> '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
@@ -375,6 +377,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)
@@ -638,12 +652,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..9c7b815c15 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -94,6 +94,11 @@ sig
   (** [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). *)
 
diff --git a/lib/cMap.ml b/lib/cMap.ml
index 876f847365..4b058380c6 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -23,8 +23,9 @@ module type S = Map.S
 
 module type ExtS =
 sig
-  include Map.S
+  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
@@ -207,4 +208,5 @@ 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 cd3d2f5b19..3ef7fa2c8a 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -25,12 +25,15 @@ module type S = Map.S
 
 module type ExtS =
 sig
-  include Map.S
+  include CSig.MapS
   (** The underlying Map library *)
 
   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. *)
diff --git a/lib/cSet.ml b/lib/cSet.ml
index d7d5c70b39..037cdc3568 100644
--- a/lib/cSet.ml
+++ b/lib/cSet.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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/cSet.mli b/lib/cSet.mli
index e550541031..2452bb60e5 100644
--- a/lib/cSet.mli
+++ b/lib/cSet.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/cSig.mli b/lib/cSig.mli
index 2a8bda2936..151cfbdca5 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,36 @@ sig
 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
+    type (+'a) t
+    val empty: 'a t
+    val is_empty: 'a t -> bool
+    val mem: key -> 'a t -> bool
+    val add: key -> 'a -> 'a t -> 'a t
+    val singleton: key -> 'a -> 'a t
+    val remove: key -> 'a t -> 'a t
+    val merge:
+         (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
+    val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+    val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+    val iter: (key -> 'a -> unit) -> 'a t -> unit
+    val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+    val for_all: (key -> 'a -> bool) -> 'a t -> bool
+    val exists: (key -> 'a -> bool) -> 'a t -> bool
+    val filter: (key -> 'a -> bool) -> 'a t -> 'a t
+    val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
+    val cardinal: 'a t -> int
+    val bindings: 'a t -> (key * 'a) list
+    val min_binding: 'a t -> (key * 'a)
+    val max_binding: 'a t -> (key * 'a)
+    val choose: 'a t -> (key * 'a)
+    val split: key -> 'a t -> 'a t * 'a option * 'a t
+    val find: key -> 'a t -> 'a
+    val map: ('a -> 'b) -> 'a t -> 'b t
+    val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
+end
diff --git a/lib/cString.ml b/lib/cString.ml
index e9006860fd..0c2ed2e7c0 100644
--- a/lib/cString.ml
+++ b/lib/cString.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/cString.mli b/lib/cString.mli
index 4fa9e1e934..5292b34d0a 100644
--- a/lib/cString.mli
+++ b/lib/cString.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/cThread.ml b/lib/cThread.ml
index 2d1f10bf39..4f60a69745 100644
--- a/lib/cThread.ml
+++ b/lib/cThread.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -8,22 +8,12 @@
 
 type thread_ic = in_channel
 
-let prepare_in_channel_for_thread_friendly_io ic =
-  Unix.set_nonblock (Unix.descr_of_in_channel ic); ic
-
-let safe_wait_timed_read fd time =
-  try Thread.wait_timed_read fd time
-  with Unix.Unix_error (Unix.EINTR, _, _) ->
-    (** On Unix, the above function may raise this exception when it is
-        interrupted by a signal. (It uses Unix.select internally.) *)
-    false
+let prepare_in_channel_for_thread_friendly_io ic = ic
 
 let thread_friendly_read_fd fd s ~off ~len =
   let rec loop () =
     try Unix.read fd s off len
-    with Unix.Unix_error((Unix.EWOULDBLOCK|Unix.EAGAIN|Unix.EINTR),_,_) ->
-      while not (safe_wait_timed_read fd 0.05) do Thread.yield () done;
-      loop ()
+    with Unix.Unix_error(Unix.EINTR,_,_) -> loop ()
   in 
     loop ()
 
diff --git a/lib/cThread.mli b/lib/cThread.mli
index 8b110f3f3e..7302dfb558 100644
--- a/lib/cThread.mli
+++ b/lib/cThread.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/cUnix.ml b/lib/cUnix.ml
index 4a1fc7621f..cb436511fb 100644
--- a/lib/cUnix.ml
+++ b/lib/cUnix.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/cUnix.mli b/lib/cUnix.mli
index 2d0d202d77..f03719c3d2 100644
--- a/lib/cUnix.mli
+++ b/lib/cUnix.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/canary.ml b/lib/canary.ml
index 23d7bd2166..c01bc15879 100644
--- a/lib/canary.ml
+++ b/lib/canary.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/canary.mli b/lib/canary.mli
index c0ba86a797..21949e7359 100644
--- a/lib/canary.mli
+++ b/lib/canary.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 7ff1d29359..3c1c5da33c 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -8,6 +8,7 @@ Hashcons
 CSet
 CMap
 Int
+Dyn
 HMap
 Option
 Store
@@ -18,11 +19,11 @@ Pp_control
 Flags
 Control
 Loc
+CList
+CString
 Serialize
 Deque
 CObj
-CList
-CString
 CArray
 CStack
 Util
diff --git a/lib/control.ml b/lib/control.ml
index 673a75a20a..bf0e1b1cd7 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/control.mli b/lib/control.mli
index 2a496bcac2..681df313bc 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/deque.ml b/lib/deque.ml
index c04d599391..ac89a35b15 100644
--- a/lib/deque.ml
+++ b/lib/deque.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/deque.mli b/lib/deque.mli
index fd644e3c63..6963f1dbac 100644
--- a/lib/deque.mli
+++ b/lib/deque.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 056b687313..676467e464 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -1,17 +1,60 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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 Errors
-open Pp
+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 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
+
+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 +67,44 @@ 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
diff --git a/lib/dyn.mli b/lib/dyn.mli
index cac912aca1..c94fa764ba 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -1,17 +1,52 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
 (************************************************************************)
 
 (** Dynamics. Use with extreme care. Not for kids. *)
+module type TParam =
+sig
+  type 'a t
+end
 
-type t
+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
+
+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 315d28cebd..89ce528318 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -39,25 +39,14 @@ let path_to_list p =
 let user_path () =
   path_to_list (Sys.getenv "PATH") (* may raise Not_found *)
 
-  (* Duplicated from system.ml to minimize dependencies *)
-let file_exists_respecting_case f =
-  if Coq_config.arch = "Darwin" then
-    (* ensure that the file exists with expected case on the
-       case-insensitive but case-preserving default MacOS file system *)
-    let rec aux f =
-      let bf = Filename.basename f in
-      let df = Filename.dirname f in
-      String.equal df "." || String.equal df "/" ||
-      aux df && Array.exists (String.equal bf) (Sys.readdir df)
-    in aux f
-  else Sys.file_exists f
-
+(* Finding a name in path using the equality provided by the file system *)
+(* whether it is case-sensitive or case-insensitive *)
 let rec which l f =
   match l with
     | [] ->
       raise Not_found
     | p :: tl ->
-      if file_exists_respecting_case (p / f) then
+      if Sys.file_exists (p / f) then
 	p
       else
 	which tl f
@@ -112,10 +101,11 @@ let _ =
 (** [check_file_else ~dir ~file oth] checks if [file] exists in
     the installation directory [dir] given relatively to [coqroot].
     If this Coq is only locally built, then [file] must be in [coqroot].
-    If the check fails, then [oth ()] is evaluated. *)
+    If the check fails, then [oth ()] is evaluated.
+    Using file system equality seems well enough for this heuristic *)
 let check_file_else ~dir ~file oth =
   let path = if Coq_config.local then coqroot else coqroot / dir in
-  if file_exists_respecting_case (path / file) then path else oth ()
+  if Sys.file_exists (path / file) then path else oth ()
 
 let guess_coqlib fail =
   let prelude = "theories/Init/Prelude.vo" in
@@ -147,7 +137,7 @@ let coqpath =
   let coqpath = getenv_else "COQPATH" (fun () -> "") in
   let make_search_path path =
     let paths = path_to_list path in
-    let valid_paths = List.filter file_exists_respecting_case paths in
+    let valid_paths = List.filter Sys.file_exists paths in
     List.rev valid_paths
   in
   make_search_path coqpath
diff --git a/lib/envars.mli b/lib/envars.mli
index 7c20c035a5..90a42859b9 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/explore.ml b/lib/explore.ml
index 3d57fc0826..587db11563 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/explore.mli b/lib/explore.mli
index f3679188c9..2b273e12b2 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/feedback.ml b/lib/feedback.ml
index a5e16ea04c..1a90685de6 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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..0d8e20230d 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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 9a0d4b5ec1..c1ec9738ca 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -83,6 +83,8 @@ let profile = false
 let print_emacs = ref false
 let coqtop_ui = ref false
 
+let xml_export = ref false
+
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
@@ -101,18 +103,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 +124,7 @@ let pr_version = function
   | V8_2 -> "8.2"
   | V8_3 -> "8.3"
   | V8_4 -> "8.4"
+  | V8_5 -> "8.5"
   | Current -> "current"
 
 (* Translate *)
diff --git a/lib/flags.mli b/lib/flags.mli
index 29a0bbef01..24780f0dcc 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -44,6 +44,8 @@ val profile : bool
 val print_emacs : bool ref
 val coqtop_ui : bool ref
 
+val xml_export : bool ref
+
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
 
@@ -55,7 +57,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
@@ -88,6 +90,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
 
diff --git a/lib/future.ml b/lib/future.ml
index 02d3702d77..9cdc1c20e3 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -1,31 +1,38 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
 (************************************************************************)
 
 (* 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
 
-exception NotReady of string
-exception NotHere of string
-let _ = Errors.register_handler (function
-  | NotReady name ->
+let not_ready_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^
                 "Please wait or pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
                 "asynchronous script processing and don't pass \"-quick\" to "^
-                "coqc.")
-  | NotHere name ->
+                "coqc."))
+let not_here_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not available "^
                 "in this process. If you really need this, pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
                 "asynchronous script processing and don't pass \"-quick\" to "^
-                "coqc.")
+                "coqc."))
+
+let customize_not_ready_msg f = not_ready_msg := f
+let customize_not_here_msg f = not_here_msg := f
+
+exception NotReady of string
+exception NotHere of string
+let _ = Errors.register_handler (function
+  | NotReady name -> !not_ready_msg name
+  | NotHere name -> !not_here_msg name
   | _ -> raise Errors.Unhandled)
 
 type fix_exn = Exninfo.iexn -> Exninfo.iexn
@@ -52,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
@@ -64,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  ]
diff --git a/lib/future.mli b/lib/future.mli
index 324d5f7d10..114c591765 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -91,13 +91,13 @@ val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
  * When a future enters the environment a corresponding hook is run to perform
  * some work.  If this fails, then its failure has to be annotated with the
  * same state id that corresponds to the future computation end.  I.e. Qed
- * is split into two parts, the lazy one (the future) and the eagher one
+ * is split into two parts, the lazy one (the future) and the eager one
  * (the hook), both performing some computations for the same state id. *)
 val fix_exn_of : 'a computation -> fix_exn
 
 (* Run remotely, returns the function to assign.
    If not blocking (the default) it raises NotReady if forced before the
-   delage assigns it. *)
+   delegate assigns it. *)
 type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
 val create_delegate :
   ?blocking:bool -> name:string ->
@@ -157,7 +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..ef0de89afb 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -9,167 +9,228 @@
 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 ValT = Dyn.Make(struct end)
+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 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
-(** Alias for concision *)
+module Val =
+struct
 
-(* Dynamics but tagged by a type expression *)
+  type 'a typ = 'a ValT.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 -> ValT.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 repr = ValT.repr
+
+  let rec pr : type a. a tag -> std_ppcmds = function
+  | Base t -> str (repr t)
+  | List t -> pr t ++ spc () ++ str "list"
+  | Opt t -> pr t ++ spc () ++ str "option"
+  | Pair (t1, t2) -> str "(" ++ pr t1 ++ str " * " ++ pr t2 ++ str ")"
 
-type rlevel
-type glevel
-type tlevel
+end
 
-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
+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
 
-let rawwit t = t
-let glbwit t = t
-let topwit t = t
+type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
+(** Alias for concision *)
 
-let wit_list t = ListArgType t
+(* Dynamics but tagged by a type expression *)
 
-let wit_opt t = OptArgType t
+type rlevel = [ `rlevel ]
+type glevel = [ `glevel ]
+type tlevel = [ `tlevel ]
 
-let wit_pair t1 t2 = PairArgType (t1,t2)
+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
 
-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
+type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument
 
-let has_type (t, v) u = argument_type_eq t u
+type raw_generic_argument = rlevel generic_argument
+type glob_generic_argument = glevel generic_argument
+type typed_generic_argument = tlevel generic_argument
 
-let unquote x = x
+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
 
-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"
+(** Creating args *)
 
-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 }
+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 pair_unpack pack (t, obj) = match t with
-| PairArgType (t1, t2) -> pack.pair_unpacker t1 t2 (Obj.obj obj)
-| _ -> failwith "out_gen"
+type ('raw, 'glb, 'top) load = {
+  dyn : 'top Val.tag;
+}
 
-(** Creating args *)
+module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end)
 
-let (arg0_map : Obj.t option String.Map.t ref) = ref String.Map.empty
+let arg0_map = ref LoadMap.empty
 
-let create_arg opt name =
-  if String.Map.mem name !arg0_map then
+let create_arg ?dyn name =
+  match ArgT.name name with
+  | Some _ ->
     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
+  | None ->
+    let dyn = match dyn with None -> Val.Base (ValT.create name) | Some dyn -> dyn in
+    let obj = LoadMap.Pack { dyn; } in
+    let name = ArgT.create name in
+    let () = arg0_map := LoadMap.add name obj !arg0_map in
+    ExtraArg 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
+let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function
+| ListArg t -> Val.List (val_tag t)
+| OptArg t -> Val.Opt (val_tag t)
+| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2)
+| ExtraArg s ->
+  match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.dyn
+
+let val_tag = function Topwit t -> val_tag t
 
 (** Registering genarg-manipulating functions *)
 
@@ -182,54 +243,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
+  | ExtraArg s ->
+    if GenMap.mem s !arg0_map then
+      let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) in
       Errors.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)
+        Errors.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 a269f92774..93665fd45d 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -68,18 +68,54 @@ ExtraArgType of string         '_a                      '_b
 
 (** {5 Generic types} *)
 
-type ('raw, 'glob, 'top) genarg_type
+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
+
+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
 (** 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 typ -> string
+  val pr : '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 : ?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 : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
 (** Alias for [make0]. *)
 
 (** {5 Specialized types} *)
@@ -91,11 +127,14 @@ val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type
    out_gen is monomorphic over 'a, hence type-safe
 *)
 
-type rlevel
-type glevel
-type tlevel
+type rlevel = [ `rlevel ]
+type glevel = [ `glevel ]
+type tlevel = [ `tlevel ]
 
-type ('a, 'co) abstract_argument_type
+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 at level ['co] represented by an OCaml value of type ['a]. *)
 
 type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type
@@ -120,7 +159,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 +180,26 @@ 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 }
+(** {6 Dynamic toplevel values} *)
 
-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
+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. *)
 
 (** {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. *)
@@ -244,35 +243,3 @@ val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_ty
 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 8e900cd581..778c366fd5 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -286,6 +286,8 @@ struct
     let m = Int.Map.find h s in
     Map.find k m
 
+  let get k s = try find k s with Not_found -> assert false
+
   let split k s = assert false (** Cannot be implemented efficiently *)
 
   let map f s =
@@ -333,7 +335,6 @@ struct
   struct
     module IntM = Int.Map.Monad(M)
     module ExtM = Map.Monad(M)
-    open M
 
     let fold f s accu =
       let ff _ m accu = ExtM.fold f m accu in
diff --git a/lib/hMap.mli b/lib/hMap.mli
index cdf933b298..c4e6a08e1b 100644
--- a/lib/hMap.mli
+++ b/lib/hMap.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 46ba0b6285..4eaacf9145 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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 8d0adc3fd6..150899cef5 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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 1ca6cc6418..af33544dc6 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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 a455eec662..733c89621c 100644
--- a/lib/hashset.mli
+++ b/lib/hashset.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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 a19bc0d1c3..97ccadeba8 100644
--- a/lib/heap.ml
+++ b/lib/heap.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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/heap.mli b/lib/heap.mli
index a69de34cef..0e77a3a068 100644
--- a/lib/heap.mli
+++ b/lib/heap.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/hook.ml b/lib/hook.ml
index 0aa373c21c..a370fe3578 100644
--- a/lib/hook.ml
+++ b/lib/hook.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/hook.mli b/lib/hook.mli
index d10f2c86f0..50347f334f 100644
--- a/lib/hook.mli
+++ b/lib/hook.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/iStream.ml b/lib/iStream.ml
index f9351d4bb5..26a666e176 100644
--- a/lib/iStream.ml
+++ b/lib/iStream.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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/iStream.mli b/lib/iStream.mli
index 8cb12af468..50f5389ba2 100644
--- a/lib/iStream.mli
+++ b/lib/iStream.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/int.ml b/lib/int.ml
index d99176572f..70bd742427 100644
--- a/lib/int.ml
+++ b/lib/int.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/int.mli b/lib/int.mli
index c910bda6ac..93d1be1f7d 100644
--- a/lib/int.mli
+++ b/lib/int.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/lib.mllib b/lib/lib.mllib
index f3f6ad8fc7..2be435f6ff 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,6 +1,5 @@
 Errors
 Bigint
-Dyn
 Segmenttree
 Unicodetable
 Unicode
@@ -15,6 +14,6 @@ Rtree
 Heap
 Unionfind
 Genarg
-Ephemeron
+CEphemeron
 Future
 RemoteCounter
diff --git a/lib/loc.ml b/lib/loc.ml
index b62677d484..afdab928c4 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -31,7 +31,7 @@ let ghost = {
   fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
   bp = 0; ep = 0; }
 
-let is_ghost loc = Pervasives.(=) loc ghost (** FIXME *)
+let is_ghost loc = loc.ep = 0
 
 let merge loc1 loc2 =
   if loc1.bp < loc2.bp then
diff --git a/lib/loc.mli b/lib/loc.mli
index 7a9a9ffdbb..f39cd2670b 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/option.ml b/lib/option.ml
index 9ea1a76982..fbb883d30a 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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..5e085620e7 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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 30bc30a9ad..c7cf9b8d0e 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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
 
@@ -268,7 +261,7 @@ let rec pr_com ft s =
       let n = String.index s '\n' in
       String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1))
     with Not_found -> s,None in
-  com_if ft (Lazy.lazy_from_val());
+  com_if ft (Lazy.from_val());
 (*  let s1 =
     if String.length s1 <> 0 && s1.[0] = ' ' then
       (Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1))
@@ -297,29 +290,29 @@ let pp_dirs ?pp_tag ft =
         begin match tok with
         | Str_def s ->
           let n = utf8_length s in
-          com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s
+          com_if ft (Lazy.from_val()); Format.pp_print_as ft n s
         | Str_len (s, n) ->
-          com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s
+          com_if ft (Lazy.from_val()); Format.pp_print_as ft n s
         end
     | Ppcmd_box(bty,ss)       -> (* Prevent evaluation of the stream! *)
-        com_if ft (Lazy.lazy_from_val());
+        com_if ft (Lazy.from_val());
         pp_open_box bty ;
         if not (Format.over_max_boxes ()) then Glue.iter pp_cmd ss;
         Format.pp_close_box ft ()
-    | Ppcmd_open_box bty      -> com_if ft (Lazy.lazy_from_val()); pp_open_box bty
+    | Ppcmd_open_box bty      -> com_if ft (Lazy.from_val()); pp_open_box bty
     | Ppcmd_close_box         -> Format.pp_close_box ft ()
     | Ppcmd_close_tbox        -> Format.pp_close_tbox ft ()
     | Ppcmd_white_space n     ->
-        com_if ft (Lazy.lazy_from_fun (fun()->Format.pp_print_break ft n 0))
+        com_if ft (Lazy.from_fun (fun()->Format.pp_print_break ft n 0))
     | Ppcmd_print_break(m,n)  ->
-        com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_break ft m n))
+        com_if ft (Lazy.from_fun(fun()->Format.pp_print_break ft m n))
     | Ppcmd_set_tab           -> Format.pp_set_tab ft ()
     | Ppcmd_print_tbreak(m,n) ->
-        com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_tbreak ft m n))
+        com_if ft (Lazy.from_fun(fun()->Format.pp_print_tbreak ft m n))
     | Ppcmd_force_newline     ->
         com_brk ft; Format.pp_force_newline ft ()
     | Ppcmd_print_if_broken   ->
-        com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_if_newline ft ()))
+        com_if ft (Lazy.from_fun(fun()->Format.pp_print_if_newline ft ()))
     | Ppcmd_comment i         ->
         let coms = split_com [] [] i !comments in
 (*        Format.pp_open_hvbox ft 0;*)
@@ -362,11 +355,11 @@ let emacs_quote_info_start = "<infomsg>"
 let emacs_quote_info_end = "</infomsg>"
 
 let emacs_quote g =
-  if !print_emacs then str emacs_quote_start ++ hov 0 g ++ str emacs_quote_end
+  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 str emacs_quote_info_start++fnl() ++ hov 0 g ++ str emacs_quote_info_end
+  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
 
 
@@ -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
@@ -424,7 +417,7 @@ type logger = message_level -> std_ppcmds -> unit
 let make_body info s =
   emacs_quote (hov 0 (info ++ spc () ++ s))
 
-let debugbody strm = hov 0 (str "Debug:" ++ spc () ++ strm)
+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
@@ -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 })
 
@@ -525,6 +518,7 @@ 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
 
diff --git a/lib/pp.mli b/lib/pp.mli
index 3b1123a9dc..2e4d029749 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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
@@ -199,6 +199,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. *)
 
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 969c1550ec..890ffe0a18 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 28d2e2998b..d26f89eb30 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
index fb334c706b..3ecaac0391 100644
--- a/lib/ppstyle.ml
+++ b/lib/ppstyle.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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 Util
+module String = CString
 
 type t = string
 (** We use the concatenated string, with dots separating each string. We
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
index f5d6184cb1..97b5869f9b 100644
--- a/lib/ppstyle.mli
+++ b/lib/ppstyle.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/predicate.ml b/lib/predicate.ml
index a60b3dadd4..1aa7db6af1 100644
--- a/lib/predicate.ml
+++ b/lib/predicate.ml
@@ -10,8 +10,6 @@
 (*                                                                     *)
 (************************************************************************)
 
-(* Sets over ordered types *)
-
 module type OrderedType =
   sig
     type t
@@ -43,9 +41,10 @@ module Make(Ord: OrderedType) =
   struct
     module EltSet = Set.Make(Ord)
 
-    (* when bool is false, the denoted set is the complement of
-       the given set *)
     type elt = Ord.t
+
+    (* (false, s) represents a set which is equal to the set s
+       (true, s)  represents a set which is equal to the complement of set s *)
     type t = bool * EltSet.t
 
     let elements (b,s) = (b, EltSet.elements s)
@@ -84,6 +83,7 @@ module Make(Ord: OrderedType) =
 
     let diff s1 s2 = inter s1 (complement s2)
 
+    (* assumes the set is infinite *)
     let subset s1 s2 =
       match (s1,s2) with
           ((false,p1),(false,p2)) -> EltSet.subset p1 p2
@@ -91,6 +91,7 @@ module Make(Ord: OrderedType) =
         | ((false,p1),(true,n2)) -> EltSet.is_empty (EltSet.inter p1 n2)
         | ((true,_),(false,_)) -> false
 
+    (* assumes the set is infinite *)
     let equal (b1,s1) (b2,s2) =
       b1=b2 && EltSet.equal s1 s2
 
diff --git a/lib/predicate.mli b/lib/predicate.mli
index bcc89e7275..cee3b0bd39 100644
--- a/lib/predicate.mli
+++ b/lib/predicate.mli
@@ -1,67 +1,84 @@
+(** Infinite sets over a chosen [OrderedType].
 
-(** Module [Pred]: sets over infinite ordered types with complement. *)
-
-(** This module implements the set data structure, given a total ordering
-   function over the set elements. All operations over sets
-   are purely applicative (no side-effects).
-   The implementation uses the Set library. *)
+    All operations over sets are purely applicative (no side-effects).
+ *)
 
+(** Input signature of the functor [Make]. *)
 module type OrderedType =
   sig
     type t
-    val compare: t -> t -> int
+    (** The type of the elements in the set.
+
+	The chosen [t] {b must be infinite}. *)
+
+    val compare : t -> t -> int
+    (** A total ordering function over the set elements.
+        This is a two-argument function [f] such that:
+        - [f e1 e2] is zero if the elements [e1] and [e2] are equal,
+        - [f e1 e2] is strictly negative if [e1] is smaller than [e2],
+        - and [f e1 e2] is strictly positive if [e1] is greater than [e2].
+     *)
   end
-          (** The input signature of the functor [Pred.Make].
-             [t] is the type of the set elements.
-             [compare] is a total ordering function over the set elements.
-             This is a two-argument function [f] such that
-             [f e1 e2] is zero if the elements [e1] and [e2] are equal,
-             [f e1 e2] is strictly negative if [e1] is smaller than [e2],
-             and [f e1 e2] is strictly positive if [e1] is greater than [e2].
-             Example: a suitable ordering function is
-             the generic structural comparison function [compare]. *)
 
 module type S =
   sig
     type elt
-          (** The type of the set elements. *)
+    (** The type of the elements in the set. *)
+
     type t
-          (** The type of sets. *)
+    (** The type of sets. *)
+
     val empty: t
-          (** The empty set. *)
+    (** The empty set. *)
+
     val full: t
-          (** The whole type. *)
+    (** The set of all elements (of type [elm]). *)
+
     val is_empty: t -> bool
-        (** Test whether a set is empty or not. *)
+    (** Test whether a set is empty or not. *)
+
     val is_full: t -> bool
-        (** Test whether a set contains the whole type or not. *)
+    (** Test whether a set contains the whole type or not. *)
+
     val mem: elt -> t -> bool
-        (** [mem x s] tests whether [x] belongs to the set [s]. *)
+    (** [mem x s] tests whether [x] belongs to the set [s]. *)
+
     val singleton: elt -> t
-        (** [singleton x] returns the one-element set containing only [x]. *)
+    (** [singleton x] returns the one-element set containing only [x]. *)
+
     val add: elt -> t -> t
-        (** [add x s] returns a set containing all elements of [s],
-           plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
+    (** [add x s] returns a set containing all elements of [s],
+        plus [x]. If [x] was already in [s], then [s] is returned unchanged. *)
+
     val remove: elt -> t -> t
         (** [remove x s] returns a set containing all elements of [s],
-           except [x]. If [x] was not in [s], [s] is returned unchanged. *)
+            except [x]. If [x] was not in [s], then [s] is returned unchanged. *)
+
     val union: t -> t -> t
+    (** Set union. *)
+
     val inter: t -> t -> t
+    (** Set intersection. *)
+
     val diff: t -> t -> t
+    (** Set difference. *)
+
     val complement: t -> t
-        (** Union, intersection, difference and set complement. *)
+    (** Set complement. *)
+
     val equal: t -> t -> bool
-        (** [equal s1 s2] tests whether the sets [s1] and [s2] are
-           equal, that is, contain equal elements. *)
+    (** [equal s1 s2] tests whether the sets [s1] and [s2] are
+        equal, that is, contain equal elements. *)
+
     val subset: t -> t -> bool
         (** [subset s1 s2] tests whether the set [s1] is a subset of
-           the set [s2]. *)
+            the set [s2]. *)
+
     val elements: t -> bool * elt list
         (** Gives a finite representation of the predicate: if the
            boolean is false, then the predicate is given in extension.
            if it is true, then the complement is given *)
   end
 
-module Make(Ord: OrderedType): (S with type elt = Ord.t)
-        (** Functor building an implementation of the set structure
-           given a totally ordered type. *)
+(** The [Make] functor constructs an implementation for any [OrderedType]. *)
+module Make (Ord : OrderedType) : (S with type elt = Ord.t)
diff --git a/lib/profile.ml b/lib/profile.ml
index c55064ca85..2350cd43ac 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/profile.mli b/lib/profile.mli
index e3221cd2bc..3328d7ea3c 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index f4d7bb7b8b..3f1982594a 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli
index f3eca418ff..1b0fa6a00e 100644
--- a/lib/remoteCounter.mli
+++ b/lib/remoteCounter.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/richpp.ml b/lib/richpp.ml
index c4a9c39d5a..fe3edd99ca 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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..807d52aba4 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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/rtree.ml b/lib/rtree.ml
index f395c086a5..f89b98c046 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 0b9424b893..e27134c3b6 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/serialize.ml b/lib/serialize.ml
index aa2e3f02a4..685ec6049c 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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..d7c14e7e73 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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/spawn.ml b/lib/spawn.ml
index 9b63be70aa..fda4b4239a 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -45,26 +45,38 @@ end
 (* Common code *)
 let assert_ b s = if not b then Errors.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
+ * in 4.03 *)
 let mk_socket_channel () =
   let open Unix in
-  let s = socket PF_INET SOCK_STREAM 0 in
-  bind s (ADDR_INET (inet_addr_loopback,0));
-  listen s 1;
-  match getsockname s with
-  | ADDR_INET(host, port) ->
-      s, string_of_inet_addr host ^":"^ string_of_int port
+  let sr = socket PF_INET SOCK_STREAM 0 in
+  bind sr (ADDR_INET (inet_addr_loopback,0)); listen sr 1;
+  let sw = socket PF_INET SOCK_STREAM 0 in
+  bind sw (ADDR_INET (inet_addr_loopback,0)); listen sw 1;
+  match getsockname sr, getsockname sw with
+  | ADDR_INET(host, portr), ADDR_INET(_, portw) ->
+      (sr, sw),
+      string_of_inet_addr host
+        ^":"^ string_of_int portr ^":"^ string_of_int portw
   | _ -> assert false
 
-let accept s =
-  let r, _, _ = Unix.select [s] [] [] accept_timeout in
+let accept (sr,sw) =
+  let r, _, _ = Unix.select [sr] [] [] accept_timeout in
   if r = [] then raise (Failure (Printf.sprintf
     "The spawned process did not connect back in %2.1fs" accept_timeout));
-  let cs, _ = Unix.accept s in
-  Unix.close s;
-  let cin, cout = Unix.in_channel_of_descr cs, Unix.out_channel_of_descr cs in
+  let csr, _ = Unix.accept sr in
+  Unix.close sr;
+  let cin = Unix.in_channel_of_descr csr in
   set_binary_mode_in cin true;
+  let w, _, _ = Unix.select [sw] [] [] accept_timeout in
+  if w = [] then raise (Failure (Printf.sprintf
+    "The spawned process did not connect back in %2.1fs" accept_timeout));
+  let csw, _ = Unix.accept sw in
+  Unix.close sw;
+  let cout = Unix.out_channel_of_descr csw in
   set_binary_mode_out cout true;
-  cs, cin, cout
+  (csr, csw), cin, cout
 
 let handshake cin cout =
   try
@@ -116,7 +128,7 @@ let spawn_pipe env prog args =
   let cout = Unix.out_channel_of_descr master2worker_w in
   set_binary_mode_in cin true;
   set_binary_mode_out cout true;
-  pid, cin, cout, worker2master_r
+  pid, cin, cout, (worker2master_r, master2worker_w)
 
 let filter_args args =
   let rec aux = function
@@ -163,7 +175,7 @@ let is_alive p = p.alive
 let uid { pid; } = string_of_int pid
 let unixpid { pid; } = pid
 
-let kill ({ pid = unixpid; oob_req; cin; cout; alive; watch } as p) =
+let kill ({ pid = unixpid; oob_resp; oob_req; cin; cout; alive; watch } as p) =
   p.alive <- false;
   if not alive then prerr_endline "This process is already dead"
   else begin try
@@ -171,6 +183,8 @@ let kill ({ pid = unixpid; oob_req; cin; cout; alive; watch } as p) =
     output_death_sentence (uid p) oob_req;
     close_in_noerr cin;
     close_out_noerr cout;
+    close_in_noerr oob_resp;
+    close_out_noerr oob_req;
     if Sys.os_type = "Unix" then Unix.kill unixpid 9;
     p.watch <- None
   with e -> prerr_endline ("kill: "^Printexc.to_string e) end
@@ -180,10 +194,10 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
 =
   let pid, oob_resp, oob_req, cin, cout, main, is_sock =
     spawn_with_control prefer_sock env prog args in
-  Unix.set_nonblock main;
+  Unix.set_nonblock (fst main);
   let gchan =
-    if is_sock then ML.async_chan_of_socket main
-    else ML.async_chan_of_file main in
+    if is_sock then ML.async_chan_of_socket (fst main)
+    else ML.async_chan_of_file (fst main) in
   let alive, watch = true, None in
   let p = { cin; cout; gchan; pid; oob_resp; oob_req; alive; watch } in
   p.watch <- Some (
@@ -206,10 +220,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
 
@@ -235,13 +252,15 @@ let is_alive p = p.alive
 let uid { pid; } = string_of_int pid
 let unixpid { pid = pid; } = pid
 
-let kill ({ pid = unixpid; oob_req; cin; cout; alive } as p) =
+let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) =
   p.alive <- false;
   if not alive then prerr_endline "This process is already dead"
   else begin try
     output_death_sentence (uid p) oob_req;
     close_in_noerr cin;
     close_out_noerr cout;
+    close_in_noerr oob_resp;
+    close_out_noerr oob_req;
     if Sys.os_type = "Unix" then Unix.kill unixpid 9;
   with e -> prerr_endline ("kill: "^Printexc.to_string e) end
 
@@ -251,8 +270,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/spawn.mli b/lib/spawn.mli
index 8022573bc2..9b86b09549 100644
--- a/lib/spawn.mli
+++ b/lib/spawn.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/system.ml b/lib/system.ml
index 26bf780101..10ef8580bf 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -11,7 +11,6 @@
 open Pp
 open Errors
 open Util
-open Unix
 
 (** Dealing with directories *)
 
@@ -44,7 +43,7 @@ let ok_dirname f =
 (* Check directory can be opened *)
 
 let exists_dir dir =
-  try let _ = closedir (opendir dir) in true with Unix_error _ -> false
+  try Sys.is_directory dir with Sys_error _ -> false
 
 let check_unix_dir warn dir =
   if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
@@ -57,17 +56,17 @@ let check_unix_dir warn dir =
 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 name.[0] <> '.' && ok_dirname name then
+  if ok_dirname name then
     let path = if path = "." then name else path//name in
-    match try (stat path).st_kind with Unix_error _ -> S_BLK with
-    | S_DIR -> f (FileDir (path,name))
-    | S_REG -> f (FileRegular name)
+    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 =
-  let dirh = opendir path in
-  try while true do apply_subdir f path (readdir dirh) done
-  with End_of_file -> closedir dirh
+  Array.iter (apply_subdir f path) (readdir path)
 
 let process_subdirectories f path =
   let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
@@ -94,17 +93,50 @@ let all_subdirs ~unix_path:root =
   else msg_warning (str ("Cannot open " ^ root));
   List.rev !l
 
-let file_exists_respecting_case f =
-  if Coq_config.arch = "Darwin" then
-    (* ensure that the file exists with expected case on the
-       case-insensitive but case-preserving default MacOS file system *)
-    let rec aux f =
-      let bf = Filename.basename f in
-      let df = Filename.dirname f in
-      (String.equal df "." || String.equal df "/" || aux df)
-      && Array.exists (String.equal bf) (Sys.readdir df)
-    in aux f
-  else Sys.file_exists f
+(* Caching directory contents for efficient syntactic equality of file
+   names even on case-preserving but case-insensitive file systems *)
+
+module StrMod = struct
+  type t = string
+  let compare = compare
+end
+
+module StrMap = Map.Make(StrMod)
+module StrSet = Set.Make(StrMod)
+
+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 (readdir dir)
+
+let exists_in_dir_respecting_case dir bf =
+  let cache_dir dir =
+    let contents = make_dir_table dir in
+    dirmap := StrMap.add dir contents !dirmap;
+    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 ||
+    not fresh &&
+      (* rescan, there is a new file we don't know about *)
+      StrSet.mem bf (cache_dir dir)
+
+let file_exists_respecting_case path f =
+  (* This function ensures that a file with expected lowercase/uppercase
+     is the correct one, even on case-insensitive file systems *)
+  let rec aux f =
+    let bf = Filename.basename f in
+    let df = Filename.dirname f in
+    (String.equal df "." || aux df)
+    && exists_in_dir_respecting_case (Filename.concat path df) bf
+  in (!Flags.batch_mode || Sys.file_exists (Filename.concat path f)) && aux f
 
 let rec search paths test =
   match paths with
@@ -130,7 +162,7 @@ let where_in_path ?(warn=true) path filename =
   in
   check_and_warn (search path (fun lpe ->
     let f = Filename.concat lpe filename in
-    if file_exists_respecting_case f then [lpe,f] else []))
+    if file_exists_respecting_case lpe filename then [lpe,f] else []))
 
 let where_in_path_rex path rex =
   search path (fun lpe ->
@@ -146,13 +178,18 @@ let where_in_path_rex path rex =
 
 let find_file_in_path ?(warn=true) paths filename =
   if not (Filename.is_implicit filename) then
-    if file_exists_respecting_case filename then
+    (* the name is considered to be a physical name and we use the file
+       system rules (e.g. possible case-insensitivity) to find it *)
+    if Sys.file_exists filename then
       let root = Filename.dirname filename in
       root, filename
     else
       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
+       physical name of a logical name, so we deal with it as a name
+       to be locate respecting case *)
     try where_in_path ~warn paths filename
     with Not_found ->
       errorlabstrm "System.find_file_in_path"
@@ -164,10 +201,12 @@ let is_in_path lpath filename =
   with Not_found -> false
 
 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 ->
+    msg_warning (str "system variable PATH not found");
+    false
 
 let open_trapping_failure name =
   try open_out_bin name
@@ -227,48 +266,42 @@ let skip_in_segment f ch =
 
 exception Bad_magic_number of string
 
-let raw_extern_intern magic =
-  let extern_state filename =
-    let channel = open_trapping_failure filename in
-    output_binary_int channel magic;
-    filename, channel
-  and intern_state 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);
-      channel
-    with
-    | End_of_file -> error_corrupted filename "premature end of file"
-    | Failure s | Sys_error s -> error_corrupted filename s
-  in
-  (extern_state,intern_state)
+let raw_extern_state magic filename =
+  let channel = open_trapping_failure filename in
+  output_binary_int channel magic;
+  channel
 
-let extern_intern ?(warn=true) magic =
-  let (raw_extern,raw_intern) = raw_extern_intern magic in
-  let extern_state name val_0 =
-    try
-      let (filename,channel) = raw_extern name in
-      try
-        marshal_out channel val_0;
-        close_out channel
-      with reraise ->
-	let reraise = Errors.push reraise in
-        let () = try_remove filename in
-        iraise reraise
-    with Sys_error s ->
-      errorlabstrm "System.extern_state" (str "System error: " ++ str s)
-  and intern_state paths name =
+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);
+    channel
+  with
+  | End_of_file -> error_corrupted filename "premature end of file"
+  | Failure s | Sys_error s -> error_corrupted filename s
+
+let extern_state magic filename val_0 =
+  try
+    let channel = raw_extern_state magic filename in
     try
-      let _,filename = find_file_in_path ~warn paths name in
-      let channel = raw_intern filename in
-      let v = marshal_in filename channel in
-      close_in channel;
-      v
-    with Sys_error s ->
-      errorlabstrm "System.intern_state" (str "System error: " ++ str s)
-  in
-  (extern_state,intern_state)
+      marshal_out channel val_0;
+      close_out channel
+    with reraise ->
+      let reraise = Errors.push reraise in
+      let () = try_remove filename in
+      iraise reraise
+  with Sys_error s ->
+    errorlabstrm "System.extern_state" (str "System error: " ++ str s)
+
+let intern_state magic filename =
+  try
+    let channel = raw_intern_state magic filename in
+    let v = marshal_in filename channel in
+    close_in channel;
+    v
+  with Sys_error s ->
+    errorlabstrm "System.intern_state" (str "System error: " ++ str s)
 
 let with_magic_number_check f a =
   try f a
@@ -283,7 +316,7 @@ type time = float * float * float
 
 let get_time () =
   let t = Unix.times ()  in
-  (Unix.gettimeofday(), t.tms_utime, t.tms_stime)
+  (Unix.gettimeofday(), t.Unix.tms_utime, t.Unix.tms_stime)
 
 (* Keep only 3 significant digits *)
 let round f = (floor (f *. 1e3)) *. 1e-3
diff --git a/lib/system.mli b/lib/system.mli
index eb29b69701..e1190dfb55 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -59,7 +59,7 @@ val where_in_path_rex :
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
 
-val file_exists_respecting_case : string -> bool
+val file_exists_respecting_case : string -> string -> bool
 
 (** {6 I/O functions } *)
 (** Generic input and output functions, parameterized by a magic number
@@ -68,11 +68,13 @@ val file_exists_respecting_case : string -> bool
 
 exception Bad_magic_number of string
 
-val raw_extern_intern : int ->
-  (string -> string * out_channel) * (string -> in_channel)
+val raw_extern_state : int -> string -> out_channel
 
-val extern_intern : ?warn:bool -> int ->
-  (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a)
+val raw_intern_state : int -> string -> in_channel
+
+val extern_state : int -> string -> 'a -> unit
+
+val intern_state : int -> string -> 'a
 
 val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
 
diff --git a/lib/terminal.ml b/lib/terminal.ml
index 58851ed274..de21f10280 100644
--- a/lib/terminal.ml
+++ b/lib/terminal.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/terminal.mli b/lib/terminal.mli
index 49172e3ce3..e0fd7f2284 100644
--- a/lib/terminal.mli
+++ b/lib/terminal.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/trie.ml b/lib/trie.ml
index e369e6ad47..0309fde9b2 100644
--- a/lib/trie.ml
+++ b/lib/trie.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/trie.mli b/lib/trie.mli
index 8184748583..de67e8f967 100644
--- a/lib/trie.mli
+++ b/lib/trie.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/unicode.ml b/lib/unicode.ml
index 1765e93dcd..938e8f1a99 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
@@ -168,6 +173,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 =
diff --git a/lib/unicode.mli b/lib/unicode.mli
index 098f6c919d..b8a11e2945 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -10,19 +10,32 @@
 
 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
+
+(** Validate an UTF-8 string *)
+val is_utf8 : string -> bool
diff --git a/lib/unionfind.ml b/lib/unionfind.ml
index c44aa73634..6e131d8fbd 100644
--- a/lib/unionfind.ml
+++ b/lib/unionfind.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/unionfind.mli b/lib/unionfind.mli
index 310d5e2ae5..ea249ae2e8 100644
--- a/lib/unionfind.mli
+++ b/lib/unionfind.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/util.ml b/lib/util.ml
index a20dba0fc4..009dfbe1c1 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 1dc405fcbe..6bed7e3552 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
@@ -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_datatype.mli b/lib/xml_datatype.mli
index f61ba032a2..a8e37935ba 100644
--- a/lib/xml_datatype.mli
+++ b/lib/xml_datatype.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll
index f6943dd132..290f2c89ab 100644
--- a/lib/xml_lexer.mll
+++ b/lib/xml_lexer.mll
@@ -88,7 +88,8 @@ let error lexbuf e =
 let newline = ['\n']
 let break = ['\r']
 let space = [' ' '\t']
-let identchar =  ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-']
+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' '<' '>' '&']
 
@@ -226,7 +227,7 @@ and entity = parse
                 { raise (Error EUnterminatedEntity) }
 
 and ident_name = parse
-        | identchar+
+        | ident
                 { lexeme lexbuf }
         | _ | eof
                 { error lexbuf EIdentExpected }
@@ -252,7 +253,7 @@ and attributes = parse
                 }
 
 and attribute = parse
-        | identchar+
+        | ident
                 { lexeme lexbuf }
         | _ | eof
                 { error lexbuf EAttributeNameExpected }
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
index cefb4af897..ac2eab352f 100644
--- a/lib/xml_parser.mli
+++ b/lib/xml_parser.mli
@@ -36,10 +36,10 @@ type t
 
 (** Several exceptions can be raised when parsing an Xml document : {ul
         {li {!Xml.Error} is raised when an xml parsing error occurs. the
-                {!Xml.error_msg} tells you which error occured during parsing
-                and the {!Xml.error_pos} can be used to retreive the document
-                location where the error occured at.}
-        {li {!Xml.File_not_found} is raised when and error occured while
+                {!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.}
         }
  *)
@@ -71,13 +71,13 @@ val error : error -> string
 (** Get the Xml error message as a string. *)
 val error_msg : error_msg -> string
 
-(** Get the line the error occured at. *)
+(** Get the line the error occurred at. *)
 val line : error_pos -> int
 
-(** Get the relative character range (in current line) the error occured at.*)
+(** 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 occured at. *)
+(** Get the absolute character range the error occurred at. *)
 val abs_range : error_pos -> int * int
 
 val pos : Lexing.lexbuf -> error_pos
@@ -98,7 +98,7 @@ val make : source -> t
  in the original Xmllight)}. *)
 val check_eof : t -> bool -> unit
 
-(** Once the parser is configurated, you can run the parser on a any kind
+(** 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
diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml
index bbb7b51ba3..e7e4d0cebc 100644
--- a/lib/xml_printer.ml
+++ b/lib/xml_printer.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)
diff --git a/lib/xml_printer.mli b/lib/xml_printer.mli
index e21eca2831..f24f51fff5 100644
--- a/lib/xml_printer.mli
+++ b/lib/xml_printer.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <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        *)