31 files changed, 403 insertions, 346 deletions

diff --git a/library/declare.ml b/library/declare.ml
index c9d5fdbe2f..3d063225f4 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -9,7 +9,7 @@
 (** This module is about the low-level declaration of logical objects *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Libnames
@@ -149,7 +149,7 @@ let cache_constant ((sp,kn), obj) =
       obj.cst_was_seff <- false;  
       if Global.exists_objlabel (Label.of_id (basename sp))
       then constant_of_kn kn
-      else Errors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
+      else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
     end else
       let () = check_exists sp in
       let kn', exported = Global.add_constant dir id obj.cst_decl in
@@ -353,7 +353,8 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
   mind_entry_polymorphic = false;
   mind_entry_universes = Univ.UContext.empty;
-  mind_entry_private = None })
+  mind_entry_private = None;
+})
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
 
@@ -398,7 +399,7 @@ let declare_mind mie =
 let pr_rank i = pr_nth (i+1)
 
 let fixpoint_message indexes l =
-  Flags.if_verbose msg_info (match l with
+  Flags.if_verbose Feedback.msg_info (match l with
   | [] -> anomaly (Pp.str "no recursive definition")
   | [id] -> pr_id id ++ str " is recursively defined" ++
       (match indexes with
@@ -413,7 +414,7 @@ let fixpoint_message indexes l =
 		    | None -> mt ()))
 
 let cofixpoint_message l =
-  Flags.if_verbose msg_info (match l with
+  Flags.if_verbose Feedback.msg_info (match l with
   | [] -> anomaly (Pp.str "No corecursive definition.")
   | [id] -> pr_id id ++ str " is corecursively defined"
   | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
@@ -423,16 +424,16 @@ let recursive_message isfix i l =
   (if isfix then fixpoint_message i else cofixpoint_message) l
 
 let definition_message id =
-  Flags.if_verbose msg_info (pr_id id ++ str " is defined")
+  Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined")
 
 let assumption_message id =
-  Flags.if_verbose msg_info (pr_id id ++ str " is assumed")
+  (* Changing "assumed" to "declared", "assuming" referring more to
+  the type of the object than to the name of the object (see
+  discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
+  Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared")
 
 (** Global universe names, in a different summary *)
 
-type universe_names =
-    (Univ.universe_level Idmap.t * Id.t Univ.LMap.t)
-
 (* Discharged or not *)
 type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
 
@@ -440,8 +441,9 @@ let cache_universes (p, l) =
   let glob = Universes.global_universe_names () in
   let glob', ctx =
     List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
-		    ((Idmap.add id lev idl, Univ.LMap.add lev id lid),
-		     Univ.ContextSet.add_universe lev ctx))
+        ((Idmap.add id (p, lev) idl,
+          Univ.LMap.add lev id lid),
+         Univ.ContextSet.add_universe lev ctx))
       (glob, Univ.ContextSet.empty) l
   in
     Global.push_context_set p ctx;
@@ -457,6 +459,12 @@ let input_universes : universe_decl -> Libobject.obj =
       classify_function = (fun a -> Keep a) }
 
 let do_universe poly l =
+  let in_section = Lib.sections_are_opened () in
+  let () =
+    if poly && not in_section then
+      user_err_loc (Loc.ghost, "Constraint",
+                    str"Cannot declare polymorphic universes outside sections")
+  in
   let l =
     List.map (fun (l, id) ->
 	      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
@@ -485,14 +493,30 @@ let input_constraints : constraint_decl -> Libobject.obj =
 let do_constraint poly l =
   let u_of_id =
     let names, _ = Universes.global_universe_names () in
-      fun (loc, id) ->
-	try Idmap.find id names
-	with Not_found ->
-	  user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+    fun (loc, id) ->
+    try Idmap.find id names
+    with Not_found ->
+      user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+  in
+  let in_section = Lib.sections_are_opened () in
+  let () =
+    if poly && not in_section then
+      user_err_loc (Loc.ghost, "Constraint",
+                    str"Cannot declare polymorphic constraints outside sections")
+  in
+  let check_poly loc p loc' p' =
+    if poly then ()
+    else if p || p' then
+      let loc = if p then loc else loc' in
+      user_err_loc (loc, "Constraint",
+                    str "Cannot declare a global constraint on " ++
+                    str "a polymorphic universe, use "
+                    ++ str "Polymorphic Constraint instead")
   in
   let constraints = List.fold_left (fun acc (l, d, r) ->
-    let lu = u_of_id l and ru = u_of_id r in
-      Univ.Constraint.add (lu, d, ru) acc)
+     let p, lu = u_of_id l and p', ru = u_of_id r in
+     check_poly (fst l) p (fst r) p';
+     Univ.Constraint.add (lu, d, ru) acc)
     Univ.Constraint.empty l
   in
     Lib.add_anonymous_leaf (input_constraints (poly, constraints))
diff --git a/library/declare.mli b/library/declare.mli
index 8dd24d2780..7824506da0 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -34,14 +34,6 @@ val declare_variable : variable -> variable_declaration -> object_name
 
 type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
 
-(** [declare_constant id cd] declares a global declaration
-   (constant/parameter) with name [id] in the current section; it returns
-   the full path of the declaration 
-
-  internal specify if the constant has been created by the kernel or by the
-  user, and in the former case, if its errors should be silent
-   
-   *)
 type internal_flag =
   | UserAutomaticRequest
   | InternalTacticRequest
@@ -53,6 +45,12 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
   ?poly:polymorphic -> ?univs:Univ.universe_context ->
   ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
+(** [declare_constant id cd] declares a global declaration
+   (constant/parameter) with name [id] in the current section; it returns
+   the full path of the declaration
+
+  internal specify if the constant has been created by the kernel or by the
+  user, and in the former case, if its errors should be silent *)
 val declare_constant :
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index b3858146d2..b2806a1ac3 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Declarations
@@ -371,7 +371,7 @@ let rec replace_module_object idl mp0 objs0 mp1 objs1 =
   match idl, objs0 with
   | _,[] -> []
   | id::idl,(id',obj)::tail when Id.equal id id' ->
-    assert (object_has_tag obj "MODULE");
+    assert (String.equal (object_tag obj) "MODULE");
     let mp_id = MPdot(mp0, Label.of_id id) in
     let objs = match idl with
       | [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1
@@ -822,7 +822,7 @@ let protect_summaries f =
   try f fs
   with reraise ->
     (* Something wrong: undo the whole process *)
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     let () = Summary.unfreeze_summaries fs in
     iraise reraise
 
@@ -897,7 +897,13 @@ let start_library dir =
   Lib.start_compilation dir mp;
   Lib.add_frozen_state ()
 
+let end_library_hook = ref ignore
+let append_end_library_hook f =
+  let old_f = !end_library_hook in
+  end_library_hook := fun () -> old_f(); f ()
+
 let end_library ?except dir =
+  !end_library_hook();
   let oname = Lib.end_compilation_checks dir in
   let mp,cenv,ast = Global.export ?except dir in
   let prefix, lib_stack = Lib.end_compilation oname in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 2b440c087a..3917fe8d64 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -90,6 +90,9 @@ val end_library :
   ?except:Future.UUIDSet.t -> library_name ->
     Safe_typing.compiled_library * library_objects * Safe_typing.native_library
 
+(** append a function to be executed at end_library *)
+val append_end_library_hook : (unit -> unit) -> unit
+
 (** [really_import_module mp] opens the module [mp] (in a Caml sense).
    It modifies Nametab and performs the [open_object] function for
    every object of the module. Raises [Not_found] when [mp] is unknown
diff --git a/library/decls.ml b/library/decls.ml
index 0cd4ccb252..6e21880f1f 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -11,7 +11,6 @@
 
 open Util
 open Names
-open Context
 open Decl_kinds
 open Libnames
 
@@ -47,16 +46,20 @@ let constant_kind kn = Cmap.find kn !csttab
 
 (** Miscellaneous functions. *)
 
+open Context.Named.Declaration
+
 let initialize_named_context_for_proof () =
   let sign = Global.named_context () in
   List.fold_right
-    (fun (id,c,t as d) signv ->
-      let d = if variable_opacity id then (id,None,t) else d in
+    (fun d signv ->
+      let id = get_id d in
+      let d = if variable_opacity id then LocalAssum (id, get_type d) else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
 let last_section_hyps dir =
-  fold_named_context
-    (fun (id,_,_) sec_ids ->
+  Context.Named.fold_outside
+    (fun d sec_ids ->
+      let id = get_id d in
       try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids
       with Not_found -> sec_ids)
     (Environ.named_context (Global.env()))
diff --git a/library/global.ml b/library/global.ml
index 2398e92b03..e748434d24 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -42,7 +42,7 @@ let () =
 
 let assert_not_parsing () =
   if !Flags.we_are_parsing then
-    Errors.anomaly (
+    CErrors.anomaly (
       Pp.strbrk"The global environment cannot be accessed during parsing")
 
 let safe_env () = assert_not_parsing(); !global_env
@@ -84,6 +84,7 @@ let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 let push_context b c = globalize0 (Safe_typing.push_context b c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
+let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
 let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
 let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
@@ -244,6 +245,14 @@ let is_template_polymorphic r =
   | IndRef ind -> Environ.template_polymorphic_ind ind env
   | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env
 
+let is_type_in_type r =
+  let env = env() in
+  match r with
+  | VarRef id -> false
+  | ConstRef c -> Environ.type_in_type_constant c env
+  | IndRef ind -> Environ.type_in_type_ind ind env
+  | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env
+
 let current_dirpath () = 
   Safe_typing.current_dirpath (safe_env ())
 
diff --git a/library/global.mli b/library/global.mli
index 9db30c8ffc..247ca20b47 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -19,14 +19,15 @@ val env : unit -> Environ.env
 
 val env_is_initial : unit -> bool
 
-val universes : unit -> Univ.universes
+val universes : unit -> UGraph.t
 val named_context_val : unit -> Environ.named_context_val
-val named_context : unit -> Context.named_context
+val named_context : unit -> Context.Named.t
 
 (** {6 Enriching the global environment } *)
 
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
+val set_typing_flags : Declarations.typing_flags -> unit
 
 (** Variables, Local definitions, constants, inductive types *)
 
@@ -73,7 +74,7 @@ val add_module_parameter :
 
 (** {6 Queries in the global environment } *)
 
-val lookup_named     : variable -> Context.named_declaration
+val lookup_named     : variable -> Context.Named.Declaration.t
 val lookup_constant  : constant -> Declarations.constant_body
 val lookup_inductive : inductive ->
   Declarations.mutual_inductive_body * Declarations.one_inductive_body
@@ -116,6 +117,7 @@ val is_joined_environment : unit -> bool
 
 val is_polymorphic : Globnames.global_reference -> bool
 val is_template_polymorphic : Globnames.global_reference -> bool
+val is_type_in_type : Globnames.global_reference -> bool
 
 val type_of_global_in_context : Environ.env -> 
   Globnames.global_reference -> Constr.types Univ.in_universe_context
diff --git a/library/globnames.ml b/library/globnames.ml
index 3ae44b2cc9..a78f5f13a9 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Names
 open Term
 open Mod_subst
@@ -14,10 +14,10 @@ open Libnames
 
 (*s Global reference is a kernel side type for all references together *)
 type global_reference =
-  | VarRef of variable
-  | ConstRef of constant
-  | IndRef of inductive
-  | ConstructRef of constructor
+  | VarRef of variable           (** A reference to the section-context. *)
+  | ConstRef of constant         (** A reference to the environment. *)
+  | IndRef of inductive          (** A reference to an inductive type. *)
+  | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
 
 let isVarRef = function VarRef _ -> true | _ -> false
 let isConstRef = function ConstRef _ -> true | _ -> false
@@ -107,17 +107,16 @@ let global_eq_gen eq_cst eq_ind eq_cons x y =
 let global_ord_gen ord_cst ord_ind ord_cons x y =
   if x == y then 0
   else match x, y with
+  | VarRef v1, VarRef v2 -> Id.compare v1 v2
+  | VarRef _, _ -> -1
+  | _, VarRef _ -> 1
   | ConstRef cx, ConstRef cy -> ord_cst cx cy
+  | ConstRef _, _ -> -1
+  | _, ConstRef _ -> 1
   | IndRef indx, IndRef indy -> ord_ind indx indy
+  | IndRef _, _ -> -1
+  | _ , IndRef _ -> 1
   | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
-  | VarRef v1, VarRef v2 -> Id.compare v1 v2
-
-  | VarRef _, (ConstRef _ | IndRef _ | ConstructRef _) -> -1
-  | ConstRef _, VarRef _ -> 1
-  | ConstRef _, (IndRef _ | ConstructRef _) -> -1
-  | IndRef _, (VarRef _ | ConstRef _) -> 1
-  | IndRef _, ConstructRef _ -> -1
-  | ConstructRef _, (VarRef _ | ConstRef _ | IndRef _) -> 1
 
 let global_hash_gen hash_cst hash_ind hash_cons gr =
   let open Hashset.Combine in
diff --git a/library/globnames.mli b/library/globnames.mli
index f94f6216f4..f4956e3df2 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -13,10 +13,10 @@ open Mod_subst
 
 (** {6 Global reference is a kernel side type for all references together } *)
 type global_reference =
-  | VarRef of variable
-  | ConstRef of constant
-  | IndRef of inductive
-  | ConstructRef of constructor
+  | VarRef of variable           (** A reference to the section-context. *)
+  | ConstRef of constant         (** A reference to the environment. *)
+  | IndRef of inductive          (** A reference to an inductive type. *)
+  | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
 
 val isVarRef : global_reference -> bool
 val isConstRef : global_reference -> bool
diff --git a/library/goptions.ml b/library/goptions.ml
index 97da8a1eab..1cf25987b1 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -9,7 +9,7 @@
 (* This module manages customization parameters at the vernacular level     *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Libobject
 open Libnames
@@ -108,7 +108,8 @@ module MakeTable =
          (fun c -> t := MySet.remove c !t))
 
     let print_table table_name printer table =
-      pp (str table_name ++
+      Feedback.msg_notice
+        (str table_name ++
 	   (hov 0
 	      (if MySet.is_empty table then str " None" ++ fnl ()
                else MySet.fold
@@ -122,7 +123,7 @@ module MakeTable =
       method mem x =
 	let y = A.encode x in
         let answer = MySet.mem y !t in
-        msg_info (A.member_message y answer)
+        Feedback.msg_info (A.member_message y answer)
       method print = print_table A.title A.printer !t
     end
 
@@ -232,6 +233,11 @@ with Not_found ->
 open Libobject
 open Lib
 
+let warn_deprecated_option =
+  CWarnings.create ~name:"deprecated-option" ~category:"deprecated"
+         (fun key -> str "Option" ++ spc () ++ str (nickname key) ++
+                       strbrk " is deprecated")
+
 let declare_option cast uncast
   { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
@@ -269,10 +275,7 @@ let declare_option cast uncast
     begin fun v -> add_anonymous_leaf (gdecl_obj v) end
   else write,write,write
   in
-  let warn () =
-    if depr then
-      msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
-  in
+  let warn () = if depr then warn_deprecated_option key in
   let cread () = cast (read ()) in
   let cwrite v = warn (); write (uncast v) in
   let clwrite v = warn (); lwrite (uncast v) in
@@ -303,19 +306,22 @@ let declare_stringopt_option =
 
 (* Setting values of options *)
 
+let warn_unknown_option =
+  CWarnings.create ~name:"unknown-option" ~category:"option"
+                   (fun key -> strbrk "There is no option " ++
+                                 str (nickname key) ++ str ".")
+
 let set_option_value locality check_and_cast key v =
   let opt = try Some (get_option key) with Not_found -> None in
   match opt with
-  | None ->
-     msg_warning
-       (str "There is no option " ++ str (nickname key) ++ str ".")
+  | None -> warn_unknown_option key
   | Some (name, depr, (_,read,write,lwrite,gwrite)) ->
-     let write = match locality with
-       | None -> write
-       | Some true -> lwrite
-       | Some false -> gwrite
-     in
-     write (check_and_cast v (read ()))
+    let write = match locality with
+      | None -> write
+      | Some true -> lwrite
+      | Some false -> gwrite
+    in
+    write (check_and_cast v (read ()))
 
 let bad_type_error () = error "Bad type of value for this option."
 
@@ -359,8 +365,8 @@ let set_string_option_value = set_string_option_value_gen None
 
 let msg_option_value (name,v) =
   match v with
-    | BoolValue true  -> str "true"
-    | BoolValue false -> str "false"
+    | BoolValue true  -> str "on"
+    | BoolValue false -> str "off"
     | IntValue (Some n) -> int n
     | IntValue None   -> str "undefined"
     | StringValue s   -> str s
@@ -373,9 +379,9 @@ let print_option_value key =
   let s = read () in
   match s with
     | BoolValue b ->
-	msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
+	Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
     | _ ->
-	msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
+	Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
 
 let get_tables () =
   let tables = !value_tab in
diff --git a/library/heads.ml b/library/heads.ml
index 8124d3474f..02465f22fc 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -15,6 +15,7 @@ open Environ
 open Globnames
 open Libobject
 open Lib
+open Context.Named.Declaration
 
 (** Characterization of the head of a term *)
 
@@ -63,13 +64,13 @@ let kind_of_head env t =
       (try on_subterm k l b (variable_head id)
        with Not_found ->
         (* a goal variable *)
-        match pi2 (lookup_named id env) with
-        | Some c -> aux k l c b
-        | None -> NotImmediatelyComputableHead)
+        match lookup_named id env with
+        | LocalDef (_,c,_) -> aux k l c b
+        | LocalAssum _ -> NotImmediatelyComputableHead)
   | Const (cst,_) ->
       (try on_subterm k l b (constant_head cst)
        with Not_found ->
-         Errors.anomaly
+         CErrors.anomaly
            Pp.(str "constant not found in kind_of_head: " ++
                str (Names.Constant.to_string cst)))
   | Construct _ | CoFix _ ->
@@ -132,8 +133,8 @@ let compute_head = function
      | None -> RigidHead (RigidParameter cst)
      | Some c -> kind_of_head env c)
 | EvalVarRef id ->
-    (match pi2 (Global.lookup_named id) with
-     | Some c when not (Decls.variable_opacity id) ->
+    (match Global.lookup_named id with
+     | LocalDef (_,c,_) when not (Decls.variable_opacity id) ->
            kind_of_head (Global.env()) c
      | _ ->
            RigidHead (RigidVar id))
diff --git a/library/impargs.ml b/library/impargs.ml
index f5f6a3eba7..bce7a15cbe 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Globnames
@@ -68,15 +68,14 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
 let is_contextual_implicit_args () = !implicit_args.contextual
 let is_maximal_implicit_args () = !implicit_args.maximal
 
-let with_implicits flags f x =
+let with_implicit_protection f x =
   let oflags = !implicit_args in
   try
-    implicit_args := flags;
     let rslt = f x in
     implicit_args := oflags;
     rslt
   with reraise ->
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     let () = implicit_args := oflags in
     iraise reraise
 
@@ -165,6 +164,7 @@ let update pos rig (na,st) =
 
 (* modified is_rigid_reference with a truncated env *)
 let is_flexible_reference env bound depth f =
+  let open Context.Named.Declaration in
   match kind_of_term f with
     | Rel n when n >= bound+depth -> (* inductive type *) false
     | Rel n when n >= depth -> (* previous argument *) true
@@ -173,8 +173,7 @@ let is_flexible_reference env bound depth f =
         let cb = Environ.lookup_constant kn env in
 	(match cb.const_body with Def _ -> true | _ -> false)
     | Var id ->
-        let (_, value, _) = Environ.lookup_named id env in
-        begin match value with None -> false | _ -> true end
+        Environ.lookup_named id env |> is_local_def
     | Ind _ | Construct _ -> false
     |  _ -> true
 
@@ -188,7 +187,7 @@ let is_reversible_pattern bound depth f l =
 (* Precondition: rels in env are for inductive types only *)
 let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
   let rec frec rig (env,depth as ed) c =
-    let hd = if strict then whd_betadeltaiota env c else c in
+    let hd = if strict then whd_all env c else c in
     let c = if strongly_strict then hd else c in
     match kind_of_term hd with
     | Rel n when (n < bound+depth) && (n >= depth) ->
@@ -234,13 +233,14 @@ let find_displayed_name_in all avoid na (_,b as envnames_b) =
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rigid = ref true in
+  let open Context.Rel.Declaration in
   let rec aux env avoid n names t =
-    let t = whd_betadeltaiota env t in
+    let t = whd_all env t in
     match kind_of_term t with
       | Prod (na,a,b) ->
 	  let na',avoid' = find_displayed_name_in all avoid na (names,b) in
 	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
-            (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
+            (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b)
       | _ ->
 	  rigid := is_rigid_head t;
 	  let names = List.rev names in
@@ -249,10 +249,10 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
 	    add_free_rels_until strict strongly_strict revpat n env t Conclusion v
 	  else v
   in
-  match kind_of_term (whd_betadeltaiota env t) with
+  match kind_of_term (whd_all env t) with
     | Prod (na,a,b) ->
 	let na',avoid = find_displayed_name_in all [] na ([],b) in
-	let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
+	let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
 	!rigid, Array.to_list v
     | _ -> true, []
 
@@ -427,7 +427,7 @@ let compute_mib_implicits flags manual kn =
       (Array.mapi  (* No need to lift, arities contain no de Bruijn *)
         (fun i mip ->
 	  (** No need to care about constraints here *)
-	  (Name mip.mind_typename, None, Global.type_of_global_unsafe (IndRef (kn,i))))
+	  Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, Global.type_of_global_unsafe (IndRef (kn,i))))
         mib.mind_packets) in
   let env_ar = push_rel_context ar env in
   let imps_one_inductive i mip =
@@ -449,8 +449,8 @@ let compute_all_mib_implicits flags manual kn =
 
 let compute_var_implicits flags manual id =
   let env = Global.env () in
-  let (_,_,ty) = lookup_named id env in
-  compute_semi_auto_implicits env flags manual ty
+  let open Context.Named.Declaration in
+  compute_semi_auto_implicits env flags manual (get_type (lookup_named id env))
 
 (* Implicits of a global reference. *)
 
@@ -525,12 +525,6 @@ let impls_of_context ctx =
   in
   List.rev_map map (List.filter is_set ctx)
 
-let section_segment_of_reference = function
-  | ConstRef con -> pi1 (section_segment_of_constant con)
-  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-    pi1 (section_segment_of_mutual_inductive kn)
-  | _ -> []
-
 let adjust_side_condition p = function
   | LessArgsThan n -> LessArgsThan (n+p)
   | DefaultImpArgs -> DefaultImpArgs
@@ -544,7 +538,7 @@ let discharge_implicits (_,(req,l)) =
   | ImplLocal -> None
   | ImplInteractive (ref,flags,exp) ->
     (try
-      let vars = section_segment_of_reference ref in
+      let vars = variable_section_segment_of_reference ref in
       let ref' = if isVarRef ref then ref else pop_global_reference ref in
       let extra_impls = impls_of_context vars in
       let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
@@ -562,7 +556,7 @@ let discharge_implicits (_,(req,l)) =
   | ImplMutualInductive (kn,flags) ->
     (try
       let l' = List.map (fun (gr, l) ->
-	let vars = section_segment_of_reference gr in
+	let vars = variable_section_segment_of_reference gr in
 	let extra_impls = impls_of_context vars in
 	((if isVarRef gr then gr else pop_global_reference gr),
 	 List.map (add_section_impls vars extra_impls) l)) l
diff --git a/library/impargs.mli b/library/impargs.mli
index 34e529ca2c..3919a519c9 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -29,8 +29,7 @@ val is_reversible_pattern_implicit_args : unit -> bool
 val is_contextual_implicit_args : unit -> bool
 val is_maximal_implicit_args : unit -> bool
 
-type implicits_flags
-val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
+val with_implicit_protection : ('a -> 'b) -> 'a -> 'b
 
 (** {6 ... } *)
 (** An [implicits_list] is a list of positions telling which arguments
@@ -136,14 +135,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list
 
 val select_stronger_impargs : implicits_list list -> implicit_status list
 
-type implicit_interactive_request
-
-type implicit_discharge_request =
-  | ImplLocal
-  | ImplConstant of constant * implicits_flags
-  | ImplMutualInductive of mutual_inductive * implicits_flags
-  | ImplInteractive of global_reference * implicits_flags *
-      implicit_interactive_request
-
 val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
 (** Equality on [explicitation]. *)
diff --git a/library/keys.ml b/library/keys.ml
index 0c167494ee..057dc3b65d 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -12,35 +12,31 @@ open Globnames
 open Term
 open Libobject
 
-type key = 
+type key =
   | KGlob of global_reference
-  | KLam 
+  | KLam
   | KLet
   | KProd
   | KSort
-  | KEvar
-  | KCase 
-  | KFix 
+  | KCase
+  | KFix
   | KCoFix
-  | KRel 
-  | KMeta
+  | KRel
 
 module KeyOrdered = struct
   type t = key
 
   let hash gr =
     match gr with
-    | KGlob gr -> 10 + RefOrdered.hash gr
+    | KGlob gr -> 8 + RefOrdered.hash gr
     | KLam -> 0
     | KLet -> 1
     | KProd -> 2
     | KSort -> 3
-    | KEvar -> 4
-    | KCase -> 5
-    | KFix -> 6
-    | KCoFix -> 7
-    | KRel -> 8
-    | KMeta -> 9
+    | KCase -> 4
+    | KFix -> 5
+    | KCoFix -> 6
+    | KRel -> 7
 
   let compare gr1 gr2 =
     match gr1, gr2 with
@@ -62,8 +58,6 @@ module Keyset = Keymap.Set
 
 (* Mapping structure for references to be considered equivalent *)
 
-type keys = Keyset.t Keymap.t
-
 let keys = Summary.ref Keymap.empty ~name:"Keys_decl"
 
 let add_kv k v m =
@@ -153,12 +147,10 @@ let pr_key pr_global = function
   | KLet -> str"Let"
   | KProd -> str"Product"
   | KSort -> str"Sort"
-  | KEvar -> str"Evar"
   | KCase -> str"Case"
   | KFix -> str"Fix"
   | KCoFix -> str"CoFix"
   | KRel -> str"Rel"
-  | KMeta -> str"Meta"
 
 let pr_keyset pr_global v = 
   prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)
diff --git a/library/kindops.ml b/library/kindops.ml
index c634193da8..21b1bec33c 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -25,7 +25,7 @@ let string_of_theorem_kind = function
 
 let string_of_definition_kind def =
   let (locality, poly, kind) = def in
-  let error () = Errors.anomaly (Pp.str "Internal definition kind") in
+  let error () = CErrors.anomaly (Pp.str "Internal definition kind") in
   match kind with
   | Definition ->
     begin match locality with
@@ -64,4 +64,4 @@ let string_of_definition_kind def =
     | Global -> "Global Instance"
     end
   | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
-    Errors.anomaly (Pp.str "Internal definition kind")
+    CErrors.anomaly (Pp.str "Internal definition kind")
diff --git a/library/lib.ml b/library/lib.ml
index f6b4a2458b..8880a8b154 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Libnames
 open Globnames
@@ -428,8 +428,10 @@ let add_section_context ctx =
        sectab := (Context ctx :: vars,repl,abs)::sl
 
 let extract_hyps (secs,ohyps) =
+  let open Context.Named.Declaration in
   let rec aux = function
-    | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
+    | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) ->
+      let (id',b,t) = to_tuple decl in
       let l, r = aux (idl,hyps) in 
 	(id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
     | (Variable (_,_,poly,ctx)::idl,hyps) ->
@@ -448,7 +450,10 @@ let instance_from_variable_context sign =
     | [] -> [] in
   Array.of_list (inst_rec sign)
 
-let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx
+let named_of_variable_context ctx = let open Context.Named.Declaration in
+                                    List.map (function id,_,None,t -> LocalAssum (id,t)
+                                                     | id,_,Some b,t -> LocalDef (id,b,t))
+                                             ctx
   
 let add_section_replacement f g poly hyps =
   match !sectab with
@@ -478,6 +483,12 @@ let section_segment_of_constant con =
 let section_segment_of_mutual_inductive kn =
   Names.Mindmap.find kn (snd (pi3 (List.hd !sectab)))
 
+let variable_section_segment_of_reference = function
+  | ConstRef con -> pi1 (section_segment_of_constant con)
+  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+      pi1 (section_segment_of_mutual_inductive kn)
+  | _ -> []
+                     
 let section_instance = function
   | VarRef id ->
      let eq = function
diff --git a/library/lib.mli b/library/lib.mli
index 513c48549e..7080b5dba7 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -168,20 +168,21 @@ type variable_context = variable_info list
 type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
 
 val instance_from_variable_context : variable_context -> Names.Id.t array
-val named_of_variable_context : variable_context -> Context.named_context
+val named_of_variable_context : variable_context -> Context.Named.t
 
 val section_segment_of_constant : Names.constant -> abstr_info
 val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info
-
+val variable_section_segment_of_reference : Globnames.global_reference -> variable_context
+                                                                                                     
 val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array
 val is_in_section : Globnames.global_reference -> bool
 
 val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit
 val add_section_context : Univ.universe_context_set -> unit
 val add_section_constant : Decl_kinds.polymorphic ->
-  Names.constant -> Context.named_context -> unit
+  Names.constant -> Context.Named.t -> unit
 val add_section_kn : Decl_kinds.polymorphic ->
-  Names.mutual_inductive -> Context.named_context -> unit
+  Names.mutual_inductive -> Context.Named.t -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 (** {6 Discharge: decrease the section level if in the current section } *)
@@ -194,6 +195,6 @@ val discharge_inductive : Names.inductive -> Names.inductive
 (* discharging a constant in one go *)
 val full_replacement_context : unit -> Opaqueproof.work_list list
 val full_section_segment_of_constant :
-  Names.constant -> (Context.named_context -> Context.named_context) list
+  Names.constant -> (Context.Named.t -> Context.Named.t) list
 
 
diff --git a/library/libnames.ml b/library/libnames.ml
index a2f22b2ef7..dd74e192ff 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -7,13 +7,13 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 
 (**********************************************)
 
-let pr_dirpath sl = (str (DirPath.to_string sl))
+let pr_dirpath sl = str (DirPath.to_string sl)
 
 (*s Operations on dirpaths *)
 
@@ -197,7 +197,7 @@ let string_of_reference = function
 
 let pr_reference = function
   | Qualid (_,qid) -> pr_qualid qid
-  | Ident (_,id) -> str (Id.to_string id)
+  | Ident (_,id) -> Id.print id
 
 let loc_of_reference = function
   | Qualid (loc,qid) -> loc
diff --git a/library/libobject.ml b/library/libobject.ml
index 706e399159..caa03c85be 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -8,18 +8,9 @@
 
 open Libnames
 open Pp
+open Util
 
-(* The relax flag is used to make it possible to load files while ignoring
-   failures to incorporate some objects.  This can be useful when one
-   wants to work with restricted Coq programs that have only parts of
-   the full capabilities, but may still be able to work correctly for
-   limited purposes.  One example is for the graphical interface, that uses
-   such a limited Coq process to do only parsing.  It loads .vo files, but
-   is only interested in loading the grammar rule definitions. *)
-
-let relax_flag = ref false;;
-
-let relax b = relax_flag := b;;
+module Dyn = Dyn.Make(struct end)
 
 type 'a substitutivity =
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
@@ -40,7 +31,7 @@ let default_object s = {
   load_function = (fun _ _ -> ());
   open_function = (fun _ _ -> ());
   subst_function = (fun _ ->
-    Errors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
+    CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
   classify_function = (fun obj -> Keep obj);
   discharge_function = (fun _ -> None);
   rebuild_function = (fun x -> x)}
@@ -70,15 +61,14 @@ type dynamic_object_declaration = {
   dyn_discharge_function : object_name * obj -> obj option;
   dyn_rebuild_function : obj -> obj }
 
-let object_tag = Dyn.tag
-let object_has_tag = Dyn.has_tag
+let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t
 
 let cache_tab =
   (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
 
 let declare_object_full odecl =
   let na = odecl.object_name in
-  let (infun,outfun) = Dyn.create na in
+  let (infun, outfun) = Dyn.Easy.make_dyn na in
   let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj)
   and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj)
   and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj)
@@ -107,36 +97,21 @@ let declare_object_full odecl =
 
 let declare_object odecl =
   try fst (declare_object_full odecl)
-  with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
+  with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
 let declare_object_full odecl =
   try declare_object_full odecl
-  with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
-
-let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t)
+  with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
 
 (* this function describes how the cache, load, open, and export functions
-   are triggered.  In relaxed mode, this function just return a meaningless
-   value instead of raising an exception when they fail. *)
+   are triggered. *)
 
 let apply_dyn_fun deflt f lobj =
   let tag = object_tag lobj in
-  try
-    let dodecl =
-      try
-        Hashtbl.find cache_tab tag
-      with Not_found ->
-        failwith "local to_apply_dyn_fun" in
-    f dodecl
-  with
-    Failure "local to_apply_dyn_fun" ->
-      if not (!relax_flag || Hashtbl.mem missing_tab tag) then
-        begin
-          Pp.msg_warning
-	    (Pp.str ("Cannot find library functions for an object with tag "
-                      ^ tag ^ " (a plugin may be missing)"));
-          Hashtbl.add missing_tab tag ()
-        end;
-      deflt
+  let dodecl =
+    try Hashtbl.find cache_tab tag
+    with Not_found -> assert false
+  in
+  f dodecl
 
 let cache_object ((_,lobj) as node) =
   apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj
@@ -158,3 +133,5 @@ let discharge_object ((_,lobj) as node) =
 
 let rebuild_object lobj =
   apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj
+
+let dump = Dyn.dump
diff --git a/library/libobject.mli b/library/libobject.mli
index f3880a437e..51b9af059f 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -99,7 +99,6 @@ val declare_object :
   'a object_declaration -> ('a -> obj)
 
 val object_tag : obj -> string
-val object_has_tag : obj -> string -> bool
 
 val cache_object : object_name * obj -> unit
 val load_object : int -> object_name * obj -> unit
@@ -108,4 +107,7 @@ val subst_object : substitution * obj -> obj
 val classify_object : obj -> obj substitutivity
 val discharge_object : object_name * obj -> obj option
 val rebuild_object : obj -> obj
-val relax : bool -> unit
+
+(** {6 Debug} *)
+
+val dump : unit -> (int * string) list
diff --git a/library/library.ml b/library/library.ml
index e34d38d153..d44f796a7a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 
 open Names
@@ -64,7 +64,7 @@ let fetch_delayed del =
     let () = close_in ch in
     if not (String.equal digest digest') then raise (Faulty f);
     obj
-  with e when Errors.noncritical e -> raise (Faulty f)
+  with e when CErrors.noncritical e -> raise (Faulty f)
 
 end
 
@@ -132,7 +132,7 @@ let try_find_library dir =
   try find_library dir
   with Not_found ->
     errorlabstrm "Library.find_library"
-      (str "Unknown library " ++ str (DirPath.to_string dir))
+      (str "Unknown library " ++ pr_dirpath dir)
 
 let register_library_filename dir f =
   (* Not synchronized: overwrite the previous binding if one existed *)
@@ -271,6 +271,12 @@ exception LibUnmappedDir
 exception LibNotFound
 type library_location = LibLoaded | LibInPath
 
+let warn_several_object_files =
+  CWarnings.create ~name:"several-object-files" ~category:"require"
+         (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++
+                            strbrk " instead of " ++ str vo ++
+                            strbrk " because it is more recent")
+
 let locate_absolute_library dir =
   (* Search in loadpath *)
   let pref, base = split_dirpath dir in
@@ -285,28 +291,17 @@ let locate_absolute_library dir =
     with Not_found -> [] in
   match find ".vo" @ find ".vio" with
   | [] -> raise LibNotFound
-  | [file] -> dir, file
+  | [file] -> file
   | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
-       msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
-         str vo ++ str " because it is more recent");
-       dir, vi
-  | [vo;vi] -> dir, vo
+    warn_several_object_files (vi, vo);
+    vi
+  | [vo;vi] -> vo
   | _ -> assert false
 
 let locate_qualified_library ?root ?(warn = true) qid =
   (* Search library in loadpath *)
   let dir, base = repr_qualid qid in
-  let loadpath = match root with
-  | None -> Loadpath.expand_path dir
-  | Some root ->
-    let filter path =
-      if is_dirpath_prefix_of root path then
-        let path = drop_dirpath_prefix root path in
-        is_dirpath_suffix_of dir path
-      else false
-    in
-    Loadpath.filter_path filter
-  in
+  let loadpath = Loadpath.expand_path ?root dir in
   let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
   let find ext =
     try
@@ -321,8 +316,7 @@ let locate_qualified_library ?root ?(warn = true) qid =
     | [lpath, file] -> lpath, file
     | [lpath_vo, vo; lpath_vi, vi]
       when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
-       msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
-         str vo ++ str " because it is more recent");
+      warn_several_object_files (vi, vo);
        lpath_vi, vi
     | [lpath_vo, vo; _ ] -> lpath_vo, vo
     | _ -> assert false
@@ -380,7 +374,7 @@ let access_table what tables dp i =
     | Fetched t -> t
     | ToFetch f ->
       let dir_path = Names.DirPath.to_string dp in
-      Flags.if_verbose msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
+      Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
       let t =
         try fetch_delayed f
         with Faulty f ->
@@ -458,35 +452,38 @@ let intern_from_file f =
 module DPMap = Map.Make(DirPath)
 
 let rec intern_library (needed, contents) (dir, f) from =
-  Pp.feedback(Feedback.FileDependency (from, f));
   (* Look if in the current logical environment *)
   try (find_library dir).libsum_digests, (needed, contents)
   with Not_found ->
   (* Look if already listed and consequently its dependencies too *)
   try (DPMap.find dir contents).library_digests, (needed, contents)
   with Not_found ->
+  Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
   (* [dir] is an absolute name which matches [f] which must be in loadpath *)
+  let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
   let m = intern_from_file f in
   if not (DirPath.equal dir m.library_name) then
     errorlabstrm "load_physical_library"
       (str "The file " ++ str f ++ str " contains library" ++ spc () ++
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
        spc() ++ pr_dirpath dir);
-  Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f));
-  m.library_digests, intern_library_deps (needed, contents) dir m (Some f)
+  Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
+  m.library_digests, intern_library_deps (needed, contents) dir m f
 
 and intern_library_deps libs dir m from =
   let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in
   (dir :: needed, DPMap.add dir m contents )
 
 and intern_mandatory_library caller from libs (dir,d) =
-  let digest, libs = intern_library libs (try_locate_absolute_library dir) from in
+  let digest, libs = intern_library libs (dir, None) (Some from) in
   if not (Safe_typing.digest_match ~actual:digest ~required:d) then
-    errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir));
+    errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++
+    str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
+    over library " ++ pr_dirpath dir);
   libs
 
-let rec_intern_library libs mref =
-  let _, libs = intern_library libs mref None in
+let rec_intern_library libs (dir, f) =
+  let _, libs = intern_library libs (dir, Some f) None in
   libs
 
 let native_name_from_filename f =
@@ -556,12 +553,20 @@ let in_require : require_obj -> obj =
 
 let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
 
+let warn_require_in_module =
+  CWarnings.create ~name:"require-in-module" ~category:"deprecated"
+                   (fun () -> strbrk "Require inside a module is" ++
+                              strbrk " deprecated and strongly discouraged. " ++
+                              strbrk "You can Require a module at toplevel " ++
+                              strbrk "and optionally Import it inside another one.")
+
 let require_library_from_dirpath modrefl export =
   let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in
   let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
   let modrefl = List.map fst modrefl in
     if Lib.is_module_or_modtype () then
       begin
+        warn_require_in_module ();
 	add_anonymous_leaf (in_require (needed,modrefl,None));
 	Option.iter (fun exp ->
 	  add_anonymous_leaf (in_import_library (modrefl,exp)))
@@ -578,7 +583,7 @@ let safe_locate_module (loc,qid) =
   try Nametab.locate_module qid
   with Not_found ->
     user_err_loc
-      (loc,"import_library", str (string_of_qualid qid) ++ str " is not a module")
+      (loc,"import_library", pr_qualid qid ++ str " is not a module")
 
 let import_module export modl =
   (* Optimization: libraries in a raw in the list are imported
@@ -603,7 +608,7 @@ let import_module export modl =
             try Declaremods.import_module export mp; aux [] l
             with Not_found ->
               user_err_loc (loc,"import_library",
-                str (string_of_qualid dir) ++ str " is not a module"))
+                pr_qualid dir ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
 
@@ -613,9 +618,9 @@ let import_module export modl =
 let check_coq_overwriting p id =
   let l = DirPath.repr p in
   let is_empty = match l with [] -> true | _ -> false in
-  if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then
+  if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then
     errorlabstrm ""
-      (str "Cannot build module " ++ str (DirPath.to_string p) ++ str "." ++ pr_id id ++ str "." ++ spc () ++
+      (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++
       str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
 
 (* Verifies that a string starts by a letter and do not contain
@@ -637,17 +642,14 @@ let check_module_name s =
         done
     | c -> err c
 
-let start_library f =
-  let () = if not (Sys.file_exists f) then
-    errorlabstrm "" (hov 0 (str "Can't find file" ++ spc () ++ str f))
-  in
+let start_library fo =
   let ldir0 =
     try
-      let lp = Loadpath.find_load_path (Filename.dirname f) in
+      let lp = Loadpath.find_load_path (Filename.dirname fo) in
       Loadpath.logical lp
     with Not_found -> Nameops.default_root_prefix
   in
-  let file = Filename.chop_extension (Filename.basename f) in
+  let file = Filename.chop_extension (Filename.basename fo) in
   let id = Id.of_string file in
   check_module_name file;
   check_coq_overwriting ldir0 id;
@@ -702,12 +704,13 @@ let error_recursively_dependent_library dir =
    writing the content and computing the checksum... *)
 
 let save_library_to ?todo dir f otab =
-  let f, except = match todo with
+  let except = match todo with
     | None ->
         assert(!Flags.compilation_mode = Flags.BuildVo);
-        f ^ "o", Future.UUIDSet.empty
+        assert(Filename.check_suffix f ".vo");
+        Future.UUIDSet.empty
     | Some (l,_) ->
-        f ^ "io",
+        assert(Filename.check_suffix f ".vio");
         List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
           Future.UUIDSet.empty l in
   let cenv, seg, ast = Declaremods.end_library ~except dir in
@@ -731,7 +734,7 @@ let save_library_to ?todo dir f otab =
       except Int.Set.empty in
   let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
   Array.iteri (fun i x ->
-    if not(is_done_or_todo i x) then Errors.errorlabstrm "library"
+    if not(is_done_or_todo i x) then CErrors.errorlabstrm "library"
       Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
     opaque_table;
   let sd = {
@@ -763,8 +766,8 @@ let save_library_to ?todo dir f otab =
       if not (Nativelib.compile_library dir ast fn) then
 	error "Could not compile the library to native code."
    with reraise ->
-    let reraise = Errors.push reraise in
-    let () = msg_warning (str "Removed file " ++ str f') in
+    let reraise = CErrors.push reraise in
+    let () = Feedback.msg_warning (str "Removed file " ++ str f') in
     let () = close_out ch in
     let () = Sys.remove f' in
     iraise reraise
@@ -780,13 +783,6 @@ let save_library_raw f sum lib univs proofs =
   System.marshal_out_segment f' ch (proofs     : seg_proofs);
   close_out ch
 
-(************************************************************************)
-(*s Display the memory use of a library. *)
-
-open Printf
-
-let mem s = Pp.mt ()
-
 module StringOrd = struct type t = string let compare = String.compare end
 module StringSet = Set.Make(StringOrd)
 
diff --git a/library/library.mli b/library/library.mli
index 25c9604ceb..b9044b60dd 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -37,9 +37,9 @@ type seg_proofs = Term.constr Future.computation array
    an export otherwise just a simple import *)
 val import_module : bool -> qualid located list -> unit
 
-(** Start the compilation of a file as a library. The argument must be an
-    existing file on the system, and the returned path is the associated
-    absolute logical path of the library. *)
+(** Start the compilation of a file as a library. The first argument must be
+    output file, and the 
+    returned path is the associated absolute logical path of the library. *)
 val start_library : CUnix.physical_path -> DirPath.t
 
 (** End the compilation of a library and save it to a ".vo" file *)
@@ -85,8 +85,5 @@ val locate_qualified_library :
 
 *)
 
-(** {6 Statistics: display the memory use of a library. } *)
-val mem : DirPath.t -> Pp.std_ppcmds
-
 (** {6 Native compiler. } *)
 val native_name_from_filename : string -> string
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 78f8dd25f3..e6f6716c3d 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -8,7 +8,7 @@
 
 open Pp
 open Util
-open Errors
+open CErrors
 open Names
 open Libnames
 
@@ -50,6 +50,13 @@ let remove_load_path dir =
   let filter p = not (String.equal p.path_physical dir) in
   load_paths := List.filter filter !load_paths
 
+let warn_overriding_logical_loadpath =
+  CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath"
+         (fun (phys_path, old_path, coq_path) ->
+          str phys_path ++ strbrk " was previously bound to " ++
+            pr_dirpath old_path ++ strbrk "; it is remapped to " ++
+            pr_dirpath coq_path)
+
 let add_load_path phys_path coq_path ~implicit =
   let phys_path = CUnix.canonical_path_name phys_path in
   let filter p = String.equal p.path_physical phys_path in
@@ -72,10 +79,8 @@ let add_load_path phys_path coq_path ~implicit =
         let () =
           (* Do not warn when overriding the default "-I ." path *)
           if not (DirPath.equal old_path Nameops.default_root_prefix) then
-            msg_warning
-              (str phys_path ++ strbrk " was previously bound to " ++
-                 pr_dirpath old_path ++ strbrk "; it is remapped to " ++
-                 pr_dirpath coq_path) in
+          warn_overriding_logical_loadpath (phys_path, old_path, coq_path)
+        in
         true in
     if replace then
       begin
@@ -84,10 +89,6 @@ let add_load_path phys_path coq_path ~implicit =
       end
   | _ -> anomaly_too_many_paths phys_path
 
-let extend_path_with_dirpath p dir =
-  List.fold_left Filename.concat p
-    (List.rev_map Id.to_string (DirPath.repr dir))
-
 let filter_path f =
   let rec aux = function
   | [] -> []
@@ -97,18 +98,19 @@ let filter_path f =
   in
   aux !load_paths
 
-let expand_path dir =
+let expand_path ?root dir =
   let rec aux = function
   | [] -> []
-  | { path_physical = ph; path_logical = lg; path_implicit = implicit }  :: l ->
-    match implicit with
-    | true ->
-      (** The path is implicit, so that we only want match the logical suffix *)
-      if is_dirpath_suffix_of dir lg then (ph, lg) :: aux l else aux l
-    | false ->
-      (** Otherwise we must match exactly *)
-      if DirPath.equal dir lg then (ph, lg) :: aux l else aux l
-  in
+  | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l ->
+    let success =
+      match root with
+      | None ->
+        if implicit then is_dirpath_suffix_of dir lg
+        else DirPath.equal dir lg
+      | Some root ->
+        is_dirpath_prefix_of root lg &&
+          is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in
+    if success then (ph, lg) :: aux l else aux l in
   aux !load_paths
 
 let locate_file fname =
diff --git a/library/loadpath.mli b/library/loadpath.mli
index 49ffc11480..4e79edbdcf 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -42,7 +42,7 @@ val find_load_path : CUnix.physical_path -> t
 val is_in_load_paths : CUnix.physical_path -> bool
 (** Whether a physical path is currently bound. *)
 
-val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list
+val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list
 (** Given a relative logical path, associate the list of absolute physical and
     logical paths which are possible matches of it. *)
 
diff --git a/library/nameops.ml b/library/nameops.ml
index 98b417c2a9..71405d0240 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -12,7 +12,7 @@ open Names
 
 (* Identifiers *)
 
-let pr_id id = str (Id.to_string id)
+let pr_id id = Id.print id
 
 let pr_name = function
   | Anonymous -> str "_"
@@ -141,7 +141,7 @@ let name_max na1 na2 =
   | Name _ -> na1
   | Anonymous -> na2
 
-let pr_lab l = str (Label.to_string l)
+let pr_lab l = Label.print l
 
 let default_library = Names.DirPath.initial (* = ["Top"] *)
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 40acb3ae2d..fa5db37ed5 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
@@ -82,6 +82,14 @@ module Make (U : UserName) (E : EqualityType) : NAMETREE
 struct
   type elt = E.t
 
+  (* A name became inaccessible, even with absolute qualification.
+     Example:
+     Module F (X : S). Module X.
+     The argument X of the functor F is masked by the inner module X.
+   *)
+  let masking_absolute n =
+    Flags.if_verbose Feedback.msg_info (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!"))
+
   type user_name = U.t
 
   type path_status =
@@ -119,9 +127,7 @@ struct
 	      | Absolute (n,_) ->
 		  (* This is an absolute name, we must keep it
 		     otherwise it may become unaccessible forever *)
-		    msg_warning (str ("Trying to mask the absolute name \""
-			     ^ U.to_string n ^ "\"!"));
-		  tree.path
+                masking_absolute n; tree.path
 	      | Nothing
 	      | Relative _ -> Relative (uname,o)
           else tree.path
@@ -144,7 +150,6 @@ struct
 	  | Nothing
 	  | Relative _ -> mktree (Absolute (uname,o)) tree.map
 
-
 let rec push_exactly uname o level tree = function
 | [] ->
   anomaly (Pp.str "Prefix longer than path! Impossible!")
@@ -155,9 +160,7 @@ let rec push_exactly uname o level tree = function
         | Absolute (n,_) ->
             (* This is an absolute name, we must keep it
                 otherwise it may become unaccessible forever *)
-              msg_warning (str ("Trying to mask the absolute name \""
-                        ^ U.to_string n ^ "\"!"));
-            tree.path
+            masking_absolute n; tree.path
         | Nothing
         | Relative _ -> Relative (uname,o)
     in
@@ -523,9 +526,9 @@ let shortest_qualid_of_tactic kn =
     KnTab.shortest_qualid Id.Set.empty sp !the_tactictab
 
 let pr_global_env env ref =
-  try str (string_of_qualid (shortest_qualid_of_global env ref))
+  try pr_qualid (shortest_qualid_of_global env ref)
   with Not_found as e ->
-    if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e
+    if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
 
 let global_inductive r =
   match global r with
diff --git a/library/states.ml b/library/states.ml
index 2e1be764ab..95bd819d66 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -35,7 +35,7 @@ let with_state_protection f x =
   try
     let a = f x in unfreeze st; a
   with reraise ->
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     (unfreeze st; iraise reraise)
 
 let with_state_protection_on_exception = Future.transactify
diff --git a/library/summary.ml b/library/summary.ml
index 46c52acc4c..6efa07f388 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -7,9 +7,11 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 
+module Dyn = Dyn.Make(struct end)
+
 type marshallable = [ `Yes | `No | `Shallow ]
 type 'a summary_declaration = {
   freeze_function : marshallable -> 'a;
@@ -21,7 +23,7 @@ let summaries = ref Int.Map.empty
 let mangle id = id ^ "-SUMMARY"
 
 let internal_declare_summary hash sumname sdecl =
-  let (infun, outfun) = Dyn.create (mangle sumname) in
+  let (infun, outfun) = Dyn.Easy.make_dyn (mangle sumname) in
   let dyn_freeze b = infun (sdecl.freeze_function b)
   and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
   and dyn_init = sdecl.init_function in
@@ -103,10 +105,10 @@ let unfreeze_summaries fs =
   in
   let fold id decl state =
     try fold id decl state
-    with e when Errors.noncritical e ->
-      let e = Errors.push e in
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in
       Printf.eprintf "Error unfrezing summay %s\n%s\n%!"
-        (name_of_summary id) (Pp.string_of_ppcmds (Errors.iprint e));
+        (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e));
       iraise e
   in
   (** We rely on the order of the frozen list, and the order of folding *)
@@ -147,7 +149,7 @@ let unfreeze_summary datas =
       let (name, summary) = Int.Map.find id !summaries in
       try summary.unfreeze_function data
       with e ->
-        let e = Errors.push e in
+        let e = CErrors.push e in
         prerr_endline ("Exception unfreezing " ^ name);
         iraise e)
   datas
@@ -164,8 +166,15 @@ let project_summary { summaries; ml_module } ?(complement=false) ids =
   List.filter (fun (id, _) -> List.mem id ids) summaries
 
 let pointer_equal l1 l2 =
+  let ptr_equal d1 d2 =
+    let Dyn.Dyn (t1, x1) = d1 in
+    let Dyn.Dyn (t2, x2) = d2 in
+    match Dyn.eq t1 t2 with
+    | None -> false
+    | Some Refl -> x1 == x2
+    in
   CList.for_all2eq
-    (fun (id1,v1) (id2,v2) -> id1 = id2 && Dyn.pointer_equal v1 v2) l1 l2
+    (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2
 
 (** All-in-one reference declaration + registration *)
 
@@ -176,3 +185,30 @@ let ref ?(freeze=fun _ r -> r) ~name x =
       unfreeze_function = ((:=) r);
       init_function = (fun () -> r := x) };
   r
+
+module Local = struct
+
+type 'a local_ref = ('a CEphemeron.key * string) ref
+
+let (:=) r v = r := (CEphemeron.create v, snd !r)
+
+let (!) r =
+  let key, name = !r in
+  try CEphemeron.get key
+  with CEphemeron.InvalidKey ->
+    let _, { init_function } =
+      Int.Map.find (String.hash (mangle name)) !summaries in
+    init_function ();
+    CEphemeron.get (fst !r)
+
+let ref ?(freeze=fun x -> x) ~name init =
+  let r = Pervasives.ref (CEphemeron.create init, name) in
+  declare_summary name
+    { freeze_function = (fun _ -> freeze !r);
+      unfreeze_function = ((:=) r);
+      init_function = (fun () -> r := init) };
+  r
+
+end
+
+let dump = Dyn.dump
diff --git a/library/summary.mli b/library/summary.mli
index c24a0b4b89..1b57613cb7 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -42,6 +42,17 @@ val declare_summary : string -> 'a summary_declaration -> unit
 
 val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
 
+(* As [ref] but the value is local to a process, i.e. not sent to, say, proof
+ * workers.  It is useful to implement a local cache for example. *)
+module Local : sig
+
+  type 'a local_ref
+  val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref
+  val (:=) : 'a local_ref -> 'a -> unit
+  val (!) : 'a local_ref -> 'a
+
+end
+
 (** Special name for the summary of ML modules.  This summary entry is
     special because its unfreeze may load ML code and hence add summary
     entries.  Thus is has to be recognizable, and handled appropriately *)
@@ -71,3 +82,7 @@ val unfreeze_summary : frozen_bits -> unit
 val surgery_summary : frozen -> frozen_bits -> frozen
 val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits
 val pointer_equal : frozen_bits -> frozen_bits -> bool
+
+(** {6 Debug} *)
+
+val dump : unit -> (int * string) list
diff --git a/library/universes.ml b/library/universes.ml
index 3bebdafc78..db95607f18 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -13,10 +13,11 @@ open Term
 open Environ
 open Univ
 open Globnames
+open Decl_kinds
 
 (** Global universe names *)
 type universe_names = 
-    Univ.universe_level Idmap.t * Id.t Univ.LMap.t
+  (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
 
 let global_universes =
   Summary.ref ~name:"Global universe names"
@@ -102,6 +103,7 @@ module Constraints = struct
 end
 
 type universe_constraints = Constraints.t
+type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option
 type 'a universe_constrained = 'a * universe_constraints
 
 type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
@@ -110,7 +112,7 @@ let enforce_eq_instances_univs strict x y c =
   let d = if strict then ULub else UEq in
   let ax = Instance.to_array x and ay = Instance.to_array y in
     if Array.length ax != Array.length ay then
-      Errors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
+      CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
 	       Pp.str " instances of different lengths");
     CArray.fold_right2
       (fun x y -> Constraints.add (Universe.make x, d, Universe.make y))
@@ -135,82 +137,76 @@ let to_constraints g s =
       | _, ULe, Some l' -> enforce_leq x y acc
       | _, ULub, _ -> acc
       | _, d, _ -> 
-	let f = if d == ULe then check_leq else check_eq in
+	let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in
 	  if f g x y then acc else 
 	    raise (Invalid_argument 
 		   "to_constraints: non-trivial algebraic constraint between universes")
   in Constraints.fold tr s Constraint.empty
 
-let eq_constr_univs_infer univs m n =
-  if m == n then true, Constraints.empty
+let eq_constr_univs_infer univs fold m n accu =
+  if m == n then Some accu
   else 
-    let cstrs = ref Constraints.empty in
-    let eq_universes strict = Univ.Instance.check_eq univs in
+    let cstrs = ref accu in
+    let eq_universes strict = UGraph.check_eq_instances univs in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
-	  else
-	    (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
-	     true)
+	match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
+	| None -> false
+	| Some accu -> cstrs := accu; true
     in
     let rec eq_constr' m n = 
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
-      res, !cstrs
+    if res then Some !cstrs else None
 
 (** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
     to expose subterms of [m] and [n], arguments. *)
-let eq_constr_univs_infer_with kind1 kind2 univs m n =
+let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
   (* spiwack: duplicates the code of [eq_constr_univs_infer] because I
      haven't find a way to factor the code without destroying
      pointer-equality optimisations in [eq_constr_univs_infer].
      Pointer equality is not sufficient to ensure equality up to
      [kind1,kind2], because [kind1] and [kind2] may be different,
      typically evaluating [m] and [n] in different evar maps. *)
-  let cstrs = ref Constraints.empty in
-  let eq_universes strict = Univ.Instance.check_eq univs in
+  let cstrs = ref accu in
+  let eq_universes strict = UGraph.check_eq_instances univs in
   let eq_sorts s1 s2 = 
     if Sorts.equal s1 s2 then true
     else
       let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-      if Univ.check_eq univs u1 u2 then true
-      else
-	(cstrs := Constraints.add (u1, UEq, u2) !cstrs;
-	 true)
+      match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
+      | None -> false
+      | Some accu -> cstrs := accu; true
   in
   let rec eq_constr' m n = 
     Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n
   in
   let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
-  res, !cstrs
+  if res then Some !cstrs else None
 
-let leq_constr_univs_infer univs m n =
-  if m == n then true, Constraints.empty
+let leq_constr_univs_infer univs fold m n accu =
+  if m == n then Some accu
   else 
-    let cstrs = ref Constraints.empty in
-    let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in
+    let cstrs = ref accu in
+    let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	if Univ.check_eq univs u1 u2 then true
-	else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
-	      true)
+	match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
+	| None -> false
+	| Some accu -> cstrs := accu; true
     in
     let leq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_leq univs u1 u2 then
-	    ((if Univ.is_type0_univ u1 then
-		cstrs := Constraints.add (u1, ULe, u2) !cstrs);
-	     true)
-	  else
-	    (cstrs := Constraints.add (u1, ULe, u2) !cstrs; 
-	     true)
+	match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with
+	| None -> false
+	| Some accu -> cstrs := accu; true
     in
     let rec eq_constr' m n = 
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -220,7 +216,7 @@ let leq_constr_univs_infer univs m n =
 	eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
-    res, !cstrs
+    if res then Some !cstrs else None
 
 let eq_constr_universes m n =
   if m == n then true, Constraints.empty
@@ -341,7 +337,7 @@ let existing_instance ctx inst =
     and a2 = Instance.to_array (UContext.instance ctx) in
     let len1 = Array.length a1 and len2 = Array.length a2 in 
       if not (len1 == len2) then
-	Errors.errorlabstrm "Universes"
+	CErrors.errorlabstrm "Universes"
 	  (str "Polymorphic constant expected " ++ int len2 ++ 
 	     str" levels but was given " ++ int len1)
       else ()
@@ -650,14 +646,14 @@ let normalize_univ_variable_opt_subst ectx =
   in
   let update l b =
     assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
-    ectx := Univ.LMap.add l (Some b) !ectx; b
+    try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false
   in normalize_univ_variable ~find ~update
 
 let normalize_univ_variable_subst subst =
   let find l = Univ.LMap.find l !subst in
   let update l b =
     assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
-    subst := Univ.LMap.add l b !subst; b in
+    try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in
     normalize_univ_variable ~find ~update
 
 let normalize_universe_opt_subst subst =
@@ -869,27 +865,27 @@ let normalize_context_set ctx us algs =
   let csts = 
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
-    let g = Univ.LSet.fold (fun v g -> Univ.add_universe v false g)
-			   ctx Univ.empty_universes
+    let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g)
+			   ctx UGraph.empty_universes
     in
     let g =
       Univ.Constraint.fold
 	(fun (l, d, r) g ->
 	 let g =
 	   if not (Level.is_small l || LSet.mem l ctx) then
-	     try Univ.add_universe l false g
-	     with Univ.AlreadyDeclared -> g
+	     try UGraph.add_universe l false g
+	     with UGraph.AlreadyDeclared -> g
 	   else g
 	 in
 	 let g =
 	   if not (Level.is_small r || LSet.mem r ctx) then
-	     try Univ.add_universe r false g
-	     with Univ.AlreadyDeclared -> g
+	     try UGraph.add_universe r false g
+	     with UGraph.AlreadyDeclared -> g
 	   else g
 	 in g) csts g
     in
-    let g = Univ.Constraint.fold Univ.enforce_constraint csts g in
-      Univ.constraints_of_universes g
+    let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in
+      UGraph.constraints_of_universes g
   in
   let noneqs =
     Constraint.fold (fun (l,d,r as cstr) noneqs ->
@@ -930,9 +926,7 @@ let normalize_context_set ctx us algs =
      mentionning other variables remain in noneqs. *)
   let noneqs, ucstrsl, ucstrsr = 
     Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> 
-      let lus = LMap.mem l us 
-      and rus = LMap.mem r us
-      in
+      let lus = LMap.mem l us and rus = LMap.mem r us in
       let ucstrsl' = 
 	if lus then add_list_map l (d, r) ucstrsl
 	else ucstrsl
@@ -1027,7 +1021,7 @@ let refresh_constraints univs (ctx, cstrs) =
     Univ.Constraint.fold (fun c (cstrs', univs as acc) -> 
       let c = translate_cstr c in
       if is_trivial_leq c then acc
-      else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
+      else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs))
       cstrs (Univ.Constraint.empty, univs)
   in ((ctx, cstrs'), univs')
 
@@ -1094,13 +1088,6 @@ let solve_constraints_system levels level_bounds level_min =
     for j=0 to nind-1 do
       if not (Int.equal i j) && Int.Set.mem j clos.(i) then
 	(v.(i) <- Universe.sup v.(i) level_bounds.(j));
-	 (* level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) *)
     done;
-    (* for j=0 to nind-1 do *)
-    (*   match levels.(j) with *)
-    (*   | Some u when not (Univ.Level.is_small u) -> *)
-    (* 	 v.(i) <- univ_level_rem u v.(i) level_min.(i) *)
-    (*   | _ -> () *)
-    (* done *)
   done;
   v
diff --git a/library/universes.mli b/library/universes.mli
index edb06dfc5c..a5740ec49f 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -19,7 +19,7 @@ val is_set_minimization : unit -> bool
 
 (** Global universe name <-> level mapping *)
 type universe_names = 
-  Univ.universe_level Idmap.t * Id.t Univ.LMap.t
+  (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
 
 val global_universe_names : unit -> universe_names
 val set_global_universe_names : universe_names -> unit
@@ -63,6 +63,7 @@ module Constraints : sig
 end
 
 type universe_constraints = Constraints.t
+type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option
 type 'a universe_constrained = 'a * universe_constraints
 type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
 
@@ -71,11 +72,12 @@ val subst_univs_universe_constraints : universe_subst_fn ->
 
 val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function
 
-val to_constraints : universes -> universe_constraints -> constraints
+val to_constraints : UGraph.t -> universe_constraints -> constraints
 
 (** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts,
    application grouping, the universe constraints in [u] and additional constraints [c]. *)
-val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
+val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
+  constr -> constr -> 'a -> 'a option
 
 (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
     {!eq_constr_univs_infer} taking kind-of-term functions, to expose
@@ -83,12 +85,13 @@ val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_
 val eq_constr_univs_infer_with :
   (constr -> (constr,types) kind_of_term) ->
   (constr -> (constr,types) kind_of_term) ->
-  Univ.universes -> constr -> constr -> bool universe_constrained
+  UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
 
 (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
     modulo alpha, casts, application grouping, the universe constraints
     in [u] and additional constraints [c]. *)
-val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
+val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
+  constr -> constr -> 'a -> 'a option
 
 (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
     application grouping and the universe constraints in [c]. *)
@@ -223,7 +226,7 @@ val restrict_universe_context : universe_context_set -> universe_set -> universe
 val simplify_universe_context : universe_context_set -> 
   universe_context_set * universe_level_subst
 
-val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes
+val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_set * UGraph.t
 
 (** Pretty-printing *)