Imported Upstream version 8.5~beta3+dfsg

27 files changed, 535 insertions, 666 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
deleted file mode 100644
index 62645b23..00000000
--- a/library/assumptions.ml
+++ /dev/null
@@ -1,225 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* The following definitions are used by the function
-   [assumptions] which gives as an output the set of all
-   axioms and sections variables on which a given term depends
-   in a context (expectingly the Global context) *)
-
-(* Initial author: Arnaud Spiwack
-   Module-traversing code: Pierre Letouzey *)
-
-open Pp
-open Errors
-open Util
-open Names
-open Term
-open Declarations
-open Mod_subst
-open Globnames
-
-type context_object =
-  | Variable of Id.t (* A section variable or a Let definition *)
-  | Axiom of constant      (* An axiom or a constant. *)
-  | Opaque of constant     (* An opaque constant. *)
-  | Transparent of constant
-
-(* Defines a set of [assumption] *)
-module OrderedContextObject =
-struct
-  type t = context_object
-  let compare x y =
-      match x , y with
-      | Variable i1 , Variable i2 -> Id.compare i1 i2
-      | Axiom k1 , Axiom k2 -> con_ord k1 k2
-      | Opaque k1 , Opaque k2 -> con_ord k1 k2
-      | Transparent k1 , Transparent k2 -> con_ord k1 k2
-      | Axiom _ , Variable _ -> 1
-      | Opaque _ , Variable _
-      | Opaque _ , Axiom _ -> 1
-      | Transparent _ , Variable _
-      | Transparent _ , Axiom _
-      | Transparent _ , Opaque _ -> 1
-      | _ , _ -> -1
-end
-
-module ContextObjectSet = Set.Make (OrderedContextObject)
-module ContextObjectMap = Map.Make (OrderedContextObject)
-
-(** For a constant c in a module sealed by an interface (M:T and
-    not M<:T), [Global.lookup_constant] may return a [constant_body]
-    without body. We fix this by looking in the implementation
-    of the module *)
-
-let modcache = ref (MPmap.empty : structure_body MPmap.t)
-
-let rec search_mod_label lab = function
-  | [] -> raise Not_found
-  | (l, SFBmodule mb) :: _ when Label.equal l lab -> mb
-  | _ :: fields -> search_mod_label lab fields
-
-let rec search_cst_label lab = function
-  | [] -> raise Not_found
-  | (l, SFBconst cb) :: _ when Label.equal l lab -> cb
-  | _ :: fields -> search_cst_label lab fields
-
-(* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But:
-    a) I don't see currently what should be used instead
-    b) this shouldn't be critical for Print Assumption. At worse some
-       constants will have a canonical name which is non-canonical,
-       leading to failures in [Global.lookup_constant], but our own
-       [lookup_constant] should work.
-*)
-
-let rec fields_of_functor f subs mp0 args = function
-  |NoFunctor a -> f subs mp0 args a
-  |MoreFunctor (mbid,_,e) ->
-    match args with
-    | [] -> assert false (* we should only encounter applied functors *)
-    | mpa :: args ->
-      let subs = add_mbid mbid mpa empty_delta_resolver (*TODO*) subs in
-      fields_of_functor f subs mp0 args e
-
-let rec lookup_module_in_impl mp =
-  try Global.lookup_module mp
-  with Not_found ->
-    (* The module we search might not be exported by its englobing module(s).
-       We access the upper layer, and then do a manual search *)
-    match mp with
-      | MPfile _ | MPbound _ ->
-	raise Not_found (* should have been found by [lookup_module] *)
-      | MPdot (mp',lab') ->
-	let fields = memoize_fields_of_mp mp' in
-	search_mod_label lab' fields
-
-and memoize_fields_of_mp mp =
-  try MPmap.find mp !modcache
-  with Not_found ->
-    let l = fields_of_mp mp in
-    modcache := MPmap.add mp l !modcache;
-    l
-
-and fields_of_mp mp =
-  let mb = lookup_module_in_impl mp in
-  let fields,inner_mp,subs = fields_of_mb empty_subst mb [] in
-  let subs =
-    if mp_eq inner_mp mp then subs
-    else add_mp inner_mp mp mb.mod_delta subs
-  in
-  Modops.subst_structure subs fields
-
-and fields_of_mb subs mb args = match mb.mod_expr with
-  |Algebraic expr -> fields_of_expression subs mb.mod_mp args expr
-  |Struct sign -> fields_of_signature subs mb.mod_mp args sign
-  |Abstract|FullStruct -> fields_of_signature subs mb.mod_mp args mb.mod_type
-
-(** The Abstract case above corresponds to [Declare Module] *)
-
-and fields_of_signature x =
-  fields_of_functor
-    (fun subs mp0 args struc ->
-      assert (List.is_empty args);
-      (struc, mp0, subs)) x
-
-and fields_of_expr subs mp0 args = function
-  |MEident mp ->
-    let mb = lookup_module_in_impl (subst_mp subs mp) in
-    fields_of_mb subs mb args
-  |MEapply (me1,mp2) -> fields_of_expr subs mp0 (mp2::args) me1
-  |MEwith _ -> assert false (* no 'with' in [mod_expr] *)
-
-and fields_of_expression x = fields_of_functor fields_of_expr x
-
-let lookup_constant_in_impl cst fallback =
-  try
-    let mp,dp,lab = repr_kn (canonical_con cst) in
-    let fields = memoize_fields_of_mp mp in
-    (* A module found this way is necessarily closed, in particular
-       our constant cannot be in an opened section : *)
-    search_cst_label lab fields
-  with Not_found ->
-    (* Either:
-       - The module part of the constant isn't registered yet :
-         we're still in it, so the [constant_body] found earlier
-         (if any) was a true axiom.
-       - The label has not been found in the structure. This is an error *)
-    match fallback with
-      | Some cb -> cb
-      | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst)
-
-let lookup_constant cst =
-  try
-    let cb = Global.lookup_constant cst in
-    if Declareops.constant_has_body cb then cb
-    else lookup_constant_in_impl cst (Some cb)
-  with Not_found -> lookup_constant_in_impl cst None
-
-(** Graph traversal of an object, collecting on the way the dependencies of
-    traversed objects *)
-let rec traverse accu t = match kind_of_term t with
-| Var id ->
-  let body () = match Global.lookup_named id with (_, body, _) -> body in
-  traverse_object accu body (VarRef id)
-| Const (kn, _) ->
-  let body () = Global.body_of_constant_body (lookup_constant kn) in
-  traverse_object accu body (ConstRef kn)
-| Ind (ind, _) ->
-  traverse_object accu (fun () -> None) (IndRef ind)
-| Construct (cst, _) ->
-  traverse_object accu (fun () -> None) (ConstructRef cst)
-| Meta _ | Evar _ -> assert false
-| _ -> Constr.fold traverse accu t
-
-and traverse_object (curr, data) body obj =
-  let data =
-    if Refmap.mem obj data then data
-    else match body () with
-    | None -> Refmap.add obj Refset.empty data
-    | Some body ->
-      let (contents, data) = traverse (Refset.empty, data) body in
-      Refmap.add obj contents data
-  in
-  (Refset.add obj curr, data)
-
-let traverse t =
-  let () = modcache := MPmap.empty in
-  traverse (Refset.empty, Refmap.empty) t
-
-(** Hopefully bullet-proof function to recover the type of a constant. It just
-    ignores all the universe stuff. There are many issues that can arise when
-    considering terms out of any valid environment, so use with caution. *)
-let type_of_constant cb = match cb.Declarations.const_type with
-| Declarations.RegularArity ty -> ty
-| Declarations.TemplateArity (ctx, arity) ->
-  Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level)
-
-let assumptions ?(add_opaque=false) ?(add_transparent=false) st t =
-  let (idts, knst) = st in
-  (** Only keep the transitive dependencies *)
-  let (_, graph) = traverse t in
-  let fold obj _ accu = match obj with
-  | VarRef id ->
-    let (_, body, t) = Global.lookup_named id in
-    if Option.is_empty body then ContextObjectMap.add (Variable id) t accu
-    else accu
-  | ConstRef kn ->
-    let cb = lookup_constant kn in
-    if not (Declareops.constant_has_body cb) then
-      let t = type_of_constant cb in
-      ContextObjectMap.add (Axiom kn) t accu
-    else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
-      let t = type_of_constant cb in
-      ContextObjectMap.add (Opaque kn) t accu
-    else if add_transparent then
-      let t = type_of_constant cb in
-      ContextObjectMap.add (Transparent kn) t accu
-    else
-      accu
-  | IndRef _ | ConstructRef _ -> accu
-  in
-  Refmap.fold fold graph ContextObjectMap.empty
diff --git a/library/assumptions.mli b/library/assumptions.mli
deleted file mode 100644
index bb36a972..00000000
--- a/library/assumptions.mli
+++ /dev/null
@@ -1,41 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Util
-open Names
-open Term
-open Globnames
-
-(** A few declarations for the "Print Assumption" command
-    @author spiwack *)
-type context_object =
-  | Variable of Id.t  (** A section variable or a Let definition *)
-  | Axiom of constant       (** An axiom or a constant. *)
-  | Opaque of constant      (** An opaque constant. *)
-  | Transparent of constant (** A transparent constant *)
-
-(** AssumptionSet.t is a set of [assumption] *)
-module ContextObjectSet : Set.S with type elt = context_object
-module ContextObjectMap : Map.ExtS
-  with type key = context_object and module Set := ContextObjectSet
-
-(** Collects all the objects on which a term directly relies, bypassing kernel
-    opacity, together with the recursive dependence DAG of objects.
-
-    WARNING: some terms may not make sense in the environment, because they are
-    sealed inside opaque modules. Do not try to do anything fancy with those
-    terms apart from printing them, otherwise demons may fly out of your nose.
-*)
-val traverse : constr -> (Refset.t * Refset.t Refmap.t)
-
-(** Collects all the assumptions (optionally including opaque definitions)
-   on which a term relies (together with their type). The above warning of
-   {!traverse} also applies. *)
-val assumptions :
-  ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> constr ->
-    Term.types ContextObjectMap.t
diff --git a/library/declare.ml b/library/declare.ml
index c3181e4c..5968fbf3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -27,22 +27,22 @@ open Decls
 open Decl_kinds
 
 (** flag for internal message display *)
-type internal_flag = 
-  | KernelVerbose (* kernel action, a message is displayed *)
-  | KernelSilent  (* kernel action, no message is displayed *)
-  | UserVerbose   (* user action, a message is displayed *)
+type internal_flag =
+  | UserAutomaticRequest (* kernel action, a message is displayed *)
+  | InternalTacticRequest  (* kernel action, no message is displayed *)
+  | UserIndividualRequest   (* user action, a message is displayed *)
 
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
-  | SectionLocalDef of definition_entry
+  | SectionLocalDef of Safe_typing.private_constants definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
 let cache_variable ((sp,_),o) =
   match o with
-  | Inl ctx -> Global.push_context_set ctx
+  | Inl ctx -> Global.push_context_set false ctx
   | Inr (id,(p,d,mk)) ->
   (* Constr raisonne sur les noms courts *)
   if variable_exists id then
@@ -50,20 +50,20 @@ let cache_variable ((sp,_),o) =
 
   let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ((ty,ctx),poly,impl) ->
-      let () = Global.push_named_assum ((id,ty),ctx) in
+      let () = Global.push_named_assum ((id,ty,poly),ctx) in
       let impl = if impl then Implicit else Explicit in
 	impl, true, poly, ctx
     | SectionLocalDef (de) ->
-      let () = Global.push_named_def (id,de) in
-        Explicit, de.const_entry_opaque, de.const_entry_polymorphic, 
-	(Univ.ContextSet.of_context de.const_entry_universes) in
+      let univs = Global.push_named_def (id,de) in
+      Explicit, de.const_entry_opaque,
+      de.const_entry_polymorphic, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id impl poly ctx;
   Dischargedhypsmap.set_discharged_hyps sp [];
   add_variable_data id (p,opaq,ctx,poly,mk)
 
 let discharge_variable (_,o) = match o with
-  | Inr (id,_) -> 
+  | Inr (id,_) ->
     if variable_polymorphic id then None
     else Some (Inl (variable_context id))
   | Inl _ -> Some o
@@ -93,9 +93,13 @@ type constant_obj = {
   cst_hyps : Dischargedhypsmap.discharged_hyps;
   cst_kind : logical_kind;
   cst_locl : bool;
+  mutable cst_exported : Safe_typing.exported_private_constant list;
+  (* mutable: to avoid change the libobject API, since cache_function
+   * does not return an updated object *)
+  mutable cst_was_seff : bool
 }
 
-type constant_declaration = constant_entry * logical_kind
+type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
 
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
@@ -116,8 +120,9 @@ let open_constant i ((sp,kn), obj) =
     match (Global.lookup_constant con).const_body with
     | (Def _ | Undef _) -> ()
     | OpaqueDef lc ->
-        match Opaqueproof.get_constraints (Global.opaque_tables ())lc with
-        | Some f when Future.is_val f -> Global.push_context_set (Future.force f)
+        match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with
+        | Some f when Future.is_val f ->
+	   Global.push_context_set false (Future.force f)
         | _ -> ()
 
 let exists_name id =
@@ -130,8 +135,17 @@ let check_exists sp =
 let cache_constant ((sp,kn), obj) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
-  let () = check_exists sp in
-  let kn' = Global.add_constant dir id obj.cst_decl in
+  let kn' =
+    if obj.cst_was_seff then begin
+      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))
+    end else
+      let () = check_exists sp in
+      let kn', exported = Global.add_constant dir id obj.cst_decl in
+      obj.cst_exported <- exported;
+      kn' in
   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
@@ -156,19 +170,22 @@ let discharge_constant ((sp, kn), obj) =
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = 
-  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
+  ConstantEntry
+    (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
   cst_hyps = [];
   cst_kind = cst.cst_kind;
   cst_locl = cst.cst_locl;
+  cst_exported = [];
+  cst_was_seff = cst.cst_was_seff;
 }
 
 let classify_constant cst = Substitute (dummy_constant cst)
 
-let inConstant : constant_obj -> obj =
-  declare_object { (default_object "CONSTANT") with
+let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) =
+  declare_object_full { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
     open_function = open_constant;
@@ -176,17 +193,41 @@ let inConstant : constant_obj -> obj =
     subst_function = ident_subst_function;
     discharge_function = discharge_constant }
 
+let declare_scheme = ref (fun _ _ -> assert false)
+let set_declare_scheme f = declare_scheme := f
+
 let declare_constant_common id cst =
-  let (sp,kn) = add_leaf id (inConstant cst) in
+  let update_tables c =
+(*  Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *)
+    declare_constant_implicits c;
+    Heads.declare_head (EvalConstRef c);
+    Notation.declare_ref_arguments_scope (ConstRef c) in
+  let o = inConstant cst in
+  let _, kn as oname = add_leaf id o in
+  List.iter (fun (c,ce,role) ->
+      (* handling of private_constants just exported *)
+      let o = inConstant {
+        cst_decl = ConstantEntry (false, ce);
+        cst_hyps = [] ;
+        cst_kind = IsProof Theorem;
+        cst_locl = false;
+        cst_exported = [];
+        cst_was_seff = true; } in
+      let id = Label.to_id (pi3 (Constant.repr3 c)) in
+      ignore(add_leaf id o);
+      update_tables c;
+      match role with
+      | Safe_typing.Subproof -> ()
+      | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|])
+    (outConstant o).cst_exported;
+  pull_to_head oname;
   let c = Global.constant_of_delta_kn kn in
-  declare_constant_implicits c;
-  Heads.declare_head (EvalConstRef c);
-  Notation.declare_ref_arguments_scope (ConstRef c);
+  update_tables c;
   c
 
-let definition_entry ?(opaque=false) ?(inline=false) ?types 
-    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body =
-  { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
+let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
+    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
+  { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
     const_entry_polymorphic = poly;
@@ -195,98 +236,33 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
-let declare_scheme = ref (fun _ _ -> assert false)
-let set_declare_scheme f = declare_scheme := f
-let declare_sideff env fix_exn se =
-  let cbl, scheme = match se with
-    | SEsubproof (c, cb, pt) -> [c, cb, pt], None
-    | SEscheme (cbl, k) ->
-        List.map (fun (_,c,cb,pt) -> c,cb,pt) cbl, Some (cbl,k) in
-  let id_of c = Names.Label.to_id (Names.Constant.label c) in
-  let pt_opaque_of cb pt =
-    match cb, pt with
-    | { const_body = Def sc }, _ -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false
-    | { const_body = OpaqueDef _ }, `Opaque(pt,univ) -> (pt, univ), true
-    | _ -> assert false
-  in
-  let ty_of cb =
-    match cb.Declarations.const_type with
-    | Declarations.RegularArity t -> Some t 
-    | Declarations.TemplateArity _ -> None in
-  let cst_of cb pt =
-    let pt, opaque = pt_opaque_of cb pt in
-    let univs, subst = 
-      if cb.const_polymorphic then
-	let univs = Univ.instantiate_univ_context cb.const_universes in
-	  univs, Vars.subst_instance_constr (Univ.UContext.instance univs)
-      else cb.const_universes, fun x -> x
-    in
-    let pt = (subst (fst pt), snd pt) in
-    let ty = Option.map subst (ty_of cb) in
-    { cst_decl = ConstantEntry (DefinitionEntry {
-        const_entry_body = Future.from_here ~fix_exn (pt, Declareops.no_seff);
-        const_entry_secctx = Some cb.Declarations.const_hyps;
-        const_entry_type = ty;
-        const_entry_opaque = opaque;
-        const_entry_inline_code = false;
-        const_entry_feedback = None;
-	const_entry_polymorphic = cb.const_polymorphic;
-	const_entry_universes = univs;
-    });
-    cst_hyps = [] ;
-    cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
-    cst_locl = true;
-  } in
-  let exists c =
-    try ignore(Environ.lookup_constant c env); true
-    with Not_found -> false in 
-  let knl =
-    CList.map_filter (fun (c,cb,pt) ->
-      if exists c then None
-      else Some (c,declare_constant_common (id_of c) (cst_of cb pt))) cbl in
-  match scheme with
-  | None -> ()
-  | Some (inds_consts,kind) ->
-      !declare_scheme kind (Array.of_list
-         (List.map (fun (c,kn) ->
-             CList.find_map (fun (x,c',_,_) ->
-               if Constant.equal c c' then Some (x,kn) else None) inds_consts)
-           knl))
-
-let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
-  let cd = (* We deal with side effects *)
+let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+  let export = (* We deal with side effects *)
     match cd with
-    | Entries.DefinitionEntry de ->
-        if export_seff ||
-           not de.const_entry_opaque ||
-           de.const_entry_polymorphic then
+    | DefinitionEntry de when
+        export_seff ||
+        not de.const_entry_opaque ||
+        de.const_entry_polymorphic ->
           let bo = de.const_entry_body in
           let _, seff = Future.force bo in
-          if Declareops.side_effects_is_empty seff then cd
-          else begin
-            let seff = Declareops.uniquize_side_effects seff in
-            Declareops.iter_side_effects
-              (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
-            Entries.DefinitionEntry { de with
-              const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
-                pt, Declareops.no_seff) }
-        end
-        else cd
-    | _ -> cd
+          Safe_typing.empty_private_constants <> seff
+    | _ -> false
   in
   let cst = {
-    cst_decl = ConstantEntry cd;
+    cst_decl = ConstantEntry (export,cd);
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
+    cst_exported = [];
+    cst_was_seff = false;
   } in
   let kn = declare_constant_common id cst in
   kn
 
-let declare_definition ?(internal=UserVerbose) 
+let declare_definition ?(internal=UserIndividualRequest)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
   ?(poly=false) id ?types (body,ctx) =
-  let cb = 
+  let cb =
     definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
   in
     declare_constant ~internal ~local id
@@ -382,12 +358,12 @@ let inInductive : inductive_obj -> obj =
 let declare_projections mind =
   let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
     match spec.mind_record with
-    | Some (Some (_, kns, pjs)) -> 
-      Array.iteri (fun i kn -> 
+    | Some (Some (_, kns, pjs)) ->
+      Array.iteri (fun i kn ->
 	let id = Label.to_id (Constant.label kn) in
 	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
 	let kn' = declare_constant id (ProjectionEntry entry,
-				       IsDefinition StructureComponent) 
+				       IsDefinition StructureComponent)
 	in
 	  assert(eq_constant kn kn')) kns; true
     | Some None | None -> false
@@ -441,50 +417,69 @@ let assumption_message id =
 
 (** Global universe names, in a different summary *)
 
-type universe_names = 
+type universe_names =
     (Univ.universe_level Idmap.t * Id.t Univ.LMap.t)
 
-let input_universes : universe_names -> Libobject.obj =
-  let open Libobject in 
-    declare_object
+(* Discharged or not *)
+type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
+
+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))
+      (glob, Univ.ContextSet.empty) l
+  in
+    Global.push_context_set false ctx;
+    if p then Lib.add_section_context ctx;
+    Universes.set_global_universe_names glob'
+
+let input_universes : universe_decl -> Libobject.obj =
+  declare_object
     { (default_object "Global universe name state") with
-      cache_function = (fun (na, pi) -> Universes.set_global_universe_names pi);
-      load_function = (fun _ (_, pi) -> Universes.set_global_universe_names pi);
-      discharge_function = (fun (_, a) -> Some a);
+      cache_function = (fun (na, pi) -> cache_universes pi);
+      load_function = (fun _ (_, pi) -> cache_universes pi);
+      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
       classify_function = (fun a -> Keep a) }
 
-let do_universe l =
-  let glob = Universes.global_universe_names () in
-  let glob' = 
-    List.fold_left (fun (idl,lid) (l, id) ->
-      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
-	(Idmap.add id lev idl, Univ.LMap.add lev id lid))
-      glob l
+let do_universe poly l =
+  let l =
+    List.map (fun (l, id) ->
+	      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
+	      (id, lev)) l
   in
-    Lib.add_anonymous_leaf (input_universes glob')
+    Lib.add_anonymous_leaf (input_universes (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 discharge_constraints (_, (p, c as a)) =
+  if p then None else Some a
 
-let input_constraints : Univ.constraints -> Libobject.obj =
-  let open Libobject in 
+let input_constraints : constraint_decl -> Libobject.obj =
+  let open Libobject in
     declare_object
     { (default_object "Global universe constraints") with
-      cache_function = (fun (na, c) -> Global.add_constraints c);
-      load_function = (fun _ (_, c) -> Global.add_constraints c);
-      discharge_function = (fun (_, a) -> Some a);
+      cache_function = cache_constraints;
+      load_function = (fun _ -> cache_constraints);
+      discharge_function = discharge_constraints;
       classify_function = (fun a -> Keep a) }
 
-let do_constraint l = 
-  let u_of_id = 
+let do_constraint poly l =
+  let u_of_id =
     let names, _ = Universes.global_universe_names () in
-      fun (loc, id) -> 
+      fun (loc, id) ->
 	try Idmap.find id names
 	with Not_found ->
-	  user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)	    
+	  user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
   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)
     Univ.Constraint.empty l
   in
-    Lib.add_anonymous_leaf (input_constraints constraints)
-  
+    Lib.add_anonymous_leaf (input_constraints (poly, constraints))
diff --git a/library/declare.mli b/library/declare.mli
index d8a00db0..c6119a58 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -22,7 +22,7 @@ open Decl_kinds
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type section_variable_entry =
-  | SectionLocalDef of definition_entry
+  | SectionLocalDef of Safe_typing.private_constants definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -32,7 +32,7 @@ val declare_variable : variable -> variable_declaration -> object_name
 (** Declaration of global constructions 
    i.e. Definition/Theorem/Axiom/Parameter/... *)
 
-type constant_declaration = constant_entry * logical_kind
+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
@@ -43,14 +43,15 @@ type constant_declaration = constant_entry * logical_kind
    
    *)
 type internal_flag =
-  | KernelVerbose
-  | KernelSilent
-  | UserVerbose
+  | UserAutomaticRequest
+  | InternalTacticRequest
+  | UserIndividualRequest
 
 (* Defaut definition entries, transparent with no secctx or proj information *)
-val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> 
-  ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Declareops.side_effects ->
-  constr -> definition_entry
+val definition_entry : ?fix_exn:Future.fix_exn ->
+  ?opaque:bool -> ?inline:bool -> ?types:types ->
+  ?poly:polymorphic -> ?univs:Univ.universe_context ->
+  ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 val declare_constant :
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
@@ -60,7 +61,7 @@ val declare_definition :
   ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
   constr Univ.in_universe_context_set -> constant
 
-(** Since transparent constant's side effects are globally declared, we
+(** Since transparent constants' side effects are globally declared, we
  *  need that *)
 val set_declare_scheme :
   (string -> (inductive * constant) array -> unit) -> unit
@@ -85,5 +86,5 @@ val exists_name : Id.t -> bool
 
 (** Global universe names and constraints *)
 
-val do_universe : Id.t Loc.located list -> unit
-val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> 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
diff --git a/library/declaremods.ml b/library/declaremods.ml
index cc7c4d7f..7f607a51 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -166,12 +166,14 @@ let consistency_checks exists dir dirinfo =
     let globref =
       try Nametab.locate_dir (qualid_of_dirpath dir)
       with Not_found ->
-        anomaly (pr_dirpath dir ++ str " should already exist!")
+        errorlabstrm "consistency_checks"
+          (pr_dirpath dir ++ str " should already exist!")
     in
     assert (eq_global_dir_reference globref dirinfo)
   else
     if Nametab.exists_dir dir then
-      anomaly (pr_dirpath dir ++ str " already exists")
+      errorlabstrm "consistency_checks"
+        (pr_dirpath dir ++ str " already exists")
 
 let compute_visibility exists i =
   if exists then Nametab.Exactly i else Nametab.Until i
@@ -845,10 +847,6 @@ type library_objects = Lib.lib_objects * Lib.lib_objects
 
 (** For the native compiler, we cache the library values *)
 
-type library_values = Nativecode.symbol array
-let library_values =
-  Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES"
-
 let register_library dir cenv (objs:library_objects) digest univ =
   let mp = MPfile dir in
   let () =
@@ -857,15 +855,15 @@ let register_library dir cenv (objs:library_objects) digest univ =
       ignore(Global.lookup_module mp);
     with Not_found ->
       (* If not, let's do it now ... *)
-      let mp', values = Global.import cenv univ digest in
+      let mp' = Global.import cenv univ digest in
       if not (ModPath.equal mp mp') then
         anomaly (Pp.str "Unexpected disk module name");
-      library_values := Dirmap.add dir values !library_values
   in
   let sobjs,keepobjs = objs in
   do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs
 
-let get_library_symbols_tbl dir = Dirmap.find dir !library_values
+let get_library_native_symbols dir =
+  Safe_typing.get_library_native_symbols (Global.safe_env ()) dir
 
 let start_library dir =
   let mp = Global.start_library dir in
@@ -950,7 +948,7 @@ type 'modast module_params =
 let debug_print_modtab _ =
   let pr_seg = function
     | [] -> str "[]"
-    | l -> str ("[." ^ string_of_int (List.length l) ^ ".]")
+    | l -> str "[." ++ int (List.length l) ++ str ".]"
   in
   let pr_modinfo mp (prefix,substobjs,keepobjs) s =
     s ++ str (string_of_mp mp) ++ (spc ())
diff --git a/library/declaremods.mli b/library/declaremods.mli
index c3578ec4..319d168d 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -75,7 +75,7 @@ val register_library :
   Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest ->
   Univ.universe_context_set -> unit
 
-val get_library_symbols_tbl : library_name -> Nativecode.symbol array
+val get_library_native_symbols : library_name -> Nativecode.symbols
 
 val start_library : library_name -> unit
 
diff --git a/library/global.ml b/library/global.ml
index 875097e4..6002382c 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -19,6 +19,7 @@ module GlobalSafeEnv : sig
   val safe_env : unit -> Safe_typing.safe_environment
   val set_safe_env : Safe_typing.safe_environment -> unit
   val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
+  val is_joined_environment : unit -> bool
 
 end = struct
 
@@ -27,6 +28,9 @@ let global_env = ref Safe_typing.empty_environment
 let join_safe_environment ?except () =
   global_env := Safe_typing.join_safe_environment ?except !global_env
 
+let is_joined_environment () =
+  Safe_typing.is_joined_environment !global_env
+  
 let () =
   Summary.declare_summary global_env_summary_name
     { Summary.freeze_function = (function
@@ -50,6 +54,7 @@ end
 let safe_env = GlobalSafeEnv.safe_env
 let join_safe_environment ?except () =
   GlobalSafeEnv.join_safe_environment ?except ()
+let is_joined_environment = GlobalSafeEnv.is_joined_environment
 
 let env () = Safe_typing.env_of_safe_env (safe_env ())
 
@@ -73,13 +78,12 @@ let globalize_with_summary fs f =
 let i2l = Label.of_id
 
 let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
-let push_named_def d = globalize0 (Safe_typing.push_named_def d)
+let push_named_def d = globalize (Safe_typing.push_named_def d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
-let push_context_set c = globalize0 (Safe_typing.push_context_set c)
-let push_context c = globalize0 (Safe_typing.push_context c)
+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_type_in_type () = globalize0 (Safe_typing.set_type_in_type)
 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)
@@ -245,7 +249,7 @@ let current_dirpath () =
 
 let with_global f = 
   let (a, ctx) = f (env ()) (current_dirpath ()) in
-    push_context_set ctx; a
+    push_context_set false ctx; a
 
 (* spiwack: register/unregister functions for retroknowledge *)
 let register field value by_clause =
diff --git a/library/global.mli b/library/global.mli
index 62d7ea32..03469bea 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -27,23 +27,23 @@ val named_context : unit -> Context.named_context
 
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
-val set_type_in_type : unit -> unit
 
 (** Variables, Local definitions, constants, inductive types *)
 
-val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit
-val push_named_def   : (Id.t * Entries.definition_entry) -> unit
+val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
+val push_named_def   : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
 
 val add_constant :
-  DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
+  DirPath.t -> Id.t -> Safe_typing.global_declaration ->
+    constant * Safe_typing.exported_private_constant list
 val add_mind :
   DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive
 
 (** Extra universe constraints *)
 val add_constraints : Univ.constraints -> unit
 
-val push_context : Univ.universe_context -> unit
-val push_context_set : Univ.universe_context_set -> unit
+val push_context : bool -> Univ.universe_context -> unit
+val push_context_set : bool -> Univ.universe_context_set -> unit
 
 (** Non-interactive modules and module types *)
 
@@ -102,7 +102,7 @@ val export : ?except:Future.UUIDSet.t -> DirPath.t ->
   module_path * Safe_typing.compiled_library * Safe_typing.native_library
 val import :
   Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest ->
-  module_path * Nativecode.symbol array
+  module_path
 
 (** {6 Misc } *)
 
@@ -112,6 +112,7 @@ val import :
 val env_of_context : Environ.named_context_val -> Environ.env
 
 val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
+val is_joined_environment : unit -> bool
 
 val is_polymorphic : Globnames.global_reference -> bool
 val is_template_polymorphic : Globnames.global_reference -> bool
diff --git a/library/goptions.ml b/library/goptions.ml
index ef25fa59..30d195f8 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -20,6 +20,7 @@ type option_value =
   | BoolValue   of bool
   | IntValue    of int option
   | StringValue of string
+  | StringOptValue of string option
 
 (** Summary of an option status *)
 type option_state = {
@@ -35,7 +36,7 @@ type option_state = {
 let nickname table = String.concat " " table
 
 let error_undeclared_key key =
-  error ((nickname key)^": no table or option of this type")
+  errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type")
 
 (****************************************************************************)
 (* 1- Tables                                                                *)
@@ -293,6 +294,10 @@ let declare_string_option =
   declare_option
     (fun v -> StringValue v)
     (function StringValue v -> v | _ -> anomaly (Pp.str "async_option"))
+let declare_stringopt_option =
+  declare_option
+    (fun v -> StringOptValue v)
+    (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option"))
 
 (* 3- User accessible commands *)
 
@@ -301,7 +306,9 @@ let declare_string_option =
 let set_option_value locality check_and_cast key v =
   let (name, depr, (_,read,write,lwrite,gwrite)) =
     try get_option key
-    with Not_found -> error ("There is no option "^(nickname 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
@@ -322,11 +329,13 @@ let check_bool_value v = function
 
 let check_string_value v = function
   | StringValue _ -> StringValue v
+  | StringOptValue _ -> StringOptValue (Some v)
   | _ -> bad_type_error ()
 
 let check_unset_value v = function
   | BoolValue _ -> BoolValue false
   | IntValue _ -> IntValue None
+  | StringOptValue _ -> StringOptValue None
   | _ -> bad_type_error ()
 
 (* Nota: For compatibility reasons, some errors are treated as
@@ -357,6 +366,8 @@ let msg_option_value (name,v) =
     | IntValue (Some n) -> int n
     | IntValue None   -> str "undefined"
     | StringValue s   -> str s
+    | StringOptValue None   -> str"undefined"
+    | StringOptValue (Some s)   -> str s
 (*     | IdentValue r    -> pr_global_env Id.Set.empty r *)
 
 let print_option_value key =
@@ -364,9 +375,9 @@ let print_option_value key =
   let s = read () in
   match s with
     | BoolValue b ->
-	msg_info (str ("The "^name^" mode is "^(if b then "on" else "off")))
+	msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off"))
     | _ ->
-	msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s))
+	msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s))
 
 let get_tables () =
   let tables = !value_tab in
@@ -383,7 +394,7 @@ let get_tables () =
 
 let print_tables () =
   let print_option key name value depr =
-    let msg = str ("  "^(nickname key)^": ") ++ msg_option_value (name, value) in
+    let msg = str "  " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in
     if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
     else msg ++ fnl ()
   in
@@ -401,10 +412,10 @@ let print_tables () =
       !value_tab (mt ()) ++
   str "Tables:" ++ fnl () ++
     List.fold_right
-      (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+      (fun (nickkey,_) p -> p ++ str "  " ++ str nickkey ++ fnl ())
       !string_table (mt ()) ++
     List.fold_right
-      (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+      (fun (nickkey,_) p -> p ++ str "  " ++ str nickkey ++ fnl ())
       !ref_table (mt ()) ++
     fnl ()
 
diff --git a/library/goptions.mli b/library/goptions.mli
index 1c44f890..9d87c14c 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -128,6 +128,7 @@ 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
 
 
 (** {6 Special functions supposed to be used only in vernacentries.ml } *)
@@ -165,6 +166,7 @@ type option_value =
   | BoolValue   of bool
   | IntValue    of int option
   | StringValue of string
+  | StringOptValue of string option
 
 (** Summary of an option status *)
 type option_state = {
diff --git a/library/heads.ml b/library/heads.ml
index 5c153b06..73d2aa05 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -68,7 +68,10 @@ let kind_of_head env t =
         | None -> NotImmediatelyComputableHead)
   | Const (cst,_) ->
       (try on_subterm k l b (constant_head cst)
-       with Not_found -> assert false)
+       with Not_found ->
+         Errors.anomaly
+           Pp.(str "constant not found in kind_of_head: " ++
+               str (Names.Constant.to_string cst)))
   | Construct _ | CoFix _ ->
       if b then NotImmediatelyComputableHead else ConstructorHead
   | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
diff --git a/library/impargs.ml b/library/impargs.ml
index 4b0e2e3d..d15a02fe 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Globnames
+open Nameops
 open Term
 open Reduction
 open Declarations
@@ -103,7 +104,7 @@ let set_maximality imps b =
   inferable following a rigid path (useful to know how to print a
   partial application)
 
-- [Manual] means the argument has been explicitely set as implicit.
+- [Manual] means the argument has been explicitly set as implicit.
 
   We also consider arguments inferable from the conclusion but it is
   operational only if [conclusion_matters] is true.
@@ -337,10 +338,12 @@ let check_correct_manual_implicits autoimps l =
   List.iter (function
     | ExplByName id,(b,fi,forced) ->
 	if not forced then
-	  error ("Wrong or non-dependent implicit argument name: "^(Id.to_string id)^".")
+	  errorlabstrm ""
+            (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".")
     | ExplByPos (i,_id),_t ->
 	if i<1 || i>List.length autoimps then
-	  error ("Bad implicit argument number: "^(string_of_int i)^".")
+	  errorlabstrm ""
+            (str "Bad implicit argument number: " ++ int i ++ str ".")
 	else
 	  errorlabstrm ""
 	    (str "Cannot set implicit argument number " ++ int i ++
diff --git a/library/impargs.mli b/library/impargs.mli
index 1d3a73e9..30f2e30f 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -59,8 +59,8 @@ type implicit_explanation =
 	  inferable following a rigid path (useful to know how to print a
 	  partial application) *)
   | Manual
-      (** means the argument has been explicitely set as implicit. *)
-      
+      (** means the argument has been explicitly set as implicit. *)
+
 (**  We also consider arguments inferable from the conclusion but it is
      operational only if [conclusion_matters] is true. *)
 
diff --git a/library/lib.ml b/library/lib.ml
index 9977b666..297441e6 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -75,7 +75,8 @@ let classify_segment seg =
     | (_,ClosedModule _) :: stk -> clean acc stk
     | (_,OpenedSection _) :: _ -> error "there are still opened sections"
     | (_,OpenedModule (ty,_,_,_)) :: _ ->
-      error ("there are still opened " ^ module_kind ty ^"s")
+      errorlabstrm "Lib.classify_segment"
+        (str "there are still opened " ++ str (module_kind ty) ++ str "s")
     | (_,FrozenState _) :: stk -> clean acc stk
   in
     clean ([],[],[]) (List.rev seg)
@@ -197,6 +198,9 @@ let split_lib_at_opening sp =
 let add_entry sp node =
   lib_stk := (sp,node) :: !lib_stk
 
+let pull_to_head oname =
+  lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk
+
 let anonymous_id =
   let n = ref 0 in
   fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n))
@@ -274,7 +278,7 @@ let start_modtype = start_mod true None
 let error_still_opened string oname =
   let id = basename (fst oname) in
   errorlabstrm ""
-    (str ("The "^string^" ") ++ pr_id id ++ str " is still opened.")
+    (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.")
 
 let end_mod is_type =
   let oname,fs =
@@ -318,7 +322,8 @@ let end_compilation_checks dir =
     try match snd (find_entry_p is_opening_node) with
       | OpenedSection _ -> error "There are some open sections."
       | OpenedModule (ty,_,_,_) ->
-	error ("There are some open "^module_kind ty^"s.")
+	errorlabstrm "Lib.end_compilation_checks"
+          (str "There are some open " ++ str (module_kind ty) ++ str "s.")
       | _ -> assert false
     with Not_found -> ()
   in
@@ -369,7 +374,8 @@ let find_opening_node id =
     let oname,entry = find_entry_p is_opening_node in
     let id' = basename (fst oname) in
     if not (Names.Id.equal id id') then
-      error ("Last block to end has name "^(Names.Id.to_string id')^".");
+      errorlabstrm "Lib.find_opening_node"
+        (str "Last block to end has name " ++ pr_id id' ++ str ".");
     entry
   with Not_found -> error "There is nothing to end."
 
@@ -389,10 +395,13 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
 		  
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
+type secentry =
+  | Variable of (Names.Id.t * Decl_kinds.binding_kind *
+		   Decl_kinds.polymorphic * Univ.universe_context_set)
+  | Context of Univ.universe_context_set
+
 let sectab =
-  Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * 
-		Decl_kinds.polymorphic * Univ.universe_context_set) list *
-		        Opaqueproof.work_list * abstr_list) list)
+  Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list)
     ~name:"section-context"
 
 let add_section () =
@@ -403,16 +412,25 @@ let add_section_variable id impl poly ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-	sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl
+	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
 
 let extract_hyps (secs,ohyps) =
   let rec aux = function
-    | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
+    | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
       let l, r = aux (idl,hyps) in 
 	(id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
-    | ((_,_,poly,ctx)::idl,hyps) -> 
+    | (Variable (_,_,poly,ctx)::idl,hyps) ->
         let l, r = aux (idl,hyps) in
           l, if poly then Univ.ContextSet.union r ctx else r
+    | (Context ctx :: idl, hyps) ->
+       let l, r = aux (idl, hyps) in
+       l, Univ.ContextSet.union r ctx
     | [], _ -> [],Univ.ContextSet.empty
   in aux (secs,ohyps)
 
@@ -433,7 +451,8 @@ let add_section_replacement f g hyps =
     let ctx = Univ.ContextSet.to_context ctx in
     let subst, ctx = Univ.abstract_universes true ctx in
     let args = instance_from_variable_context (List.rev sechyps) in
-    sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,subst,ctx) abs)::sl
+    sectab := (vars,f (Univ.UContext.instance ctx,args) exps,
+	      g (sechyps,subst,ctx) abs)::sl
 
 let add_section_kn kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
@@ -453,10 +472,13 @@ let section_segment_of_mutual_inductive kn =
 
 let section_instance = function
   | VarRef id ->
-      if List.exists (fun (id',_,_,_) -> Names.id_eq id id') 
-	(pi1 (List.hd !sectab))
-      then Univ.Instance.empty, [||]
-      else raise Not_found
+     let eq = function
+       | Variable (id',_,_,_) -> Names.id_eq id id'
+       | Context _ -> false
+     in
+     if List.exists eq (pi1 (List.hd !sectab))
+     then Univ.Instance.empty, [||]
+     else raise Not_found
   | ConstRef con ->
       Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
diff --git a/library/lib.mli b/library/lib.mli
index 9c4d26c5..bb883175 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -55,6 +55,7 @@ val segment_of_objects :
 
 val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name
 val add_anonymous_leaf : Libobject.obj -> unit
+val pull_to_head : Libnames.object_name -> unit
 
 (** this operation adds all objects with the same name and calls [load_object]
    for each of them *)
@@ -172,7 +173,7 @@ val section_instance : Globnames.global_reference -> Univ.universe_instance * Na
 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
diff --git a/library/libobject.ml b/library/libobject.ml
index 5f2a2127..85c830ea 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Libnames
+open Pp
 
 (* 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
@@ -33,15 +34,13 @@ type 'a object_declaration = {
   discharge_function : object_name * 'a -> 'a option;
   rebuild_function : 'a -> 'a }
 
-let yell s = Errors.anomaly (Pp.str s)
-
 let default_object s = {
   object_name = s;
   cache_function = (fun _ -> ());
   load_function = (fun _ _ -> ());
   open_function = (fun _ _ -> ());
   subst_function = (fun _ ->
-    yell ("The object "^s^" does not know how to substitute!"));
+    Errors.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)}
@@ -102,7 +101,16 @@ let declare_object_full odecl =
 			     dyn_rebuild_function = rebuild };
   (infun,outfun)
 
-let declare_object odecl = fst (declare_object_full odecl)
+(* The "try .. with .. " allows for correct printing when calling
+   declare_object a loading time.
+*)
+
+let declare_object odecl =
+  try fst (declare_object_full odecl)
+  with e -> Errors.fatal_error (Errors.print e) (Errors.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)
 
diff --git a/library/library.ml b/library/library.ml
index b4261309..024ac9e6 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -19,10 +19,12 @@ open Lib
 (************************************************************************)
 (*s Low-level interning/externing of libraries to files *)
 
-(*s Loading from disk to cache (preparation phase) *)
+let raw_extern_library f =
+  System.raw_extern_state Coq_config.vo_magic_number f
 
-let (raw_extern_library, raw_intern_library) =
-  System.raw_extern_intern Coq_config.vo_magic_number
+let raw_intern_library f =
+  System.with_magic_number_check
+    (System.raw_intern_state Coq_config.vo_magic_number) f
 
 (************************************************************************)
 (** Serialized objects loaded on-the-fly *)
@@ -56,7 +58,7 @@ let in_delayed f ch =
 let fetch_delayed del =
   let { del_digest = digest; del_file = f; del_off = pos; } = del in
   try
-    let ch = System.with_magic_number_check raw_intern_library f in
+    let ch = raw_intern_library f in
     let () = seek_in ch pos in
     let obj, _, digest' = System.marshal_in_segment f ch in
     let () = close_in ch in
@@ -76,19 +78,22 @@ open Delayed
 type compilation_unit_name = DirPath.t
 
 type library_disk = {
-  md_name : compilation_unit_name;
   md_compiled : Safe_typing.compiled_library;
   md_objects : Declaremods.library_objects;
+}
+
+type summary_disk = {
+  md_name : compilation_unit_name;
+  md_imports : compilation_unit_name array;
   md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
-  md_imports : compilation_unit_name array }
+}
 
 (*s Modules loaded in memory contain the following informations. They are
     kept in the global table [libraries_table]. *)
 
 type library_t = {
   library_name : compilation_unit_name;
-  library_compiled : Safe_typing.compiled_library;
-  library_objects : Declaremods.library_objects;
+  library_data : library_disk delayed;
   library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
   library_imports : compilation_unit_name array;
   library_digests : Safe_typing.vodigest;
@@ -126,7 +131,8 @@ let find_library dir =
 let try_find_library dir =
   try find_library dir
   with Not_found ->
-    error ("Unknown library " ^ (DirPath.to_string dir))
+    errorlabstrm "Library.find_library"
+      (str "Unknown library " ++ str (DirPath.to_string dir))
 
 let register_library_filename dir f =
   (* Not synchronized: overwrite the previous binding if one existed *)
@@ -165,8 +171,9 @@ 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
-    if not !Flags.no_native_compiler then
-      Nativelib.link_library ~prefix ~dirname ~basename:f
+    (* This will not produce errors or warnings if the native compiler was
+       not enabled *)
+    Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
     | [] -> link m; [libname]
@@ -374,14 +381,14 @@ let access_table what tables dp i =
     | Fetched t -> t
     | ToFetch f ->
       let dir_path = Names.DirPath.to_string dp in
-      msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
+      Flags.if_verbose msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
       let t =
         try fetch_delayed f
         with Faulty f ->
-          error
-            ("The file "^f^" (bound to " ^ dir_path ^
-            ") is inaccessible or corrupted,\n" ^
-            "cannot load some "^what^" in it.\n")
+          errorlabstrm "Library.access_table"
+            (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
+             str ") is inaccessible or corrupted,\ncannot load some " ++
+             str what ++ str " in it.\n")
       in
       tables := LibraryMap.add dp (Fetched t) !tables;
       t
@@ -405,19 +412,19 @@ let () =
 (************************************************************************)
 (* Internalise libraries *)
 
+type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
   Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool
 type seg_discharge = Opaqueproof.cooking_info list array
 type seg_proofs = Term.constr Future.computation array
 
-let mk_library md digests univs =
+let mk_library sd md digests univs =
   {
-    library_name     = md.md_name;
-    library_compiled = md.md_compiled;
-    library_objects  = md.md_objects;
-    library_deps     = md.md_deps;
-    library_imports  = md.md_imports;
+    library_name     = sd.md_name;
+    library_data     = md;
+    library_deps     = sd.md_deps;
+    library_imports  = sd.md_imports;
     library_digests  = digests;
     library_extra_univs = univs;
   }
@@ -429,24 +436,25 @@ let mk_summary m = {
 }
 
 let intern_from_file f =
-  let ch = System.with_magic_number_check raw_intern_library f in
-  let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in
+  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 (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
   close_in ch;
-  register_library_filename lmd.md_name f;
-  add_opaque_table lmd.md_name (ToFetch del_opaque);
+  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 lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
+  | None -> mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty
   | Some (utab,uall,true) ->
-      add_univ_table lmd.md_name (Fetched utab);
-      mk_library lmd (Dvivo (digest_lmd,digest_u)) uall
+      add_univ_table lsd.md_name (Fetched utab);
+      mk_library lsd lmd (Dvivo (digest_lsd,digest_u)) uall
   | Some (utab,_,false) ->
-      add_univ_table lmd.md_name (Fetched utab);
-      mk_library lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
+      add_univ_table lsd.md_name (Fetched utab);
+      mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty
 
 module DPMap = Map.Make(DirPath)
 
@@ -462,7 +470,7 @@ let rec intern_library (needed, contents) (dir, f) from =
   let m = intern_from_file f in
   if not (DirPath.equal dir m.library_name) then
     errorlabstrm "load_physical_library"
-      (str ("The file " ^ f ^ " contains library") ++ spc () ++
+      (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));
@@ -475,52 +483,18 @@ and intern_library_deps libs dir m from =
 and intern_mandatory_library caller from libs (dir,d) =
   let digest, libs = intern_library libs (try_locate_absolute_library dir) from in
   if not (Safe_typing.digest_match ~actual:digest ~required:d) then
-    errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^
-      ".vo makes inconsistent assumptions over library " ^
-      DirPath.to_string dir));
+    errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir));
   libs
 
 let rec_intern_library libs mref =
   let _, libs = intern_library libs mref None in
   libs
 
-let check_library_short_name f dir = function
-  | Some id when not (Id.equal id (snd (split_dirpath dir))) ->
-      errorlabstrm "check_library_short_name"
-      (str ("The file " ^ f ^ " contains library") ++ spc () ++
-      pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++
-      pr_id id)
-  | _ -> ()
-
-let rec_intern_by_filename_only id f =
-  let m = try intern_from_file f with Sys_error s -> error s in
-  (* Only the base name is expected to match *)
-  check_library_short_name f m.library_name id;
-  (* We check no other file containing same library is loaded *)
-  if library_is_loaded m.library_name then
-    begin
-      msg_warning
-	(pr_dirpath m.library_name ++ str " is already loaded from file " ++
-	str (library_full_filename m.library_name));
-      m.library_name, []
-    end
- else
-    let needed, contents = intern_library_deps ([], DPMap.empty) m.library_name m (Some f) in
-    let needed = List.map (fun dir -> dir, DPMap.find dir contents) needed in
-    m.library_name, needed
-
 let native_name_from_filename f =
-  let ch = System.with_magic_number_check raw_intern_library f in
-  let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in
+  let ch = raw_intern_library f in
+  let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
   Nativecode.mod_uid_of_dirpath lmd.md_name
 
-let rec_intern_library_from_file idopt f =
-  (* A name is specified, we have to check it contains library id *)
-  let paths = Loadpath.get_paths () in
-  let _, f =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in
-  rec_intern_by_filename_only idopt f
-
 (**********************************************************************)
 (*s [require_library] loads and possibly opens a library. This is a
     synchronized operation. It is performed as follows:
@@ -539,10 +513,11 @@ let rec_intern_library_from_file idopt f =
 *)
 
 let register_library m =
+  let l = fetch_delayed m.library_data in
   Declaremods.register_library
     m.library_name
-    m.library_compiled
-    m.library_objects
+    l.md_compiled
+    l.md_objects
     m.library_digests
     m.library_extra_univs;
   register_loaded_library (mk_summary m)
@@ -595,25 +570,13 @@ let require_library_from_dirpath modrefl export =
       add_anonymous_leaf (in_require (needed,modrefl,export));
   add_frozen_state ()
 
-let require_library_from_file idopt file export =
-  let modref,needed = rec_intern_library_from_file idopt file in
-  let needed = List.rev_map snd needed in
-  if Lib.is_module_or_modtype () then begin
-    add_anonymous_leaf (in_require (needed,[modref],None));
-    Option.iter (fun exp -> add_anonymous_leaf (in_import_library ([modref],exp)))
-      export
-  end
-  else
-    add_anonymous_leaf (in_require (needed,[modref],export));
-  add_frozen_state ()
-
 (* the function called by Vernacentries.vernac_import *)
 
 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 ^ " is not a module"))
+      (loc,"import_library", str (string_of_qualid qid) ++ str " is not a module")
 
 let import_module export modl =
   (* Optimization: libraries in a raw in the list are imported
@@ -638,7 +601,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)^" is not a module")))
+                str (string_of_qualid dir) ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
 
@@ -650,8 +613,8 @@ let check_coq_overwriting p id =
   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
     errorlabstrm ""
-      (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^
-      ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
+      (str "Cannot build module " ++ str (DirPath.to_string 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
    others caracters than letters, digits, or `_` *)
@@ -673,29 +636,28 @@ let check_module_name s =
     | c -> err c
 
 let start_library f =
-  let paths = Loadpath.get_paths () in
-  let _, longf =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let () = if not (Sys.file_exists f) then
+    errorlabstrm "" (hov 0 (str "Can't find file" ++ spc () ++ str f))
+  in
   let ldir0 =
     try
-      let lp = Loadpath.find_load_path (Filename.dirname longf) in
+      let lp = Loadpath.find_load_path (Filename.dirname f) in
       Loadpath.logical lp
     with Not_found -> Nameops.default_root_prefix
   in
-  let file = Filename.basename f in
+  let file = Filename.chop_extension (Filename.basename f) in
   let id = Id.of_string file in
   check_module_name file;
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
   Declaremods.start_library ldir;
-  ldir,longf
+  ldir
 
 let load_library_todo f =
-  let paths = Loadpath.get_paths () in
-  let _, longf =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let longf = Loadpath.locate_file (f^".v") in
   let f = longf^"io" in
-  let ch = System.with_magic_number_check raw_intern_library f in
+  let ch = raw_intern_library f in
+  let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
   let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
   let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
   let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in
@@ -706,7 +668,7 @@ let load_library_todo f =
   if s2 = None then errorlabstrm "restart" (str"not a .vio file");
   if s3 = None then errorlabstrm "restart" (str"not a .vio file");
   if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file");
-  longf, s1, Option.get s2, Option.get s3, Option.get tasks, s5
+  longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
 (*s [save_library dir] ends library [dir] and save it to the disk. *)
@@ -770,18 +732,23 @@ let save_library_to ?todo dir f otab =
     if not(is_done_or_todo i x) then Errors.errorlabstrm "library"
       Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
     opaque_table;
-  let md = {
+  let sd = {
     md_name = dir;
+    md_deps = Array.of_list (current_deps ());
+    md_imports = Array.of_list (current_reexports ());
+  } in
+  let md = {
     md_compiled = cenv;
     md_objects = seg;
-    md_deps = Array.of_list (current_deps ());
-    md_imports = Array.of_list (current_reexports ()) } in
-  if Array.exists (fun (d,_) -> DirPath.equal d dir) md.md_deps then
+  } in
+  if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then
     error_recursively_dependent_library dir;
   (* Open the vo file and write the magic number *)
-  let (f',ch) = raw_extern_library f in
+  let f' = f in
+  let ch = raw_extern_library f' in
   try
     (* Writing vo payload *)
+    System.marshal_out_segment f' ch (sd           : seg_sum);
     System.marshal_out_segment f' ch (md           : seg_lib);
     System.marshal_out_segment f' ch (utab         : seg_univ option);
     System.marshal_out_segment f' ch (dtab         : seg_discharge option);
@@ -789,19 +756,21 @@ let save_library_to ?todo dir f otab =
     System.marshal_out_segment f' ch (opaque_table : seg_proofs);
     close_out ch;
     (* Writing native code files *)
-    if not !Flags.no_native_compiler then
+    if !Flags.native_compiler then
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
       if not (Nativelib.compile_library dir ast fn) then
-        msg_error (str"Could not compile the library to native code. Skipping.")
+	error "Could not compile the library to native code."
    with reraise ->
     let reraise = Errors.push reraise in
-    let () = msg_warning (str ("Removed file "^f')) in
+    let () = msg_warning (str "Removed file " ++ str f') in
     let () = close_out ch in
     let () = Sys.remove f' in
     iraise reraise
 
-let save_library_raw f lib univs proofs =
-  let (f',ch) = raw_extern_library (f^"o") in
+let save_library_raw f sum lib univs proofs =
+  let f' = f^"o" in
+  let ch = raw_extern_library f' in
+  System.marshal_out_segment f' ch (sum        : seg_sum);
   System.marshal_out_segment f' ch (lib        : seg_lib);
   System.marshal_out_segment f' ch (Some univs : seg_univ option);
   System.marshal_out_segment f' ch (None       : seg_discharge option);
diff --git a/library/library.mli b/library/library.mli
index 35067068..d5e610dd 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -22,12 +22,11 @@ open Libnames
 (** Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
 val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
-val require_library_from_file :
-  Id.t option -> CUnix.physical_path -> bool option -> unit
 
-(** {6 ... } *)
+(** {6 Start the compilation of a library } *)
 
 (** Segments of a library *)
+type seg_sum
 type seg_lib
 type seg_univ = (* cst, all_cst, finished? *)
   Univ.universe_context_set Future.computation array * Univ.universe_context_set * bool
@@ -38,17 +37,19 @@ type seg_proofs = Term.constr Future.computation array
    an export otherwise just a simple import *)
 val import_module : bool -> qualid located list -> unit
 
-(** {6 Start the compilation of a library } *)
-val start_library : string -> DirPath.t * string
+(** 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. *)
+val start_library : CUnix.physical_path -> DirPath.t
 
-(** {6 End the compilation of a library and save it to a ".vo" file } *)
+(** End the compilation of a library and save it to a ".vo" file *)
 val save_library_to :
   ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
 val load_library_todo :
-  string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
-val save_library_raw : string -> seg_lib -> seg_univ -> seg_proofs -> unit
+  string -> string * seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
 
 (** {6 Interrogate the status of libraries } *)
 
diff --git a/library/library.mllib b/library/library.mllib
index eca28c82..92065736 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -16,5 +16,4 @@ Dischargedhypsmap
 Goptions
 Decls
 Heads
-Assumptions
 Keys
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 26af809e..622d390a 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -28,8 +28,6 @@ let physical p = p.path_physical
 
 let get_load_paths () = !load_paths
 
-let get_paths () = List.map physical !load_paths
-
 let anomaly_too_many_paths path =
   anomaly (str "Several logical paths are associated to" ++ spc () ++ str path)
 
@@ -112,3 +110,9 @@ let expand_path dir =
       if DirPath.equal dir lg then (ph, lg) :: aux l else aux l
   in
   aux !load_paths
+
+let locate_file fname =
+  let paths = List.map physical !load_paths in
+  let _,longfname =
+    System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
+  longfname
diff --git a/library/loadpath.mli b/library/loadpath.mli
index 3251b8c6..269e28e0 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -27,9 +27,6 @@ val logical : t -> DirPath.t
 val get_load_paths : unit -> t list
 (** Get the current loadpath association. *)
 
-val get_paths : unit -> CUnix.physical_path list
-(** Same as [get_load_paths] but only get the physical part. *)
-
 val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit
 (** [add_load_path phys log type] adds the binding [phys := log] to the current
     loadpaths. *)
@@ -52,3 +49,7 @@ val expand_path : DirPath.t -> (CUnix.physical_path * DirPath.t) list
 val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list
 (** As {!expand_path} but uses a filter function instead, and ignores the
     implicit status of loadpaths. *)
+
+val locate_file : string -> string
+(** Locate a file among the registered paths. Do not use this function, as
+    it does not respect the visibility of paths. *)
diff --git a/library/nameops.ml b/library/nameops.ml
index 02b085a7..3a23ab97 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -136,6 +136,11 @@ let name_fold_map f e = function
   | Name id -> let (e,id) = f e id in (e,Name id)
   | Anonymous -> e,Anonymous
 
+let name_max na1 na2 =
+  match na1 with
+  | Name _ -> na1
+  | Anonymous -> na2
+
 let pr_lab l = str (Label.to_string l)
 
 let default_library = Names.DirPath.initial (* = ["Top"] *)
diff --git a/library/nameops.mli b/library/nameops.mli
index 23432ae2..de1f99fe 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -34,7 +34,7 @@ val name_iter : (Id.t -> unit) -> Name.t -> unit
 val name_cons : Name.t -> Id.t list -> Id.t list
 val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
 val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
-
+val name_max : Name.t -> Name.t -> Name.t
 
 val pr_lab : Label.t -> Pp.std_ppcmds
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 6af1e686..5b6d7cd9 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -524,7 +524,8 @@ let shortest_qualid_of_tactic kn =
 
 let pr_global_env env ref =
   try str (string_of_qualid (shortest_qualid_of_global env ref))
-  with Not_found as e -> prerr_endline "pr_global_env not found"; raise e
+  with Not_found as e ->
+    if !Flags.debug then Pp.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 96a487b1..3cb6da12 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -21,18 +21,12 @@ let unfreeze (fl,fs) =
   Lib.unfreeze fl;
   Summary.unfreeze_summaries fs
 
-let (extern_state,intern_state) =
-  let ensure_suffix f = CUnix.make_suffix f ".coq" in
-  let (raw_extern, raw_intern) =
-    extern_intern Coq_config.state_magic_number in
-  (fun s ->
-    let s = ensure_suffix s in
-    raw_extern s (freeze ~marshallable:`Yes)),
-  (fun s ->
-    let s = ensure_suffix s in
-    let paths = Loadpath.get_paths () in
-    unfreeze (with_magic_number_check (raw_intern paths) s);
-    Library.overwrite_library_filenames s)
+let extern_state s =
+  System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:`Yes)
+
+let intern_state s =
+  unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
+  Library.overwrite_library_filenames s
 
 (* Rollback. *)
 
diff --git a/library/universes.ml b/library/universes.ml
index 9fddc706..6cccb10e 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -12,11 +12,14 @@ open Names
 open Term
 open Environ
 open Univ
+open Globnames
 
+(** Global universe names *)
 type universe_names = 
     Univ.universe_level Idmap.t * Id.t Univ.LMap.t
 
-let global_universes = Summary.ref ~name:"Global universe names" 
+let global_universes =
+  Summary.ref ~name:"Global universe names"
   ((Idmap.empty, Univ.LMap.empty) : universe_names)
 
 let global_universe_names () = !global_universes
@@ -26,6 +29,25 @@ let pr_with_global_universes l =
   try Nameops.pr_id (LMap.find l (snd !global_universes))
   with Not_found -> Level.pr l
 
+(** Local universe names of polymorphic references *)
+
+type universe_binders = (Id.t * Univ.universe_level) list
+
+let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
+
+let universe_binders_of_global ref =
+  try
+    let l = Refmap.find ref !universe_binders_table in l
+  with Not_found -> []
+
+let register_universe_binders ref l =
+  universe_binders_table := Refmap.add ref l !universe_binders_table
+		     
+(* To disallow minimization to Set *)
+
+let set_minimization = ref true
+let is_set_minimization () = !set_minimization
+			    
 type universe_constraint_type = ULe | UEq | ULub
 
 type universe_constraint = universe * universe_constraint_type * universe
@@ -139,6 +161,32 @@ let eq_constr_univs_infer univs m n =
     let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
       res, !cstrs
 
+(** 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 =
+  (* 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 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)
+  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
+
 let leq_constr_univs_infer univs m n =
   if m == n then true, Constraints.empty
   else 
@@ -148,15 +196,18 @@ let leq_constr_univs_infer univs m n =
       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)
+	if Univ.check_eq univs u1 u2 then true
+	else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
+	      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 true
+	  if Univ.check_leq univs u1 u2 then
+	    ((if Univ.is_small_univ u1 then
+		cstrs := Constraints.add (u1, ULe, u2) !cstrs);
+	     true)
 	  else
 	    (cstrs := Constraints.add (u1, ULe, u2) !cstrs; 
 	     true)
@@ -169,7 +220,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
+    res, !cstrs
 
 let eq_constr_universes m n =
   if m == n then true, Constraints.empty
@@ -188,7 +239,7 @@ let eq_constr_universes 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
+    res, !cstrs
 
 let leq_constr_universes m n =
   if m == n then true, Constraints.empty
@@ -216,22 +267,22 @@ let leq_constr_universes m n =
       Constr.compare_head_gen_leq eq_universes leq_sorts 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
+    res, !cstrs
 
 let compare_head_gen_proj env equ eqs eqc' m n =
   match kind_of_term m, kind_of_term n with
   | Proj (p, c), App (f, args)
   | App (f, args), Proj (p, c) -> 
-    (match kind_of_term f with
-    | Const (p', u) when eq_constant (Projection.constant p) p' -> 
-      let pb = Environ.lookup_projection p env in
-      let npars = pb.Declarations.proj_npars in
-	if Array.length args == npars + 1 then
-	  eqc' c args.(npars)
-	else false
-    | _ -> false)
+      (match kind_of_term f with
+      | Const (p', u) when eq_constant (Projection.constant p) p' -> 
+          let pb = Environ.lookup_projection p env in
+          let npars = pb.Declarations.proj_npars in
+	  if Array.length args == npars + 1 then
+	    eqc' c args.(npars)
+	  else false
+      | _ -> false)
   | _ -> Constr.compare_head_gen equ eqs eqc' m n
-    
+      
 let eq_constr_universes_proj env m n =
   if m == n then true, Constraints.empty
   else 
@@ -249,7 +300,7 @@ let eq_constr_universes_proj env m n =
       m == n ||	compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n
     in
     let res = eq_constr' m n in
-      res, !cstrs
+    res, !cstrs
 
 (* Generator of levels *)
 let new_univ_level, set_remote_new_univ_level =
@@ -697,7 +748,10 @@ let pr_constraints_map cmap =
       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 minimize_univ_variables ctx us algs left right cstrs =
   let left, lbounds = 
     Univ.LMap.fold (fun r lower (left, lbounds as acc)  ->
@@ -713,15 +767,14 @@ let minimize_univ_variables ctx us algs left right cstrs =
   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
-		(* if alg then assert(not alg); *)
-		let l' = 
-		  if enf then Universe.make l 
-		  else l' 
-		(* match Universe.level l' with Some _ -> l' | None -> Universe.make l  *)
-		in
-		  acc', (d, l') :: left') (acc, []) l
+	    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, []
     and right =
       try Some (LMap.find u right)
@@ -729,24 +782,22 @@ let minimize_univ_variables ctx us algs left right cstrs =
     in
     let instantiate_lbound lbound =
       let alg = LSet.mem u algs in
-      if alg then
-	 (* u is algebraic and has no upper bound constraints: we
-	    instantiate it with it's lower bound, if any *)
-	 instantiate_with_lbound u lbound 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. *)
-	  if not (Level.equal l u) && not (LSet.mem l algs) then
-	    (* if right = None then. Should check that u does not 
-	       have upper constraints that are not already in right *)
-	      instantiate_with_lbound u lbound false false acc
-	    (* else instantiate_with_lbound u lbound false true acc *)
-	  else
-	    (* assert false: l can't be alg *)
-	    acc, (true, false, lbound)
+	if alg then
+	  (* u is algebraic: we instantiate it with it's lower bound, if any, 
+              or enforce the constraints if it is bounded from the top. *)
+	  instantiate_with_lbound u lbound 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. *)
+	     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; *)
@@ -794,22 +845,63 @@ let minimize_univ_variables ctx us algs left right cstrs =
       if v == None then fst (aux acc u)
       else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs)
       us (ctx, us, algs, lbounds, cstrs)
-      
+
 let normalize_context_set ctx us algs = 
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   let uf = UF.create () in
+  (** Keep the Prop/Set <= i constraints separate for minimization *)
+  let smallles, csts =
+    Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) ->
+        if d == Le then
+	  if Univ.Level.is_small l then
+	    if is_set_minimization () then
+	      (Constraint.add cstr smallles, noneqs)
+	    else (smallles, noneqs)
+	  else if Level.is_small r then
+	    if Level.is_prop r then
+	      raise (Univ.UniverseInconsistency
+		       (Le,Universe.make l,Universe.make r,None))
+	    else (smallles, Constraint.add (l,Eq,r) noneqs)
+	  else (smallles, Constraint.add cstr noneqs)
+	else (smallles, Constraint.add cstr noneqs))
+    csts (Constraint.empty, Constraint.empty)
+  in
   let csts = 
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
-    let g = Univ.merge_constraints csts Univ.empty_universes in
+    let g = Univ.LSet.fold (fun v g -> Univ.add_universe v false g)
+			   ctx Univ.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
+	   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
+	   else g
+	 in g) csts g
+    in
+    let g = Univ.Constraint.fold Univ.enforce_constraint csts g in
       Univ.constraints_of_universes g
   in
   let noneqs =
-    Constraint.fold (fun (l,d,r) noneqs ->
-      if d == Eq then (UF.union l r uf; noneqs) 
-      else Constraint.add (l,d,r) noneqs)
-    csts Constraint.empty
+    Constraint.fold (fun (l,d,r as cstr) noneqs ->
+      if d == Eq then (UF.union l r uf; noneqs)
+      else (* We ignore the trivial Prop/Set <= i constraints. *)
+	if d == Le && Univ.Level.is_small l then noneqs
+	else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r
+	then noneqs
+	else Constraint.add cstr noneqs)
+      csts Constraint.empty
   in
+  let noneqs = Constraint.union noneqs smallles in
   let partition = UF.partition uf in
   let flex x = LMap.mem x us in
   let ctx, subst, eqs = List.fold_left (fun (ctx, subst, cstrs) s -> 
@@ -819,7 +911,7 @@ let normalize_context_set ctx us algs =
       Constraint.add (canon, Univ.Eq, g) cst) global
       cstrs 
     in
-    let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in 
+    let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in
     let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in 
       (LSet.diff (LSet.diff ctx rigid) flexible, subst, cstrs))
     (ctx, LMap.empty, Constraint.empty) partition
@@ -915,12 +1007,12 @@ let simplify_universe_context (univs,csts) =
   let csts' = subst_univs_level_constraints subst csts' in
     (univs', csts'), subst
 
-let is_small_leq (l,d,r) =
-  Level.is_small l && d == Univ.Le
+let is_trivial_leq (l,d,r) =
+  Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r))
 
 (* Prop < i <-> Set+1 <= i <-> Set < i *)
 let translate_cstr (l,d,r as cstr) =
-  if Level.equal Level.prop l && d == Univ.Lt then
+  if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then
     (Level.set, d, r)
   else cstr
 
@@ -928,7 +1020,7 @@ let refresh_constraints univs (ctx, cstrs) =
   let cstrs', univs' = 
     Univ.Constraint.fold (fun c (cstrs', univs as acc) -> 
       let c = translate_cstr c in
-      if Univ.check_constraint univs c && not (is_small_leq c) then acc
+      if is_trivial_leq c then acc
       else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
       cstrs (Univ.Constraint.empty, univs)
   in ((ctx, cstrs'), univs')
@@ -995,13 +1087,14 @@ let solve_constraints_system levels level_bounds level_min =
   for i=0 to nind-1 do
     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))
+	(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 -> v.(i) <- univ_level_rem u v.(i) level_min.(i)
-      | None -> ()
-    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 252648d7..45672ef4 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -12,8 +12,12 @@ open Term
 open Environ
 open Univ
 
+val set_minimization : bool ref
+val is_set_minimization : unit -> bool
+
 (** Universes *)
 
+(** Global universe name <-> level mapping *)
 type universe_names = 
   Univ.universe_level Idmap.t * Id.t Univ.LMap.t
 
@@ -22,6 +26,13 @@ val set_global_universe_names : universe_names -> unit
 
 val pr_with_global_universes : Level.t -> Pp.std_ppcmds
 
+(** Local universe name <-> level mapping *)
+
+type universe_binders = (Id.t * Univ.universe_level) list
+					   
+val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
+val universe_binders_of_global : Globnames.global_reference -> universe_binders
+
 (** The global universe counter *)
 val set_remote_new_univ_level : universe_level RemoteCounter.installer
 
@@ -66,6 +77,14 @@ val to_constraints : universes -> universe_constraints -> constraints
    application grouping, the universe constraints in [u] and additional constraints [c]. *)
 val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
 
+(** [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
+    subterms of [m] and [n], arguments. *)
+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
+
 (** [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]. *)