Imported Upstream version 8.6upstream/8.6

32 files changed, 675 insertions, 555 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 5f6f0fe4..c9992fff 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
@@ -158,7 +158,7 @@ let cache_constant ((sp,kn), obj) =
   assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   let cst = Global.lookup_constant kn' in
-  add_section_constant (cst.const_proj <> None) kn' cst.const_hyps;
+  add_section_constant cst.const_polymorphic kn' cst.const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
   add_constant_kind (constant_of_kn kn) obj.cst_kind
 
@@ -325,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let kn' = Global.add_mind dir id mie in
   assert (eq_mind kn' (mind_of_kn kn));
   let mind = Global.lookup_mind kn' in
-  add_section_kn kn' mind.mind_hyps;
+  add_section_kn mind.mind_polymorphic kn' mind.mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
@@ -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,15 +424,32 @@ 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)
+type universe_context_decl = polymorphic * Univ.universe_context_set
+
+let cache_universe_context (p, ctx) =
+  Global.push_context_set p ctx;
+  if p then Lib.add_section_context ctx
+
+let input_universe_context : universe_context_decl -> Libobject.obj =
+  declare_object
+    { (default_object "Global universe context state") with
+      cache_function = (fun (na, pi) -> cache_universe_context pi);
+      load_function = (fun _ (_, pi) -> cache_universe_context pi);
+      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
+      classify_function = (fun a -> Keep a) }
+
+let declare_universe_context poly ctx =
+  Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
 
 (* Discharged or not *)
 type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
@@ -440,13 +458,13 @@ 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;
-    if p then Lib.add_section_context ctx;
-    Universes.set_global_universe_names glob'
+  cache_universe_context (p, ctx);
+  Universes.set_global_universe_names glob'
 
 let input_universes : universe_decl -> Libobject.obj =
   declare_object
@@ -457,6 +475,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
@@ -467,8 +491,10 @@ let do_universe poly l =
 type constraint_decl = polymorphic * Univ.constraints
 
 let cache_constraints (na, (p, c)) =
-  Global.add_constraints c;
-  if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty)
+  let ctx =
+    Univ.ContextSet.add_constraints c
+      Univ.ContextSet.empty (* No declared universes here, just constraints *)
+  in cache_universe_context (p,ctx)
 
 let discharge_constraints (_, (p, c as a)) =
   if p then None else Some a
@@ -483,16 +509,40 @@ let input_constraints : constraint_decl -> Libobject.obj =
       classify_function = (fun a -> Keep a) }
 
 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)
+  let open Misctypes in
+  let u_of_id x =
+    match x with
+    | GProp -> Loc.dummy_loc, (false, Univ.Level.prop)
+    | GSet -> Loc.dummy_loc, (false, Univ.Level.set)
+    | GType None ->
+       user_err_loc (Loc.dummy_loc, "Constraint",
+                     str "Cannot declare constraints on anonymous universes")
+    | GType (Some (loc, id)) ->
+       let id = Id.of_string id in
+       let names, _ = Universes.global_universe_names () in
+       try loc, 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 ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in
+     check_poly ploc p rloc 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 8dd24d27..f70d594d 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
 
@@ -89,7 +87,11 @@ val exists_name : Id.t -> bool
 
 
 
-(** Global universe names and constraints *)
+(** Global universe contexts, names and constraints *)
+
+val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit
 
 val do_universe : polymorphic -> Id.t Loc.located list -> unit
-val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
+val do_constraint : polymorphic ->
+  (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
+  unit
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 04348415..b2806a1a 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
@@ -642,7 +642,11 @@ let declare_module interp_modast id args res mexpr_o fs =
   let env = Global.env () in
   let mty_entry_o, subs, inl_res = match res with
     | Enforce (mty,ann) ->
-        Some (fst (interp_modast env ModType mty)), [], inl2intopt ann
+        let inl = inl2intopt ann in
+        let mte, _ = interp_modast env ModType mty in
+        (* We check immediately that mte is well-formed *)
+        let _ = Mod_typing.translate_mse env None inl mte in
+        Some mte, [], inl
     | Check mtys ->
 	None, build_subtypes interp_modast env mp arg_entries_r mtys,
         default_inline ()
@@ -727,7 +731,10 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs =
   let arg_entries_r = intern_args interp_modast args in
   let params = mk_params_entry arg_entries_r in
   let env = Global.env () in
-  let entry = params, fst (interp_modast env ModType mty) in
+  let mte, _ = interp_modast env ModType mty in
+  (* We check immediately that mte is well-formed *)
+  let _ = Mod_typing.translate_mse env None inl mte in
+  let entry = params, mte in
   let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in
   let sobjs = get_functor_sobjs false env inl entry in
   let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in
@@ -815,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
 
@@ -890,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 2b440c08..3917fe8d 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 0cd4ccb2..6e21880f 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 2398e92b..e748434d 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 9db30c8f..247ca20b 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 3ae44b2c..a78f5f13 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 f94f6216..f4956e3d 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 5f6512e1..9dc0f405 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
 
@@ -207,6 +208,10 @@ type 'a option_sig = {
   optread  : unit -> 'a;
   optwrite : 'a -> unit }
 
+type option_locality = OptLocal | OptDefault | OptGlobal
+
+type option_mod = OptSet | OptAppend
+
 module OptionOrd =
 struct
   type t = option_name
@@ -232,52 +237,57 @@ with Not_found ->
 open Libobject
 open Lib
 
-let declare_option cast uncast
+let warn_deprecated_option =
+  CWarnings.create ~name:"deprecated-option" ~category:"deprecated"
+         (fun key -> str "Option" ++ spc () ++ str (nickname key) ++
+                       strbrk " is deprecated")
+
+let get_locality = function
+  | Some true -> OptLocal
+  | Some false -> OptGlobal
+  | None -> OptDefault
+
+let declare_option cast uncast append ?(preprocess = fun x -> x)
   { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
   let default = read() in
-  (* spiwack: I use two spaces in the nicknames of "local" and "global" objects.
-      That way I shouldn't collide with [nickname key] for any [key]. As [key]-s are
-       lists of strings *without* spaces. *)
-  let (write,lwrite,gwrite) = if sync then
-    let ldecl_obj = (* "Local": doesn't survive section or modules. *)
-      declare_object {(default_object ("L  "^nickname key)) with
-		       cache_function = (fun (_,v) -> write v);
-		       classify_function = (fun _ -> Dispose)}
-    in
-    let decl_obj = (* default locality: survives sections but not modules. *)
-      declare_object {(default_object (nickname key)) with
-		       cache_function = (fun (_,v) -> write v);
-		       classify_function = (fun _ -> Dispose);
-		       discharge_function = (fun (_,v) -> Some v)}
-    in
-    let gdecl_obj = (* "Global": survives section and modules. *)
-      declare_object {(default_object ("G  "^nickname key)) with
-		       cache_function = (fun (_,v) -> write v);
-		       classify_function = (fun v -> Substitute v);
-		       subst_function = (fun (_,v) -> v);
-		       discharge_function = (fun (_,v) -> Some v);
-		       load_function = (fun _ (_,v) -> write v)}
-    in
-    let _ = Summary.declare_summary (nickname key)
-	     { Summary.freeze_function = (fun _ -> read ());
-	       Summary.unfreeze_function = write;
-	       Summary.init_function = (fun () -> write default) }
-    in
-    begin fun v -> add_anonymous_leaf (decl_obj v) end ,
-    begin fun v -> add_anonymous_leaf (ldecl_obj v) end ,
-    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")
+  let change =
+    if sync then
+      let _ = Summary.declare_summary (nickname key)
+        { Summary.freeze_function = (fun _ -> read ());
+          Summary.unfreeze_function = write;
+          Summary.init_function = (fun () -> write default) } in
+      let cache_options (_,(l,m,v)) =
+        match m with
+        | OptSet -> write v
+        | OptAppend -> write (append (read ()) v) in
+      let load_options i o = cache_options o in
+      let subst_options (subst,obj) = obj in
+      let discharge_options (_,(l,_,_ as o)) =
+        match l with OptLocal -> None | _ -> Some o in
+      let classify_options (l,_,_ as o) =
+        match l with OptGlobal -> Substitute o | _ -> Dispose in
+      let options : option_locality * option_mod * _ -> obj =
+        declare_object
+          { (default_object (nickname key)) with
+            load_function = load_options;
+            cache_function = cache_options;
+            subst_function = subst_options;
+            discharge_function = discharge_options;
+            classify_function = classify_options } in
+      (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v)))
+    else
+      (fun _ m v ->
+        let v = preprocess v in
+        match m with
+       | OptSet -> write v
+       | OptAppend -> write (append (read ()) v))
   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
-  let cgwrite v = warn (); gwrite (uncast v) in
-  value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab;
+  let cwrite l v = warn (); change l OptSet (uncast v) in
+  let cappend l v = warn (); change l OptAppend (uncast v) in
+  value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,cappend)) !value_tab;
   write
 
 type 'a write_function = 'a -> unit
@@ -286,36 +296,38 @@ let declare_int_option =
   declare_option
     (fun v -> IntValue v)
     (function IntValue v -> v | _ -> anomaly (Pp.str "async_option"))
+    (fun _ _ -> anomaly (Pp.str "async_option"))
 let declare_bool_option =
   declare_option
     (fun v -> BoolValue v)
     (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option"))
+    (fun _ _ -> anomaly (Pp.str "async_option"))
 let declare_string_option =
   declare_option
     (fun v -> StringValue v)
     (function StringValue v -> v | _ -> anomaly (Pp.str "async_option"))
+    (fun x y -> x^","^y)
 let declare_stringopt_option =
   declare_option
     (fun v -> StringOptValue v)
     (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option"))
+    (fun _ _ -> anomaly (Pp.str "async_option"))
 
 (* 3- User accessible commands *)
 
 (* 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 (name, depr, (_,read,write,lwrite,gwrite)) =
-    try get_option key
-    with Not_found ->
-      errorlabstrm "Goptions.set_option_value"
-        (str "There is no option " ++ str (nickname key) ++ str ".")
-  in
-  let write = match locality with
-    | None -> write
-    | Some true -> lwrite
-    | Some false -> gwrite
-  in
-  write (check_and_cast v (read ()))
+  let opt = try Some (get_option key) with Not_found -> None in
+  match opt with
+  | None -> warn_unknown_option key
+  | Some (name, depr, (_,read,write,append)) ->
+    write (get_locality locality) (check_and_cast v (read ()))
 
 let bad_type_error () = error "Bad type of value for this option."
 
@@ -345,13 +357,18 @@ let check_unset_value v = function
 let set_int_option_value_gen locality =
   set_option_value locality check_int_value
 let set_bool_option_value_gen locality key v =
-  try set_option_value locality check_bool_value key v
-  with UserError (_,s) -> msg_warning s
+  set_option_value locality check_bool_value key v
 let set_string_option_value_gen locality =
   set_option_value locality check_string_value
 let unset_option_value_gen locality key =
-  try set_option_value locality check_unset_value key ()
-  with UserError (_,s) -> msg_warning s
+  set_option_value locality check_unset_value key ()
+
+let set_string_option_append_value_gen locality key v =
+  let opt = try Some (get_option key) with Not_found -> None in
+  match opt with
+  | None -> warn_unknown_option key
+  | Some (name, depr, (_,read,write,append)) ->
+    append (get_locality locality) (check_string_value v (read ()))
 
 let set_int_option_value = set_int_option_value_gen None
 let set_bool_option_value = set_bool_option_value_gen None
@@ -361,27 +378,27 @@ 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
+    | StringValue s   -> str "\"" ++ str s ++ str "\""
     | StringOptValue None   -> str"undefined"
-    | StringOptValue (Some s)   -> str s
+    | StringOptValue (Some s)   -> str "\"" ++ str s ++ str "\""
 (*     | IdentValue r    -> pr_global_env Id.Set.empty r *)
 
 let print_option_value key =
-  let (name, depr, (_,read,_,_,_)) = get_option key in
+  let (name, depr, (_,read,_,_)) = get_option key in
   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
-  let fold key (name, depr, (sync,read,_,_,_)) accu =
+  let fold key (name, depr, (sync,read,_,_)) accu =
     let state = {
       opt_sync = sync;
       opt_name = name;
@@ -400,13 +417,13 @@ let print_tables () =
   in
   str "Synchronous options:" ++ fnl () ++
     OptionMap.fold
-      (fun key (name, depr, (sync,read,_,_,_)) p ->
+      (fun key (name, depr, (sync,read,_,_)) p ->
         if sync then p ++ print_option key name (read ()) depr
         else p)
       !value_tab (mt ()) ++
   str "Asynchronous options:" ++ fnl () ++
     OptionMap.fold
-      (fun key (name, depr, (sync,read,_,_,_)) p ->
+      (fun key (name, depr, (sync,read,_,_)) p ->
         if sync then p
         else p ++ print_option key name (read ()) depr)
       !value_tab (mt ()) ++
diff --git a/library/goptions.mli b/library/goptions.mli
index 26864503..3b3651f3 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -122,13 +122,19 @@ type 'a option_sig = {
 
 (** When an option is declared synchronous ([optsync] is [true]), the output is
    a synchronous write function. Otherwise it is [optwrite] *)
+(** The [preprocess] function is triggered before setting the option. It can be
+    used to emit a warning on certain values, and clean-up the final value. *)
 
 type 'a write_function = 'a -> unit
 
-val declare_int_option   : int option option_sig -> int option write_function
-val declare_bool_option  : bool option_sig   -> bool write_function
-val declare_string_option: string option_sig -> string write_function
-val declare_stringopt_option: string option option_sig -> string option write_function
+val declare_int_option   : ?preprocess:(int option -> int option) ->
+                           int option option_sig -> int option write_function
+val declare_bool_option  : ?preprocess:(bool -> bool) ->
+                           bool option_sig   -> bool write_function
+val declare_string_option: ?preprocess:(string -> string) ->
+                           string option_sig -> string write_function
+val declare_stringopt_option: ?preprocess:(string option -> string option) ->
+                              string option option_sig -> string option write_function
 
 
 (** {6 Special functions supposed to be used only in vernacentries.ml } *)
@@ -154,6 +160,7 @@ val get_ref_table :
 val set_int_option_value_gen    : bool option -> option_name -> int option -> unit
 val set_bool_option_value_gen   : bool option -> option_name -> bool   -> unit
 val set_string_option_value_gen : bool option -> option_name -> string -> unit
+val set_string_option_append_value_gen : bool option -> option_name -> string -> unit
 val unset_option_value_gen : bool option -> option_name -> unit
 
 val set_int_option_value    : option_name -> int option -> unit
diff --git a/library/heads.ml b/library/heads.ml
index 8124d347..02465f22 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 f5f6a3eb..828d652c 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. *)
 
@@ -491,13 +491,15 @@ let implicits_of_global ref =
     let l = Refmap.find ref !implicits_table in
     try
       let rename_l = Arguments_renaming.arguments_names ref in
-      let rename imp name = match imp, name with
-       | Some (_, x,y), Name id -> Some (id, x,y)
-       | _ -> imp in
-      List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l
+      let rec rename implicits names = match implicits, names with
+        | [], _ -> []
+        | _, [] -> implicits
+        | Some (_, x,y) :: implicits, Name id :: names ->
+           Some (id, x,y) :: rename implicits names
+        | imp :: implicits, _ :: names -> imp :: rename implicits names
+      in
+      List.map (fun (t, il) -> t, rename il rename_l) l
     with Not_found -> l
-    | Invalid_argument _ ->
-        anomaly (Pp.str "renamings list and implicits list have different lenghts")
   with Not_found -> [DefaultImpArgs,[]]
 
 let cache_implicits_decl (ref,imps) =
@@ -525,12 +527,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 +540,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 +558,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
@@ -663,7 +659,7 @@ let check_inclusion l =
   let rec aux = function
     | n1::(n2::_ as nl) ->
 	if n1 <= n2 then
-	  error "Sequences of implicit arguments must be of different lengths";
+	  error "Sequences of implicit arguments must be of different lengths.";
 	aux nl
     | _ -> () in
   aux (List.map (fun (imps,_) -> List.length imps) l)
diff --git a/library/impargs.mli b/library/impargs.mli
index 34e529ca..3919a519 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 0c167494..057dc3b6 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 c634193d..21b1bec3 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 ff892916..f680ecee 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
@@ -231,11 +231,16 @@ let add_leaves id objs =
   List.iter add_obj objs;
   oname
 
-let add_anonymous_leaf obj =
+let add_anonymous_leaf ?(cache_first = true) obj =
   let id = anonymous_id () in
   let oname = make_oname id in
-  cache_object (oname,obj);
-  add_entry oname (Leaf obj)
+  if cache_first then begin
+    cache_object (oname,obj);
+    add_entry oname (Leaf obj)
+  end else begin
+    add_entry oname (Leaf obj);
+    cache_object (oname,obj)
+  end
 
 let add_frozen_state () =
   add_anonymous_entry
@@ -408,21 +413,30 @@ let add_section () =
   sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),
                 (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
 
+let check_same_poly p vars =
+  let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in
+  if List.exists pred vars then
+    error "Cannot mix universe polymorphic and monomorphic declarations in sections."
+
 let add_section_variable id impl poly ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-	sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
+       List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab;
+       sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
 
 let add_section_context ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-	sectab := (Context ctx :: vars,repl,abs)::sl
+       check_same_poly true vars;
+       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) ->
@@ -441,12 +455,16 @@ 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 hyps =
+let add_section_replacement f g poly hyps =
   match !sectab with
   | [] -> ()
   | (vars,exps,abs)::sl ->
+    let () = check_same_poly poly vars in
     let sechyps,ctx = extract_hyps (vars,hyps) in
     let ctx = Univ.ContextSet.to_context ctx in
     let subst, ctx = Univ.abstract_universes true ctx in
@@ -454,13 +472,13 @@ let add_section_replacement f g hyps =
     sectab := (vars,f (Univ.UContext.instance ctx,args) exps,
 	      g (sechyps,subst,ctx) abs)::sl
 
-let add_section_kn kn =
+let add_section_kn poly kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
-    add_section_replacement f f
+    add_section_replacement f f poly
 
-let add_section_constant is_projection kn =
+let add_section_constant poly kn =
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
-    add_section_replacement f f
+    add_section_replacement f f poly
 
 let replacement_context () = pi2 (List.hd !sectab)
 
@@ -470,6 +488,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
@@ -487,13 +511,6 @@ let section_instance = function
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
 
-let full_replacement_context () = List.map pi2 !sectab
-let full_section_segment_of_constant con =
-  List.map (fun (vars,_,(x,_)) -> fun hyps ->
-    named_of_variable_context
-      (try pi1 (Names.Cmap.find con x)
-       with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab
-
 (*************)
 (* Sections. *)
 
@@ -594,15 +611,6 @@ let rec dp_of_mp = function
   |Names.MPbound _ -> library_dp ()
   |Names.MPdot (mp,_) -> dp_of_mp mp
 
-let rec split_mp = function
-  |Names.MPfile dp -> dp, Names.DirPath.empty
-  |Names.MPdot (prfx, lbl) ->
-    let mprec, dprec = split_mp prfx in
-    mprec, Libnames.add_dirpath_suffix dprec (Names.Label.to_id lbl)
-  |Names.MPbound mbid ->
-    let (_,id,dp) = Names.MBId.repr mbid in
-    library_dp (), Names.DirPath.make [id]
-
 let rec split_modpath = function
   |Names.MPfile dp -> dp, []
   |Names.MPbound mbid -> library_dp (), [Names.MBId.to_id mbid]
@@ -614,20 +622,6 @@ let library_part = function
   |VarRef id -> library_dp ()
   |ref -> dp_of_mp (mp_of_global ref)
 
-let remove_section_part ref =
-  let sp = Nametab.path_of_global ref in
-  let dir,_ = repr_path sp in
-  match ref with
-  | VarRef id ->
-      anomaly (Pp.str "remove_section_part not supported on local variables")
-  | _ ->
-      if is_dirpath_prefix_of dir (cwd ()) then
-        (* Not yet (fully) discharged *)
-        pop_dirpath_n (sections_depth ()) (cwd ())
-      else
-	(* Theorem/Lemma outside its outer section of definition *)
-	dir
-
 (************************)
 (* Discharging names *)
 
diff --git a/library/lib.mli b/library/lib.mli
index 29fc7cd2..a8e110c6 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -54,7 +54,7 @@ val segment_of_objects :
   current list of operations (most recent ones coming first). *)
 
 val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name
-val add_anonymous_leaf : Libobject.obj -> unit
+val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
 val pull_to_head : Libnames.object_name -> unit
 
 (** this operation adds all objects with the same name and calls [load_object]
@@ -138,10 +138,8 @@ val library_dp : unit -> Names.DirPath.t
 
 (** Extract the library part of a name even if in a section *)
 val dp_of_mp : Names.module_path -> Names.DirPath.t
-val split_mp : Names.module_path -> Names.DirPath.t * Names.DirPath.t
 val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list
 val library_part :  Globnames.global_reference -> Names.DirPath.t
-val remove_section_part : Globnames.global_reference -> Names.DirPath.t
 
 (** {6 Sections } *)
 
@@ -168,19 +166,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 : bool (* is_projection *) -> 
-  Names.constant -> Context.named_context -> unit
-val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit
+val add_section_constant : Decl_kinds.polymorphic ->
+  Names.constant -> Context.Named.t -> unit
+val add_section_kn : Decl_kinds.polymorphic ->
+  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 } *)
@@ -189,10 +189,3 @@ val discharge_kn :  Names.mutual_inductive -> Names.mutual_inductive
 val discharge_con : Names.constant -> Names.constant
 val discharge_global : Globnames.global_reference -> Globnames.global_reference
 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
-
-
diff --git a/library/libnames.ml b/library/libnames.ml
index a2f22b2e..dd74e192 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 706e3991..caa03c85 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 f3880a43..51b9af05 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 79e5792c..d44f796a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 
 open Names
@@ -35,7 +35,7 @@ module Delayed :
 sig
 
 type 'a delayed
-val in_delayed : string -> in_channel -> 'a delayed
+val in_delayed : string -> in_channel -> 'a delayed * Digest.t
 val fetch_delayed : 'a delayed -> 'a
 
 end =
@@ -50,7 +50,7 @@ type 'a delayed = {
 let in_delayed f ch =
   let pos = pos_in ch in
   let _, digest = System.skip_in_segment f ch in
-  { del_file = f; del_digest = digest; del_off = pos; }
+  ({ del_file = f; del_digest = digest; del_off = pos; }, digest)
 
 (** Fetching a table of opaque terms at position [pos] in file [f],
     expecting to find first a copy of [digest]. *)
@@ -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 *)
@@ -171,9 +171,8 @@ let register_loaded_library m =
     let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
     let f = prefix ^ "cmo" in
     let f = Dynlink.adapt_filename f in
-    (* This will not produce errors or warnings if the native compiler was
-       not enabled *)
-    Nativelib.link_library ~prefix ~dirname ~basename:f
+    if not Coq_config.no_native_compiler then
+      Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
     | [] -> link m; [libname]
@@ -272,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
@@ -286,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
@@ -322,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
@@ -381,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 ->
@@ -438,56 +431,59 @@ let mk_summary m = {
 let intern_from_file f =
   let ch = raw_intern_library f in
   let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in
-  let (lmd : seg_lib delayed) = in_delayed f ch in
+  let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in
   let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
   let _ = System.skip_in_segment f ch in
   let _ = System.skip_in_segment f ch in
-  let (del_opaque : seg_proofs delayed) = in_delayed f ch in
+  let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in
   close_in ch;
   register_library_filename lsd.md_name f;
   add_opaque_table lsd.md_name (ToFetch del_opaque);
   let open Safe_typing in
   match univs with
-  | None -> mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty
+  | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
   | Some (utab,uall,true) ->
       add_univ_table lsd.md_name (Fetched utab);
-      mk_library lsd lmd (Dvivo (digest_lsd,digest_u)) uall
+      mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall
   | Some (utab,_,false) ->
       add_univ_table lsd.md_name (Fetched utab);
-      mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty
+      mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
 
 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 =
@@ -557,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)))
@@ -579,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
@@ -604,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
 
@@ -614,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
@@ -638,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;
@@ -703,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
@@ -732,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 = {
@@ -764,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
@@ -781,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 25c9604c..b9044b60 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 78f8dd25..d03c6c55 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
@@ -65,17 +72,12 @@ let add_load_path phys_path coq_path ~implicit =
     let replace =
       if DirPath.equal coq_path old_path then
         implicit <> old_implicit
-      else if DirPath.equal coq_path (Nameops.default_root_prefix)
-              && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then
-        false (* This is the default "-I ." path, don't override the old path *)
       else
         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 +86,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 +95,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 49ffc114..4e79edbd 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 98b417c2..71405d02 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 40acb3ae..fa5db37e 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 2e1be764..95bd819d 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 46c52acc..6efa07f3 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 c24a0b4b..1b57613c 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 7972c478..112b20a4 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 =
@@ -706,12 +702,45 @@ let pr_universe_body = function
 
 let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
 
-exception Found of Level.t
+let compare_constraint_type d d' =
+  match d, d' with
+  | Eq, Eq -> 0
+  | Eq, _ -> -1
+  | _, Eq -> 1
+  | Le, Le -> 0
+  | Le, _ -> -1
+  | _, Le -> 1
+  | Lt, Lt -> 0
+
+type lowermap = constraint_type LMap.t
+
+let lower_union =
+  let merge k a b =
+    match a, b with
+    | Some _, None -> a
+    | None, Some _ -> b
+    | None, None -> None
+    | Some l, Some r ->
+       if compare_constraint_type l r >= 0 then a
+       else b
+  in LMap.merge merge
+
+let lower_add l c m =
+  try let c' = LMap.find l m in
+      if compare_constraint_type c c' > 0 then
+        LMap.add l c m
+      else m
+  with Not_found -> LMap.add l c m
+
+let lower_of_list l =
+  List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l
+
+exception Found of Level.t * lowermap
 let find_inst insts v =
-  try LMap.iter (fun k (enf,alg,v') ->
-    if not alg && enf && Universe.equal v' v then raise (Found k))
+  try LMap.iter (fun k (enf,alg,v',lower) ->
+    if not alg && enf && Universe.equal v' v then raise (Found (k, lower)))
 	insts; raise Not_found
-  with Found l -> l
+  with Found (f,l) -> (f,l)
 
 let compute_lbound left =
  (** The universe variable was not fixed yet.
@@ -730,27 +759,33 @@ let compute_lbound left =
 	 else None))
       None left
   
-let instantiate_with_lbound u lbound alg enforce (ctx, us, algs, insts, cstrs) =
+let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cstrs) =
   if enforce then
     let inst = Universe.make u in
     let cstrs' = enforce_leq lbound inst cstrs in
       (ctx, us, LSet.remove u algs, 
-       LMap.add u (enforce,alg,lbound) insts, cstrs'), (enforce, alg, inst)
+       LMap.add u (enforce,alg,lbound,lower) insts, cstrs'),
+      (enforce, alg, inst, lower)
   else (* Actually instantiate *)
     (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
-     LMap.add u (enforce,alg,lbound) insts, cstrs), (enforce, alg, lbound)
+     LMap.add u (enforce,alg,lbound,lower) insts, cstrs),
+    (enforce, alg, lbound, lower)
 
 type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
 
 let pr_constraints_map cmap =
   LMap.fold (fun l cstrs acc -> 
     Level.pr l ++ str " => " ++ 
-      prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl ()
-    ++ acc)
+      prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++
+      fnl () ++ acc)
     cmap (mt ())
 
 let remove_alg l (ctx, us, algs, insts, cstrs) =
   (ctx, us, LSet.remove l algs, insts, cstrs)
+
+let remove_lower u lower =
+  let levels = Universe.levels u in
+  LSet.fold (fun l acc -> LMap.remove l acc) levels lower
     
 let minimize_univ_variables ctx us algs left right cstrs =
   let left, lbounds = 
@@ -760,22 +795,50 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	let lbounds' = 
 	  match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
 	  | None -> lbounds
-	  | Some lbound -> LMap.add r (true, false, lbound) lbounds
+	  | Some lbound -> LMap.add r (true, false, lbound, lower_of_list lower)
+                                   lbounds
 	in (Univ.LMap.remove r left, lbounds'))
       left (left, Univ.LMap.empty)
   in
   let rec instance (ctx', us, algs, insts, cstrs as acc) u =
-    let acc, left = 
-      try let l = LMap.find u left in
-	    List.fold_left
-	      (fun (acc, left') (d, l) -> 
-	       let acc', (enf,alg,l') = aux acc l in
-	       let l' = 
-		 if enf then Universe.make l 
-		 else l' 
-	       in acc', (d, l') :: left')
-	      (acc, []) l
-      with Not_found -> acc, []
+    let acc, left, lower =
+      try
+        let l = LMap.find u left in
+	let acc, left, newlow, lower =
+          List.fold_left
+	  (fun (acc, left', newlow, lower') (d, l) ->
+	   let acc', (enf,alg,l',lower) = aux acc l in
+	   let l' =
+	     if enf then Universe.make l
+	     else l'
+	   in acc', (d, l') :: left',
+              lower_add l d newlow, lower_union lower lower')
+	  (acc, [], LMap.empty, LMap.empty) l
+        in
+        let not_lower (d,l) =
+        (* We're checking if (d,l) is already implied by the lower
+	  constraints on some level u. If it represents l < u (d is Lt
+	  or d is Le and i > 0, the i < 0 case is impossible due to
+	  invariants of Univ), and the lower constraints only have l <=
+	  u then it is not implied. *)
+          Univ.Universe.exists
+          (fun (l,i) ->
+             let d =
+               if i == 0 then d
+               else match d with
+                    | Le -> Lt
+                    | d -> d
+             in
+             try let d' = LMap.find l lower in
+                 (* If d is stronger than the already implied lower
+                  * constraints we must keep it. *)
+                 compare_constraint_type d d' > 0
+             with Not_found ->
+               (** No constraint existing on l *) true) l
+        in
+        let left = List.uniquize (List.filter not_lower left) in
+        (acc, left, LMap.union newlow lower)
+      with Not_found -> acc, [], LMap.empty
     and right =
       try Some (LMap.find u right)
       with Not_found -> None
@@ -783,31 +846,33 @@ let minimize_univ_variables ctx us algs left right cstrs =
     let instantiate_lbound lbound =
       let alg = LSet.mem u algs in
 	if alg then
-	  (* u is algebraic: we instantiate it with it's lower bound, if any, 
+	  (* u is algebraic: we instantiate it with its lower bound, if any,
               or enforce the constraints if it is bounded from the top. *)
-	  instantiate_with_lbound u lbound true false acc
+          let lower = remove_lower lbound lower in
+	  instantiate_with_lbound u lbound lower true false acc
 	else (* u is non algebraic *)
 	  match Universe.level lbound with
 	  | Some l -> (* The lowerbound is directly a level *) 
 	     (* u is not algebraic but has no upper bounds,
   	        we instantiate it with its lower bound if it is a 
 	        different level, otherwise we keep it. *)
+             let lower = LMap.remove l lower in
 	     if not (Level.equal l u) then
 	       (* Should check that u does not 
   	          have upper constraints that are not already in right *)
 	       let acc' = remove_alg l acc in
-		 instantiate_with_lbound u lbound false false acc'
-	     else acc, (true, false, lbound)
-	| None -> 
-	  try 
-	    (* if right <> None then raise Not_found; *)
-	    (* Another universe represents the same lower bound, 
-	       we can share them with no harm. *)
-	    let can = find_inst insts lbound in
-	      instantiate_with_lbound u (Universe.make can) false false acc
+		 instantiate_with_lbound u lbound lower false false acc'
+	     else acc, (true, false, lbound, lower)
+	  | None ->
+	     try
+	       (* Another universe represents the same lower bound,
+                  we can share them with no harm. *)
+	       let can, lower = find_inst insts lbound in
+               let lower = LMap.remove can lower in
+	       instantiate_with_lbound u (Universe.make can) lower false false acc
 	  with Not_found -> 
 	    (* We set u as the canonical universe representing lbound *)
-	    instantiate_with_lbound u lbound false true acc
+	    instantiate_with_lbound u lbound lower false true acc
     in
     let acc' acc = 
       match right with
@@ -816,7 +881,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in
 	  if List.is_empty dangling then acc
 	  else
-	    let ((ctx', us, algs, insts, cstrs), (enf,_,inst as b)) = acc in
+	    let ((ctx', us, algs, insts, cstrs), (enf,_,inst,lower as b)) = acc in
 	    let cstrs' = List.fold_left (fun cstrs (d, r) -> 
 	      if d == Univ.Le then
 		enforce_leq inst (Universe.make r) cstrs
@@ -828,15 +893,15 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	    in
 	      (ctx', us, algs, insts, cstrs'), b
     in
-      if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u))
+      if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower))
       else
 	let lbound = compute_lbound left in
 	  match lbound with
 	  | None -> (* Nothing to do *)
-	    acc' (acc, (true, false, Universe.make u))
+	    acc' (acc, (true, false, Universe.make u, lower))
 	  | Some lbound ->
 	     try acc' (instantiate_lbound lbound) 
-	     with Failure _ -> acc' (acc, (true, false, Universe.make u))
+	     with Failure _ -> acc' (acc, (true, false, Universe.make u, lower))
   and aux (ctx', us, algs, seen, cstrs as acc) u =
     try acc, LMap.find u seen 
     with Not_found -> instance acc u
@@ -869,27 +934,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 +995,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
@@ -959,10 +1022,10 @@ let universes_of_constr c =
   let rec aux s c = 
     match kind_of_term c with
     | Const (_, u) | Ind (_, u) | Construct (_, u) ->
-      LSet.union (Instance.levels u) s
+      LSet.fold LSet.add (Instance.levels u) s
     | Sort u when not (Sorts.is_small u) -> 
       let u = univ_of_sort u in
-	LSet.union (Universe.levels u) s
+      LSet.fold LSet.add (Universe.levels u) s
     | _ -> fold_constr aux s c
   in aux LSet.empty c
 
@@ -1027,7 +1090,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 +1157,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 edb06dfc..d3a271b8 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,46 +226,12 @@ 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 *)
 
 val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
 
-(* For tracing *)
-
-type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
-
-val pr_constraints_map : constraints_map -> Pp.std_ppcmds
-
-val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> universe_set -> universe_set -> 
-  universe_level * (universe_set * universe_set * universe_set)
-    
-val compute_lbound : (constraint_type * Univ.universe) list -> universe option
-
-val instantiate_with_lbound : 
-  Univ.LMap.key ->
-  Univ.universe ->
-  bool ->
-  bool ->
-  Univ.LSet.t * Univ.universe option Univ.LMap.t *
-    Univ.LSet.t *
-    (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints ->
-  (Univ.LSet.t * Univ.universe option Univ.LMap.t *
-    Univ.LSet.t *
-     (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) *
-    (bool * bool * Univ.universe)
-
-val minimize_univ_variables : 
-           Univ.LSet.t ->
-           Univ.universe option Univ.LMap.t ->
-           Univ.LSet.t ->
-  constraints_map -> constraints_map ->
-           Univ.constraints ->
-           Univ.LSet.t * Univ.universe option Univ.LMap.t *
-	     Univ.LSet.t *
-           (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints
-
 (** {6 Support for old-style sort-polymorphism } *)
 
 val solve_constraints_system : universe option array -> universe array -> universe array ->