Imported Upstream snapshot 8.3~beta0+13298

35 files changed, 1801 insertions, 1929 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index d6dfbb6b..5fd27f46 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_kinds.ml 11809 2009-01-20 11:39:55Z aspiwack $ *)
+(* $Id$ *)
 
 open Util
 open Libnames
@@ -44,7 +44,7 @@ type definition_object_kind =
 
 type assumption_object_kind = Definitional | Logical | Conjectural
 
-(* [assumption_kind] 
+(* [assumption_kind]
 
                 |  Local      | Global
    ------------------------------------
diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli
index 70c63c39..0ebab9ca 100644
--- a/library/decl_kinds.mli
+++ b/library/decl_kinds.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_kinds.mli 11809 2009-01-20 11:39:55Z aspiwack $ *)
+(* $Id$ *)
 
 open Util
 open Libnames
@@ -44,7 +44,7 @@ type definition_object_kind =
 
 type assumption_object_kind = Definitional | Logical | Conjectural
 
-(* [assumption_kind] 
+(* [assumption_kind]
 
                 |  Local      | Global
    ------------------------------------
diff --git a/library/declare.ml b/library/declare.ml
index c349bef1..3e4853c8 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: declare.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id$ *)
 
 (** This module is about the low-level declaration of logical objects *)
 
@@ -27,11 +27,17 @@ open Cooking
 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 *)
+
 (** XML output hooks *)
 
 let xml_declare_variable = ref (fun (sp:object_name) -> ())
-let xml_declare_constant = ref (fun (sp:bool * constant)-> ())
-let xml_declare_inductive = ref (fun (sp:bool * object_name) -> ())
+let xml_declare_constant = ref (fun (sp:internal_flag * constant)-> ())
+let xml_declare_inductive = ref (fun (sp:internal_flag * object_name) -> ())
 
 let if_xml f x = if !Flags.xml_export then f x else ()
 
@@ -39,11 +45,14 @@ let set_xml_declare_variable f = xml_declare_variable := if_xml f
 let set_xml_declare_constant f = xml_declare_constant := if_xml f
 let set_xml_declare_inductive f = xml_declare_inductive := if_xml f
 
+let cache_hook = ref ignore
+let add_cache_hook f = cache_hook := f
+
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep *)
+  | SectionLocalAssum of types * bool (* Implicit status *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
@@ -53,18 +62,17 @@ let cache_variable ((sp,_),o) =
   | Inr (id,(p,d,mk)) ->
   (* Constr raisonne sur les noms courts *)
   if variable_exists id then
-    errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
-  let impl,opaq,cst,keep = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum (ty, impl, keep) ->
+    alreadydeclared (pr_id id ++ str " already exists");
+  let impl,opaq,cst = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum (ty, impl) ->
         let cst = Global.push_named_assum (id,ty) in
 	let impl = if impl then Lib.Implicit else Lib.Explicit in
-	let keep = if keep <> [] then Some (ty, keep) else None in
-	impl, true, cst, keep
-    | SectionLocalDef (c,t,opaq) -> 
+	impl, true, cst
+    | SectionLocalDef (c,t,opaq) ->
         let cst = Global.push_named_def (id,c,t) in
-        Lib.Explicit, opaq, cst, None in
+        Lib.Explicit, opaq, cst in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
-  add_section_variable id impl keep;
+  add_section_variable id impl;
   Dischargedhypsmap.set_discharged_hyps sp [];
   add_variable_data id (p,opaq,cst,mk)
 
@@ -72,7 +80,7 @@ let discharge_variable (_,o) = match o with
   | Inr (id,_) -> Some (Inl (variable_constraints id))
   | Inl _ -> Some o
 
-let (inVariable, outVariable) =
+let (inVariable,_) =
   declare_object { (default_object "VARIABLE") with
     cache_function = cache_variable;
     discharge_function = discharge_variable;
@@ -87,6 +95,7 @@ let declare_variable id obj =
   !xml_declare_variable oname;
   oname
 
+
 (** Declaration of constants and parameters *)
 
 type constant_declaration = constant_entry * logical_kind
@@ -95,26 +104,28 @@ type constant_declaration = constant_entry * logical_kind
 (* section (if Remark or Fact) is needed to access a construction *)
 let load_constant i ((sp,kn),(_,_,kind)) =
   if Nametab.exists_cci sp then
-    errorlabstrm "cache_constant" 
-      (pr_id (basename sp) ++ str " already exists");
-  Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn));
-  add_constant_kind (constant_of_kn kn) kind
+    alreadydeclared (pr_id (basename sp) ++ str " already exists");
+  let con = Global.constant_of_delta (constant_of_kn kn) in
+  Nametab.push (Nametab.Until i) sp (ConstRef con);
+  add_constant_kind con kind
 
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn),_) =
-  Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn))
+  let con = Global.constant_of_delta (constant_of_kn kn) in
+    Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
 let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
   if variable_exists id or Nametab.exists_cci sp then
-    errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+    alreadydeclared (pr_id id ++ str " already exists");
   let kn' = Global.add_constant dir id cdt in
   assert (kn' = constant_of_kn kn);
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   add_section_constant kn' (Global.lookup_constant kn').const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
-  add_constant_kind (constant_of_kn kn) kind
+  add_constant_kind (constant_of_kn kn) kind;
+  !cache_hook sp
 
 let discharged_hyps kn sechyps =
   let (_,dir,_) = repr_kn kn in
@@ -134,19 +145,16 @@ let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false))
 
 let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk
 
-let export_constant cst = Some (dummy_constant cst)
-
-let classify_constant (_,cst) = Substitute (dummy_constant cst)
+let classify_constant cst = Substitute (dummy_constant cst)
 
-let (inConstant, outConstant) =
+let (inConstant,_) =
   declare_object { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
     open_function = open_constant;
     classify_function = classify_constant;
     subst_function = ident_subst_function;
-    discharge_function = discharge_constant;
-    export_function = export_constant } 
+    discharge_function = discharge_constant }
 
 let hcons_constant_declaration = function
   | DefinitionEntry ce when !Flags.hash_cons_proofs ->
@@ -154,17 +162,17 @@ let hcons_constant_declaration = function
       DefinitionEntry
        { const_entry_body = hcons1_constr ce.const_entry_body;
 	 const_entry_type = Option.map hcons1_constr ce.const_entry_type;
-         const_entry_opaque = ce.const_entry_opaque; 
+         const_entry_opaque = ce.const_entry_opaque;
          const_entry_boxed = ce.const_entry_boxed }
   | cd -> cd
 
 let declare_constant_common id dhyps (cd,kind) =
   let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in
-  let kn = constant_of_kn kn in
-  declare_constant_implicits kn;
-  Heads.declare_head (EvalConstRef kn);
-  Notation.declare_ref_arguments_scope (ConstRef kn);
-  kn
+  let c = Global.constant_of_delta (constant_of_kn kn) in
+  declare_constant_implicits c;
+  Heads.declare_head (EvalConstRef c);
+  Notation.declare_ref_arguments_scope (ConstRef c);
+  c
 
 let declare_constant_gen internal id (cd,kind) =
   let cd = hcons_constant_declaration cd in
@@ -172,8 +180,10 @@ let declare_constant_gen internal id (cd,kind) =
   !xml_declare_constant (internal,kn);
   kn
 
-let declare_internal_constant = declare_constant_gen true
-let declare_constant = declare_constant_gen false
+(* TODO: add a third function to distinguish between KernelVerbose
+ * and user Verbose *)
+let declare_internal_constant = declare_constant_gen KernelSilent
+let declare_constant = declare_constant_gen UserVerbose
 
 (** Declaration of inductive blocks *)
 
@@ -186,14 +196,15 @@ let declare_inductive_argument_scopes kn mie =
 
 let inductive_names sp kn mie =
   let (dp,_) = repr_path sp in
-  let names, _ = 
+  let kn = Global.mind_of_delta (mind_of_kn kn) in
+  let names, _ =
     List.fold_left
       (fun (names, n) ind ->
 	 let ind_p = (kn,n) in
 	 let names, _ =
 	   List.fold_left
 	     (fun (names, p) l ->
-		let sp = 
+		let sp =
 		  Libnames.make_path dp l
 		in
 		  ((sp, ConstructRef (ind_p,p)) :: names, p+1))
@@ -206,16 +217,15 @@ let inductive_names sp kn mie =
 
 let check_exists_inductive (sp,_) =
   (if variable_exists (basename sp) then
-    errorlabstrm ""
-      (pr_id (basename sp) ++ str " already exists"));
+    alreadydeclared (pr_id (basename sp) ++ str " already exists"));
   if Nametab.exists_cci sp then
     let (_,id) = repr_path sp in
-    errorlabstrm "" (pr_id id ++ str " already exists")
+    alreadydeclared (pr_id id ++ str " already exists")
 
 let load_inductive i ((sp,kn),(_,mie)) =
   let names = inductive_names sp kn mie in
   List.iter check_exists_inductive names;
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref) names
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
 
 let open_inductive i ((sp,kn),(_,mie)) =
   let names = inductive_names sp kn mie in
@@ -227,15 +237,18 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
   let kn' = Global.add_mind dir id mie in
-  assert (kn'=kn);
-  add_section_kn kn (Global.lookup_mind kn').mind_hyps;
+  assert (kn'= mind_of_kn kn);
+  add_section_kn kn' (Global.lookup_mind kn').mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names;
+  List.iter (fun (sp,_) -> !cache_hook sp) (inductive_names sp kn mie)
+
 
 let discharge_inductive ((sp,kn),(dhyps,mie)) =
-  let mie = Global.lookup_mind kn in
+  let mind = (Global.mind_of_delta (mind_of_kn kn)) in
+  let mie = Global.lookup_mind mind in
   let repl = replacement_context () in
-  let sechyps = section_segment_of_mutual_inductive kn in
+  let sechyps = section_segment_of_mutual_inductive mind in
   Some (discharged_hyps kn sechyps,
         Discharge.process_inductive (named_of_variable_context sechyps) repl mie)
 
@@ -253,17 +266,14 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_finite = true;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
 
-let export_inductive x = Some (dummy_inductive_entry x)
-
-let (inInductive, outInductive) =
-  declare_object {(default_object "INDUCTIVE") with 
+let (inInductive,_) =
+  declare_object {(default_object "INDUCTIVE") with
     cache_function = cache_inductive;
     load_function = load_inductive;
     open_function = open_inductive;
-    classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a));
+    classify_function = (fun a -> Substitute (dummy_inductive_entry a));
     subst_function = ident_subst_function;
-    discharge_function = discharge_inductive;
-    export_function = export_inductive } 
+    discharge_function = discharge_inductive }
 
 (* for initial declaration *)
 let declare_mind isrecord mie =
@@ -271,8 +281,43 @@ let declare_mind isrecord mie =
     | ind::_ -> ind.mind_entry_typename
     | [] -> anomaly "cannot declare an empty list of inductives" in
   let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
-  declare_mib_implicits kn;
-  declare_inductive_argument_scopes kn mie;
+  let mind = (Global.mind_of_delta (mind_of_kn kn)) in
+  declare_mib_implicits mind;
+  declare_inductive_argument_scopes mind mie;
   !xml_declare_inductive (isrecord,oname);
   oname
 
+(* Declaration messages *)
+
+let pr_rank i = str (ordinal (i+1))
+
+let fixpoint_message indexes l =
+  Flags.if_verbose msgnl (match l with
+  | [] -> anomaly "no recursive definition"
+  | [id] -> pr_id id ++ str " is recursively defined" ++
+      (match indexes with
+	 | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
+	 | _ -> mt ())
+  | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
+		  spc () ++ str "are recursively defined" ++
+		  match indexes with
+		    | Some a -> spc () ++ str "(decreasing respectively on " ++
+			prlist_with_sep pr_comma pr_rank (Array.to_list a) ++
+			str " arguments)"
+		    | None -> mt ()))
+
+let cofixpoint_message l =
+  Flags.if_verbose msgnl (match l with
+  | [] -> anomaly "No corecursive definition."
+  | [id] -> pr_id id ++ str " is corecursively defined"
+  | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
+                    spc () ++ str "are corecursively defined"))
+
+let recursive_message isfix i l =
+  (if isfix then fixpoint_message i else cofixpoint_message) l
+
+let definition_message id =
+  Flags.if_verbose msgnl (pr_id id ++ str " is defined")
+
+let assumption_message id =
+  Flags.if_verbose msgnl (pr_id id ++ str " is assumed")
diff --git a/library/declare.mli b/library/declare.mli
index 2f1cd06e..12e323f1 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declare.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -21,11 +21,11 @@ open Nametab
 open Decl_kinds
 (*i*)
 
-(* This module provides the official functions to declare new variables, 
+(* This module provides the official functions to declare new variables,
    parameters, constants and inductive types. Using the following functions
    will add the entries in the global environment (module [Global]), will
    register the declarations in the library (module [Lib]) --- so that the
-   reset works properly --- and will fill some global tables such as 
+   reset works properly --- and will fill some global tables such as
    [Nametab] and [Impargs]. *)
 
 open Nametab
@@ -34,7 +34,7 @@ open Nametab
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep list *)
+  | SectionLocalAssum of types * bool (* Implicit status *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
@@ -48,6 +48,11 @@ type constant_declaration = 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 *)
+type internal_flag =
+  | KernelVerbose
+  | KernelSilent
+  | UserVerbose
+
 val declare_constant :
  identifier -> constant_declaration -> constant
 
@@ -57,9 +62,22 @@ val declare_internal_constant :
 (* [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
    the whole block (boolean must be true iff it is a record) *)
-val declare_mind : bool -> mutual_inductive_entry -> object_name
+val declare_mind : internal_flag -> mutual_inductive_entry -> object_name
 
-(* hooks for XML output *)
+(* Hooks for XML output *)
 val set_xml_declare_variable : (object_name -> unit) -> unit
-val set_xml_declare_constant : (bool * constant -> unit) -> unit
-val set_xml_declare_inductive : (bool * object_name -> unit) -> unit
+val set_xml_declare_constant : (internal_flag * constant -> unit) -> unit
+val set_xml_declare_inductive : (internal_flag * object_name -> unit) -> unit
+
+(* Hook for the cache function of constants and inductives *)
+val add_cache_hook : (full_path -> unit) -> unit
+
+(* Declaration messages *)
+
+val definition_message : identifier -> unit
+val assumption_message : identifier -> unit
+val fixpoint_message : int array option -> identifier list -> unit
+val cofixpoint_message : identifier list -> unit
+val recursive_message : bool (* true = fixpoint *) ->
+  int array option -> identifier list -> unit
+
diff --git a/library/declaremods.ml b/library/declaremods.ml
index cfada00c..4449c531 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.ml 12295 2009-08-27 11:01:49Z soubiran $ i*)
+(*i $Id$ i*)
+
 open Pp
 open Util
 open Names
@@ -21,7 +22,7 @@ open Mod_subst
 (* modules and components *)
 
 
-(* This type is a functional closure of substitutive lib_objects.
+(* OBSOLETE This type is a functional closure of substitutive lib_objects.
 
    The first part is a partial substitution (which will be later
    applied to lib_objects when completed).
@@ -39,157 +40,161 @@ open Mod_subst
    therefore must be substitued with valid names before use.
 
 *)
-type substitutive_objects = 
-    substitution * mod_bound_id list * mod_self_id * lib_objects
+type substitutive_objects =
+     mod_bound_id list * module_path * lib_objects
 
 
 (* For each module, we store the following things:
 
-   In modtab_substobjs: substitutive_objects 
-     when we will do Module M:=N, the objects of N will be reloaded 
+   In modtab_substobjs: substitutive_objects
+     when we will do Module M:=N, the objects of N will be reloaded
      with M after substitution
 
    In modtab_objects: "substituted objects" @ "keep objects"
 
-   substituted objects - 
-     roughly the objects above after the substitution - we need to 
+   substituted objects -
+     roughly the objects above after the substitution - we need to
      keep them to call open_object when the module is opened (imported)
- 
+
    keep objects -
-     The list of non-substitutive objects - as above, for each of 
-     them we will call open_object when the module is opened 
-     
+     The list of non-substitutive objects - as above, for each of
+     them we will call open_object when the module is opened
+
    (Some) Invariants:
    * If the module is a functor, the two latter lists are empty.
 
-   * Module objects in substitutive_objects part have empty substituted 
+   * Module objects in substitutive_objects part have empty substituted
      objects.
 
-   * Modules which where created with Module M:=mexpr or with 
+   * Modules which where created with Module M:=mexpr or with
      Module M:SIG. ... End M. have the keep list empty.
 *)
-let modtab_substobjs = 
+let modtab_substobjs =
   ref (MPmap.empty : substitutive_objects MPmap.t)
-let modtab_objects = 
+let modtab_objects =
   ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t)
 
 
 (* currently started interactive module (if any) - its arguments (if it
    is a functor) and declared output type *)
-let openmod_info = 
-  ref (([],None,None) : mod_bound_id list * module_struct_entry option 
-                                          * struct_expr_body option) 
+let openmod_info =
+  ref ((MPfile(initial_dir),[],None,[])
+	 : module_path *  mod_bound_id list *
+           (module_struct_entry * bool) option * module_type_body list)
 
 (* The library_cache here is needed to avoid recalculations of
    substituted modules object during "reloading" of libraries *)
 let library_cache = ref Dirmap.empty
 
 let _ = Summary.declare_summary "MODULE-INFO"
-	  { Summary.freeze_function = (fun () -> 
+	  { Summary.freeze_function = (fun () ->
 					 !modtab_substobjs,
 					 !modtab_objects,
 					 !openmod_info,
 					 !library_cache);
-	    Summary.unfreeze_function = (fun (sobjs,objs,info,libcache) -> 
+	    Summary.unfreeze_function = (fun (sobjs,objs,info,libcache) ->
 					   modtab_substobjs := sobjs;
 					   modtab_objects := objs;
 					   openmod_info := info;
 					   library_cache := libcache);
-	    Summary.init_function = (fun () -> 
+	    Summary.init_function = (fun () ->
 				       modtab_substobjs := MPmap.empty;
 				       modtab_objects := MPmap.empty;
-				       openmod_info := ([],None,None);
-				       library_cache := Dirmap.empty);
-	    Summary.survive_module = false;
-	    Summary.survive_section = false }
+				       openmod_info := ((MPfile(initial_dir),
+							 [],None,[]));
+				       library_cache := Dirmap.empty) }
 
-(* auxiliary functions to transform section_path and kernel_name given
+(* auxiliary functions to transform full_path and kernel_name given
    by Lib into module_path and dir_path needed for modules *)
 
-let mp_of_kn kn = 
-  let mp,sec,l = repr_kn kn in 
-    if sec=empty_dirpath then 
-      MPdot (mp,l) 
+let mp_of_kn kn =
+  let mp,sec,l = repr_kn kn in
+    if sec=empty_dirpath then
+      MPdot (mp,l)
     else
       anomaly ("Non-empty section in module name!" ^ string_of_kn kn)
 
-let is_bound mp =
-  match mp with
-    | MPbound _ -> true
-    | _ -> false
-
-let dir_of_sp sp = 
+let dir_of_sp sp =
   let dir,id = repr_path sp in
-    extend_dirpath dir id
+    add_dirpath_suffix dir id
 
-let msid_of_mp = function
-    MPself msid -> msid
-  | _ -> anomaly "'Self' module path expected!"
+(* Subtyping checks *)
 
-let msid_of_prefix (_,(mp,sec)) = 
-  if sec=empty_dirpath then 
-    msid_of_mp mp
-  else
-    anomaly ("Non-empty section in module name!" ^ 
-	     string_of_mp mp ^ "." ^ string_of_dirpath sec)
-
-let scrape_alias mp =
-  Environ.scrape_alias mp (Global.env())
-	
+let check_sub mtb sub_mtb_l =
+  (* The constraints are checked and forgot immediately : *)
+  ignore (List.fold_right
+	    (fun sub_mtb env ->
+	       Environ.add_constraints
+		 (Subtyping.check_subtypes env mtb sub_mtb) env)
+	    sub_mtb_l (Global.env()))
 
 (* This function checks if the type calculated for the module [mp] is
-   a subtype of [sub_mtb]. Uses only the global environment. *)
-let check_subtypes mp sub_mtb =
-  let env = Global.env () in
-  let mtb = Environ.lookup_modtype mp env in
-  let sub_mtb = 
-    {typ_expr = sub_mtb;
-    typ_strength = None;
-    typ_alias = empty_subst} in
-  let _ = Environ.add_constraints 
-	    (Subtyping.check_subtypes env mtb sub_mtb) 
-  in
-    ()  (* The constraints are checked and forgot immediately! *) 
+   a subtype of all signatures in [sub_mtb_l]. Uses only the global
+   environment. *)
 
-let compute_subst_objects mp (subst,mbids,msid,objs) =
-  match mbids with
-  | [] -> 
-      let subst' = join_alias (map_msid msid mp) subst in
-      Some (join (map_msid msid mp) (join subst' subst), objs)
-  | _ ->
-      None
+let check_subtypes mp sub_mtb_l =
+  let env = Global.env () in
+  let mb = Environ.lookup_module mp env in
+  let mtb = Modops.module_type_of_module env None mb in
+  check_sub mtb sub_mtb_l
+
+(* Same for module type [mp] *)
+
+let check_subtypes_mt mp sub_mtb_l =
+  check_sub (Environ.lookup_modtype mp (Global.env())) sub_mtb_l
+
+(* Create a functor type entry *)
+
+let funct_entry args m =
+  List.fold_right
+    (fun (arg_id,(arg_t,_)) mte -> MSEfunctor (arg_id,arg_t,mte))
+    args m
+
+(* Prepare the module type list for check of subtypes *)
+
+let build_subtypes interp_modtype mp args mtys =
+  List.map
+    (fun (m,inl) ->
+       let mte = interp_modtype (Global.env()) m in
+       let mtb = Mod_typing.translate_module_type (Global.env()) mp inl mte in
+       let funct_mtb =
+	 List.fold_right
+           (fun (arg_id,(arg_t,arg_inl)) mte ->
+              let arg_t =
+		Mod_typing.translate_module_type (Global.env())
+		  (MPbound arg_id) arg_inl arg_t
+	      in
+              SEBfunctor(arg_id,arg_t,mte))
+           args mtb.typ_expr
+       in
+       { mtb with typ_expr = funct_mtb })
+    mtys
 
-let subst_substobjs dir mp substobjs =
-  match compute_subst_objects mp substobjs with
-  | Some (subst, objs) ->
-	let prefix = dir,(mp,empty_dirpath) in
-	Some (subst_objects prefix subst objs)
-  | None -> None
 
 (* These functions register the visibility of the module and iterates
    through its components. They are called by plenty module functions *)
 
 let compute_visibility exists what i dir dirinfo =
-  if exists then 
-    if 
-      try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo 
-      with Not_found -> false 
+  if exists then
+    if
+      try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo
+      with Not_found -> false
     then
       Nametab.Exactly i
     else
       errorlabstrm (what^"_module")
-	(pr_dirpath dir ++ str " should already exist!") 
+	(pr_dirpath dir ++ str " should already exist!")
   else
     if Nametab.exists_dir dir then
       errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
     else
       Nametab.Until i
-
+(*
 let do_load_and_subst_module i dir mp substobjs keep =
   let prefix = (dir,(mp,empty_dirpath)) in
   let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
   let vis = compute_visibility false "load_and_subst" i dir dirinfo in
-  let objects = compute_subst_objects mp substobjs in
+  let objects = compute_subst_objects mp substobjs resolver in
   Nametab.push_dir vis dir dirinfo;
   modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
   match objects with
@@ -200,101 +205,63 @@ let do_load_and_subst_module i dir mp substobjs keep =
       Some (seg@keep)
   | None ->
       None
+*)
 
-let do_module exists what iter_objects i dir mp substobjs objects =
+let do_module exists what iter_objects i dir mp substobjs keep=
   let prefix = (dir,(mp,empty_dirpath)) in
   let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
   let vis = compute_visibility exists what i dir dirinfo in
     Nametab.push_dir vis dir dirinfo;
     modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
-    match objects with
-	Some seg -> 
-	  modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects;
-	  iter_objects (i+1) prefix seg	  
-      | None ->  ()
-
-let conv_names_do_module exists what iter_objects i 
-      (sp,kn) substobjs substituted =
+    match substobjs with
+	([],mp1,objs) -> 
+	  modtab_objects := MPmap.add mp (prefix,objs@keep) !modtab_objects;
+	  iter_objects (i+1) prefix (objs@keep)  
+      | (mbids,_,_) ->  ()
+
+let conv_names_do_module exists what iter_objects i
+      (sp,kn) substobjs =
   let dir,mp = dir_of_sp sp, mp_of_kn kn in
-  do_module exists what iter_objects i dir mp substobjs substituted
+  do_module exists what iter_objects i dir mp substobjs []
 
 (* Interactive modules and module types cannot be recached! cache_mod*
    functions can be called only once (and "end_mod*" set the flag to
    false then)
 *)
-
-let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) =
-  let _ = match entry with
-    | None ->
-	anomaly "You must not recache interactive modules!"
-    | Some (me,sub_mte_o) ->
-	let sub_mtb_o = match sub_mte_o with 
-	    None -> None
-	  | Some mte -> Some (Mod_typing.translate_struct_entry
-				(Global.env()) mte)
-	in
-	  
-	let mp = Global.add_module (basename sp) me in
-	  if mp <> mp_of_kn kn then
-	    anomaly "Kernel and Library names do not match";
-	  
-	  match sub_mtb_o with
-	      None -> ()
-	    | Some (sub_mtb,sub) -> 
-		check_subtypes mp sub_mtb
-
-  in
-  conv_names_do_module false "cache" load_objects 1 oname substobjs substituted
-
-
-
-
+let cache_module ((sp,kn),(entry,substobjs)) =
+  let dir,mp = dir_of_sp sp, mp_of_kn kn in
+    do_module false "cache" load_objects 1 dir mp substobjs []
+    
 (* TODO: This check is not essential *)
 let check_empty s = function
      | None -> ()
-     | Some _ -> 
+     | Some _ ->
 	 anomaly ("We should never have full info in " ^ s^"!")
 
 
 (* When this function is called the module itself is already in the
    environment. This function loads its objects only *)
 
-let load_module i (oname,(entry,substobjs,substituted)) =
+let load_module i (oname,(entry,substobjs)) =
   (* TODO: This check is not essential *)
   check_empty "load_module" entry;
-  conv_names_do_module false "load" load_objects i oname substobjs substituted
+  conv_names_do_module false "load" load_objects i oname substobjs
 
 
-let open_module i (oname,(entry,substobjs,substituted)) =
+let open_module i (oname,(entry,substobjs)) =
   (* TODO: This check is not essential *)
   check_empty "open_module" entry;
-  conv_names_do_module true "open" open_objects i oname substobjs substituted
+  conv_names_do_module true "open" open_objects i oname substobjs
 
 
 
-let subst_module ((sp,kn),subst,(entry,substobjs,_)) =
+let subst_module (subst,(entry,(mbids,mp,objs))) =
   check_empty "subst_module" entry;
-  let dir,mp = dir_of_sp sp, mp_of_kn kn in
-  let (sub,mbids,msid,objs) = substobjs in
-  let sub = subst_key subst sub in
-  let sub' = update_subst_alias subst sub in
-  let sub' = update_subst_alias sub' (map_msid msid mp) in
- (* let sub = join_alias sub sub' in*)
-  let sub = join sub' sub in
-  let subst' = join sub subst in
-  (* substitutive_objects get the new substitution *)
-  let substobjs = (subst',mbids,msid,objs) in
-  (* if we are not a functor - calculate substitued.
-     We add "msid |-> mp" to the substitution *)
-  let substituted = subst_substobjs dir mp substobjs
-  in
-    (None,substobjs,substituted)
-
-
-let classify_module (_,(_,substobjs,_)) =
-  Substitute (None,substobjs,None)
+    (None,(mbids,subst_mp subst mp, subst_objects subst objs))
 
 
+let classify_module (_,substobjs) =
+  Substitute (None,substobjs)
 
 let (in_module,out_module) =
   declare_object {(default_object "MODULE") with
@@ -302,182 +269,17 @@ let (in_module,out_module) =
     load_function = load_module;
     open_function = open_module;
     subst_function = subst_module;
-    classify_function = classify_module;
-    export_function = (fun _ -> anomaly "No modules in sections!") }
-
-
-let rec replace_alias modalias_obj obj =
-  let rec put_alias (id_alias,obj_alias) l =
-    match l with 
-	[] -> []
-      | (id,o)::r 
-	  when ( object_tag o = "MODULE") ->
-	  if id = id_alias then
-(*	    let (entry,subst_o,substed_o) = out_module_alias obj_alias in
-	    let (entry',subst_o',substed_o') = out_module o in
-	      begin
-		match substed_o,substed_o' with
-		    Some a,Some b ->
-		      (id,in_module_alias 
-			 (entry,subst_o',Some (dump_alias_object a b)))::r*)
-	    (id_alias,obj_alias)::r
-		 (* | _,_ -> (id,o)::r
-	      end*)
-	  else (id,o)::(put_alias (id_alias,obj_alias) r)
-      | e::r -> e::(put_alias (id_alias,obj_alias) r) in
-  let rec choose_obj_alias list_alias list_obj =
-    match list_alias with
-      | [] -> list_obj
-      | o::r ->choose_obj_alias r (put_alias o list_obj) in
-    choose_obj_alias modalias_obj obj
-	  
-and dump_alias_object alias_obj obj =
-  let rec alias_in_obj seg =
-    match seg with
-      | [] -> []
-      | (id,o)::r when (object_tag o = "MODULE ALIAS") -> 
-	  (id,o)::(alias_in_obj r)
-      | e::r -> (alias_in_obj r) in
-  let modalias_obj = alias_in_obj alias_obj in
-    replace_alias modalias_obj obj
-      
-and do_module_alias exists what iter_objects i dir mp alias substobjs objects =
-  let prefix = (dir,(alias,empty_dirpath)) in
-  let alias_objects = 
-    try Some (MPmap.find alias !modtab_objects) with
-	Not_found -> None in
-  let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
-  let vis = compute_visibility exists what i dir dirinfo in
-    Nametab.push_dir vis dir dirinfo;
-    modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
-    match alias_objects,objects with
-	Some (_,seg), Some seg' -> 
-	  let new_seg = dump_alias_object seg seg' in
-	  modtab_objects := MPmap.add mp (prefix,new_seg) !modtab_objects;
-	  iter_objects (i+1) prefix new_seg 	  
-      | _,_->  ()
-
-and cache_module_alias ((sp,kn),(entry,substobjs,substituted)) =
-  let dir,mp,alias = match entry with
-    | None ->
-	anomaly "You must not recache interactive modules!"
-    | Some (me,sub_mte_o) ->
-	let sub_mtb_o = match sub_mte_o with 
-	    None -> None
-	  | Some mte -> Some (Mod_typing.translate_struct_entry
-				(Global.env()) mte)
-	in
-
-	let mp' = match me with 
-	  | {mod_entry_type = None;
-	     mod_entry_expr = Some (MSEident mp)} ->
-	      Global.add_alias (basename sp) mp	 
-	  | _ -> anomaly "cache module alias"
-	in
-	  if mp' <> mp_of_kn kn then
-	    anomaly "Kernel and Library names do not match";
-	  
-	  let _ = match sub_mtb_o with
-	      None -> ()
-	    | Some (sub_mtb,sub) -> 
-	      check_subtypes mp' sub_mtb in
-	    match me with
-	      | {mod_entry_type = None;
-		 mod_entry_expr = Some (MSEident mp)} ->
-		    dir_of_sp sp,mp_of_kn kn,scrape_alias mp		
-	      | _ -> anomaly "cache module alias"
-  in
-    do_module_alias false "cache" load_objects 1 dir mp alias substobjs substituted
-
-and load_module_alias i ((sp,kn),(entry,substobjs,substituted)) =
-  let dir,mp,alias= 
-    match entry with 
-      | Some (me,_)->
-	  begin
-	    match me with
-	      |{mod_entry_type = None;
-		mod_entry_expr = Some (MSEident mp)} ->
-		 dir_of_sp sp,mp_of_kn kn,scrape_alias mp
-	      | _ -> anomaly "Modops: Not an alias"
-	  end
-      | None -> anomaly "Modops: Empty info"
-  in
-    do_module_alias false "load" load_objects i dir mp alias substobjs substituted
-
-and open_module_alias i ((sp,kn),(entry,substobjs,substituted)) =
-  let dir,mp,alias=
-    match entry with 
-      | Some (me,_)->
-	  begin
-	    match me with
-	      |{mod_entry_type = None;
-		mod_entry_expr = Some (MSEident mp)} ->
-		 dir_of_sp sp,mp_of_kn kn,scrape_alias mp
-	      | _ -> anomaly "Modops: Not an alias"
-	  end
-      | None -> anomaly "Modops: Empty info"
-  in
-    do_module_alias true "open" open_objects i dir mp alias substobjs substituted
-
-and subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) =
-  let dir,mp = dir_of_sp sp, mp_of_kn kn in
-  let (sub,mbids,msid,objs) = substobjs in
-  let sub' = update_subst_alias subst (map_msid msid mp) in
-  let subst' = join sub' subst in
-  let subst' = join sub subst' in
-  (* substitutive_objects get the new substitution *)
-  let substobjs = (subst',mbids,msid,objs) in
-  (* if we are not a functor - calculate substitued.
-     We add "msid |-> mp" to the substitution *)
-    match entry with 
-      | Some (me,sub)->
-	  begin
-	    match me with
-	      |{mod_entry_type = None;
-		mod_entry_expr = Some (MSEident mp')} ->
-		 let mp' = subst_mp subst' mp' in
-		 let mp' = scrape_alias mp' in
-		   (Some ({mod_entry_type = None;
-			 mod_entry_expr = 
-			      Some (MSEident mp')},sub),
-		    substobjs, match mbids with
-		      | [] -> let subst = update_subst subst' (map_mp mp' mp) in
-			  Some (subst_objects (dir,(mp',empty_dirpath)) 
-				  (join (join subst' subst) (join (map_msid msid mp')
-						  (map_mp mp mp')))
-				   objs)
-			    
-		      | _ -> None)
-		     
-	      | _ -> anomaly "Modops: Not an alias"
-	  end
-      | None -> anomaly "Modops: Empty info"
-
-and classify_module_alias (_,(entry,substobjs,_)) =
-  Substitute (entry,substobjs,None)
-	        
-let (in_module_alias,out_module_alias) =
-  declare_object {(default_object "MODULE ALIAS") with
-		    cache_function = cache_module_alias;
-		    open_function = open_module_alias;
-		    classify_function = classify_module_alias;
-		    subst_function = subst_module_alias;
-		    load_function = load_module_alias;  
-		    export_function = (fun _ -> anomaly "No modules in sections!") }
-    
-
-
-
+    classify_function = classify_module }
 
 let cache_keep _ = anomaly "This module should not be cached!"
 
-let load_keep i ((sp,kn),seg) = 
+let load_keep i ((sp,kn),seg) =
   let mp = mp_of_kn kn in
   let prefix = dir_of_sp sp, (mp,empty_dirpath) in
-    begin 
+    begin
       try
 	let prefix',objects = MPmap.find mp !modtab_objects in
-	  if prefix' <> prefix then 
+	  if prefix' <> prefix then
 	    anomaly "Two different modules with the same path!";
 	  modtab_objects := MPmap.add mp (prefix,objects@seg) !modtab_objects;
       with
@@ -485,16 +287,15 @@ let load_keep i ((sp,kn),seg) =
     end;
     load_objects i prefix seg
 
-let open_keep i ((sp,kn),seg) = 
+let open_keep i ((sp,kn),seg) =
   let dirpath,mp = dir_of_sp sp, mp_of_kn kn in
     open_objects i (dirpath,(mp,empty_dirpath)) seg
 
-let (in_modkeep,out_modkeep) = 
+let (in_modkeep,_) =
   declare_object {(default_object "MODULE KEEP OBJECTS") with
     cache_function = cache_keep;
     load_function = load_keep;
-    open_function = open_keep;
-    export_function = (fun _ -> anomaly "No modules in sections!") }
+    open_function = open_keep }
 
 (* we remember objects for a module type. In case of a declaration:
    Module M:SIG:=...
@@ -506,7 +307,7 @@ let modtypetab =
 (* currently started interactive module type. We remember its arguments
    if it is a functor type *)
 let openmodtype_info =
-  ref ([] : mod_bound_id list)
+  ref ([],[] : mod_bound_id list * module_type_body list)
 
 let _ = Summary.declare_summary "MODTYPE-INFO"
 	  { Summary.freeze_function = (fun () ->
@@ -516,261 +317,253 @@ let _ = Summary.declare_summary "MODTYPE-INFO"
 					   openmodtype_info := snd ft);
 	    Summary.init_function = (fun () ->
 				       modtypetab := MPmap.empty;
-				       openmodtype_info := []);
-	    Summary.survive_module = false;
-	    Summary.survive_section = true }
+				       openmodtype_info := [],[]) }
 
 
-let cache_modtype ((sp,kn),(entry,modtypeobjs)) =
-  let _ = 
+let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
+  let mp = mp_of_kn kn in
+
+  let _ =
     match entry with
       | None ->
 	  anomaly "You must not recache interactive module types!"
-      | Some mte ->
-	  let mp = Global.add_modtype (basename sp) mte in
-	  if mp <>mp_of_kn kn then
+      | Some (mte,inl) ->
+	  if mp <> Global.add_modtype (basename sp) mte inl then
 	    anomaly "Kernel and Library names do not match"
   in
 
+  (* Using declare_modtype should lead here, where we check
+     that any given subtyping is indeed accurate *)
+  check_subtypes_mt mp sub_mty_l;
+
   if Nametab.exists_modtype sp then
     errorlabstrm "cache_modtype"
-      (pr_sp sp ++ str " already exists") ;
+      (pr_path sp ++ str " already exists") ;
 
-  Nametab.push_modtype (Nametab.Until 1) sp (mp_of_kn kn);
+  Nametab.push_modtype (Nametab.Until 1) sp mp;
 
-  modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab
+  modtypetab := MPmap.add mp modtypeobjs !modtypetab
 
 
-let load_modtype i ((sp,kn),(entry,modtypeobjs)) =
+let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) =
   check_empty "load_modtype" entry;
 
   if Nametab.exists_modtype sp then
     errorlabstrm "cache_modtype"
-      (pr_sp sp ++ str " already exists") ;
+      (pr_path sp ++ str " already exists") ;
 
   Nametab.push_modtype (Nametab.Until i) sp (mp_of_kn kn);
-    
+
   modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab
 
 
-let open_modtype i ((sp,kn),(entry,_)) =
+let open_modtype i ((sp,kn),(entry,_,_)) =
   check_empty "open_modtype" entry;
 
-  if 
-    try Nametab.locate_modtype (qualid_of_sp sp) <> (mp_of_kn kn) 
+  if
+    try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn)
     with Not_found -> true
   then
-    errorlabstrm ("open_modtype") 
-      (pr_sp sp ++ str " should already exist!");
+    errorlabstrm ("open_modtype")
+      (pr_path sp ++ str " should already exist!");
 
   Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn)
 
-let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) =
+let subst_modtype (subst,(entry,(mbids,mp,objs),_)) =
   check_empty "subst_modtype" entry;
-  (entry,(join subs subst,mbids,msid,objs))
+  (entry,(mbids,subst_mp subst mp,subst_objects subst objs),[])
 
 
-let classify_modtype (_,(_,substobjs)) =
-  Substitute (None,substobjs)
+let classify_modtype (_,substobjs,_) =
+  Substitute (None,substobjs,[])
 
 
-let (in_modtype,out_modtype) =
+let (in_modtype,_) =
     declare_object {(default_object "MODULE TYPE") with
       cache_function = cache_modtype;
       open_function = open_modtype;
       load_function = load_modtype;
       subst_function = subst_modtype;
-      classify_function = classify_modtype;
-      export_function = Option.make }
+      classify_function = classify_modtype }
 
 
-
-let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp =
-  let rec mp_rec = function
-    | [] -> MPself msid
-	| i::r -> MPdot(mp_rec r,label_of_id i)
-  in 
-    if mbids<>[] then 
+let rec replace_module_object idl ( mbids, mp, lib_stack) (mbids2,mp2,objs) mp1=
+  if mbids<>[] then 
     error "Unexpected functor objects"
-    else
-      let rec replace_idl = function 
-	| _,[] -> [] 
-	| id::idl,(id',obj)::tail when id = id' ->
-	    let tag = object_tag obj in
-	    if tag = "MODULE" or tag ="MODULE ALIAS" then
-              (match idl with
-		   [] -> (id, in_module_alias (Some
-						 ({mod_entry_type = None;
-						   mod_entry_expr = Some (MSEident mp)},None)
-						 ,modobjs,None))::tail
-		 | _ ->
-		     let (a,substobjs,_) = if tag =  "MODULE ALIAS" then
-		       out_module_alias obj else out_module obj in
-                     let substobjs' = replace_module_object idl substobjs modobjs mp in
-  		       if tag =  "MODULE ALIAS" then
-			 (id, in_module_alias (a,substobjs',None))::tail
-		       else
-			 (id, in_module (None,substobjs',None))::tail
-              )
-	    else error "MODULE expected!"
-	| idl,lobj::tail -> lobj::replace_idl (idl,tail)
-      in
-	(join (map_mp (mp_rec (List.rev idl)) mp) subst, mbids, msid, replace_idl (idl,lib_stack))
-	  
-let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) =
-  (subst, mbids1@mbids2, msid, lib_stack)
-
-let rec get_modtype_substobjs env = function
-    MSEident ln -> MPmap.find ln !modtypetab
+  else
+    let rec replace_idl = function 
+      | _,[] -> [] 
+      | id::idl,(id',obj)::tail when id = id' ->
+	  if object_tag obj = "MODULE" then
+           (match idl with
+               [] -> (id, in_module 
+			(None,(mbids,(MPdot(mp,label_of_id id)),subst_objects 
+				 (map_mp mp1 (MPdot(mp,label_of_id id)) empty_delta_resolver) objs)))::tail
+             | _ ->
+               let (_,substobjs) = out_module obj in
+                let substobjs' = replace_module_object idl substobjs 
+		  (mbids2,mp2,objs) mp in
+                  (id, in_module (None,substobjs'))::tail
+           )
+	  else error "MODULE expected!"
+      | idl,lobj::tail -> lobj::replace_idl (idl,tail)
+    in
+      (mbids, mp, replace_idl (idl,lib_stack))
+
+let discr_resolver mb  = 
+     match mb.mod_type with
+	SEBstruct _ -> 
+	  Some mb.mod_delta
+      | _ -> (*case mp is a functor *)
+	  None
+
+(* Small function to avoid module typing during substobjs retrivial  *)
+let rec get_objs_modtype_application env = function
+| MSEident mp -> 
+    MPmap.find mp !modtypetab,Environ.lookup_modtype mp env,[]
+| MSEapply (fexpr, MSEident mp) -> 
+    let objs,mtb,mp_l= get_objs_modtype_application env fexpr in
+      objs,mtb,mp::mp_l
+| MSEapply (_,mexpr) ->
+    Modops.error_application_to_not_path mexpr
+| _ -> error "Application of a non-functor."
+
+let rec compute_subst env mbids sign mp_l inline =
+  match mbids,mp_l with
+    | _,[] -> mbids,empty_subst
+    | [],r -> error "Application of a functor with too few arguments."
+    | mbid::mbids,mp::mp_l ->
+	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
+	let mb = Environ.lookup_module mp env in
+	let mbid_left,subst = compute_subst env mbids fbody_b mp_l inline in
+	match discr_resolver mb with
+	  | None ->
+	      mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst
+	  | Some mp_delta ->
+	      let mp_delta =
+		if not inline then mp_delta else
+		  Modops.complete_inline_delta_resolver env mp
+		    farg_id farg_b mp_delta
+	      in
+	      mbid_left,join (map_mbid mbid mp mp_delta) subst
+
+let rec get_modtype_substobjs env mp_from inline = function
+    MSEident ln -> 
+      MPmap.find ln !modtypetab 
   | MSEfunctor (mbid,_,mte) ->
-      let (subst, mbids, msid, objs) = get_modtype_substobjs env mte in
-	(subst, mbid::mbids, msid, objs)
-  | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mty
-  | MSEwith (mty, With_Module (idl,mp)) -> 
-      let substobjs = get_modtype_substobjs env mty in
-      let mp = Environ.scrape_alias mp env in
-      let modobjs = MPmap.find mp !modtab_substobjs in
-	replace_module_object idl substobjs modobjs mp
-  | MSEapply (mexpr, MSEident mp) ->
-     let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in
-      let farg_id, farg_b, fbody_b = Modops.destr_functor env 
-	(Modops.eval_struct env ftb) in
-      let mp = Environ.scrape_alias mp env in
-      let sub_alias = (Environ.lookup_modtype mp env).typ_alias in
-      let sub_alias = match Modops.eval_struct env (SEBident mp) with
-	| SEBstruct (msid,sign) -> join_alias 
-	    (subst_key (map_msid msid mp) sub_alias)
-	      (map_msid msid mp)
-	| _ -> sub_alias in
-      let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in
-      let mbid,mbids= (match mbids with
-	   | mbid::mbids -> mbid,mbids
-	   | [] -> match mexpr with
-	       | MSEident _  -> error "Application of a non-functor"
-	       | _ -> error "Application of a functor with too few arguments") in
-      let resolve =
-	Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
-      let sub3=
-	if sub1 = empty_subst then
-	  update_subst sub_alias (map_mbid farg_id mp (Some resolve))
-	else
-	  let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in
-	  let sub_alias' =  update_subst sub_alias sub1' in
-	    join sub1' sub_alias'
+      let (mbids, mp, objs) = get_modtype_substobjs env mp_from inline mte in
+	(mbid::mbids, mp, objs)
+  | MSEwith (mty, With_Definition _) ->
+      get_modtype_substobjs env mp_from inline mty
+  | MSEwith (mty, With_Module (idl,mp1)) -> 
+      let substobjs = get_modtype_substobjs env mp_from inline mty in
+      let modobjs = MPmap.find mp1 !modtab_substobjs in
+	replace_module_object idl substobjs modobjs mp1
+  | MSEapply (fexpr, MSEident mp) as me ->
+      let (mbids, mp1, objs),mtb_mp1,mp_l =
+	get_objs_modtype_application env me in
+      let mbids_left,subst =
+	compute_subst env mbids mtb_mp1.typ_expr (List.rev mp_l) inline
       in
-      let sub3 = join sub3 
-	(update_subst sub_alias (map_mbid farg_id mp (Some resolve))) in
-	(* application outside the kernel, only for substitutive
-           objects (that are all non-logical objects) *)
-	((join 
-	    (join subst sub3)
-	    (map_mbid mbid mp (Some resolve)))
-	   , mbids, msid, objs)
+      (mbids_left, mp1,subst_objects subst objs)
   | MSEapply (_,mexpr) ->
       Modops.error_application_to_not_path mexpr
 
- 
 (* push names of bound modules (and their components) to Nametab *)
 (* add objects associated to them *)
 let process_module_bindings argids args =
-  let process_arg id (mbid,mty) =
+  let process_arg id (mbid,(mty,inl)) =
     let dir = make_dirpath [id] in
     let mp = MPbound mbid in
-    let substobjs = get_modtype_substobjs (Global.env()) mty in
-    ignore (do_load_and_subst_module 1 dir mp substobjs [])
-  in
-    List.iter2 process_arg argids args
-
-let intern_args interp_modtype (idl,arg) = 
+    let (mbids,mp_from,objs) =
+      get_modtype_substobjs (Global.env()) mp inl mty in
+    let substobjs = (mbids,mp,subst_objects
+		       (map_mp mp_from mp empty_delta_resolver) objs)in
+      do_module false "start" load_objects 1 dir mp substobjs []
+    in
+      List.iter2 process_arg argids args
+
+let intern_args interp_modtype (idl,(arg,inl)) =
   let lib_dir = Lib.library_dp() in
   let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
   let mty = interp_modtype (Global.env()) arg in
   let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
-  let substobjs = get_modtype_substobjs (Global.env()) mty in
+  let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env())
+    (MPbound (List.hd mbids)) inl mty in
   List.map2
-    (fun dir mbid -> 
-      Global.add_module_parameter mbid mty;
-      let mp = MPbound mbid in
-      ignore (do_load_and_subst_module 1 dir mp substobjs []);
-      (mbid,mty))
+    (fun dir mbid ->
+       let resolver = Global.add_module_parameter mbid mty inl in
+       let mp = MPbound mbid in
+       let substobjs = (mbi,mp,subst_objects
+			  (map_mp mp_from mp resolver) objs) in
+	 do_module false "interp" load_objects 1 dir mp substobjs [];
+	 (mbid,(mty,inl)))
     dirs mbids
 
-let start_module interp_modtype export id args res_o =
-  let fs = Summary.freeze_summaries () in
-
+let start_module_ interp_modtype export id args res fs =
   let mp = Global.start_module id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-
-  let res_entry_o, sub_body_o = match res_o with
-      None -> None, None
-    | Some (res, restricted) ->
-	(* we translate the module here to catch errors as early as possible *)
+  let res_entry_o, sub_body_l = match res with
+    | Topconstr.Enforce (res,inl) ->
 	let mte = interp_modtype (Global.env()) res in
-	if restricted then
-	  Some mte, None
-	else
-	  let mtb,_ = Mod_typing.translate_struct_entry (Global.env()) mte in
-	  let sub_mtb = 
-	    List.fold_right 
-	      (fun (arg_id,arg_t) mte -> 
-		let arg_t,sub = Mod_typing.translate_struct_entry (Global.env()) arg_t
-		in
-		let arg_t = {typ_expr = arg_t;
-			     typ_strength = None;
-			     typ_alias = sub} in
-		  SEBfunctor(arg_id,arg_t,mte))
-	      arg_entries mtb
-	  in
-	  None, Some sub_mtb
+	let _ = Mod_typing.translate_struct_type_entry (Global.env()) inl mte in
+	Some (mte,inl), []
+    | Topconstr.Check resl ->
+	None, build_subtypes interp_modtype mp arg_entries resl
   in
-
   let mbids = List.map fst arg_entries in
-    openmod_info:=(mbids,res_entry_o,sub_body_o);
+  openmod_info:=(mp,mbids,res_entry_o,sub_body_l);
   let prefix = Lib.start_module export id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
   Lib.add_frozen_state (); mp
 
 
-let end_module id =
+let end_module () =
 
-  let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in
-  let mbids, res_o, sub_o = !openmod_info in
+  let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in
+  let mp,mbids, res_o, sub_l = !openmod_info in
   let substitute, keep, special = Lib.classify_segment lib_stack in
 
-  let dir = fst oldprefix in
-  let msid = msid_of_prefix oldprefix in
-
-  let substobjs, keep, special = try
+  let mp_from,substobjs, keep, special = try
     match res_o with
-      | None -> 
-	  (empty_subst, mbids, msid, substitute), keep, special
-      | Some (MSEident ln) ->
-	  abstract_substobjs mbids (MPmap.find ln (!modtypetab)), [], []
-      | Some (MSEwith _ as mty) ->
-	  abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], []
-      | Some (MSEfunctor _) -> 
+      | None ->
+	  (* the module is not sealed *)
+	  None,( mbids, mp, substitute), keep, special
+      | Some (MSEident ln as mty, inline) ->
+	  let (mbids1,mp1,objs) =
+	    get_modtype_substobjs (Global.env()) mp inline mty in
+	  Some mp1,(mbids@mbids1,mp1,objs), [], []
+      | Some (MSEwith _ as mty, inline) ->
+	  let (mbids1,mp1,objs) =
+	    get_modtype_substobjs (Global.env()) mp inline mty in
+	  Some mp1,(mbids@mbids1,mp1,objs), [], []
+      | Some (MSEfunctor _, _) ->
 	  anomaly "Funsig cannot be here..."
-      | Some (MSEapply _ as mty) ->
-	  abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], []
+      | Some (MSEapply _ as mty, inline) ->
+	  let (mbids1,mp1,objs) =
+	    get_modtype_substobjs (Global.env()) mp inline mty in
+	  Some mp1,(mbids@mbids1,mp1,objs), [], []
   with
 	Not_found -> anomaly "Module objects not found..."
   in
     (* must be called after get_modtype_substobjs, because of possible
      dependencies on functor arguments *)
 
-  let mp = Global.end_module id res_o in
+  let id = basename (fst oldoname) in
+  let mp,resolver = Global.end_module fs id res_o in
 
-  begin match sub_o with
-      None -> ()
-    | Some sub_mtb -> check_subtypes mp sub_mtb
-  end;
+  check_subtypes mp sub_l;
 
-  Summary.module_unfreeze_summaries fs;
-
-  let substituted = subst_substobjs dir mp substobjs in
-  let node = in_module (None,substobjs,substituted) in
-  let objects = 
-    if keep = [] || mbids <> [] then 
+(* we substitute objects if the module is 
+   sealed by a signature (ie. mp_from != None *)
+  let substobjs = match mp_from,substobjs with
+      None,_ -> substobjs
+    | Some mp_from,(mbids,_,objs) ->
+	(mbids,mp,subst_objects (map_mp mp_from mp resolver) objs) 
+  in
+  let node = in_module (None,substobjs) in
+  let objects =
+    if keep = [] || mbids <> [] then
       special@[node]   (* no keep objects or we are defining a functor *)
     else
       special@[node;in_modkeep keep]   (* otherwise *)
@@ -779,7 +572,7 @@ let end_module id =
 
     if (fst newoname) <> (fst oldoname) then
       anomaly "Names generated on start_ and end_module do not match";
-    if mp_of_kn (snd newoname) <> mp then 
+    if mp_of_kn (snd newoname) <> mp then
       anomaly "Kernel and Library names do not match";
 
     Lib.add_frozen_state () (* to prevent recaching *);
@@ -787,7 +580,7 @@ let end_module id =
 
 
 
-let module_objects mp = 
+let module_objects mp =
   let prefix,objects = MPmap.find mp !modtab_objects in
     segment_of_objects prefix objects
 
@@ -799,63 +592,67 @@ let module_objects mp =
 type library_name = dir_path
 
 (* The first two will form substitutive_objects, the last one is keep *)
-type library_objects = 
-    mod_self_id * lib_objects * lib_objects
+type library_objects =
+    module_path * lib_objects * lib_objects
 
 
 let register_library dir cenv objs digest =
   let mp = MPfile dir in
+  let substobjs, keep =
   try 
     ignore(Global.lookup_module mp);
     (* if it's in the environment, the cached objects should be correct *)
-    let substobjs, objects = Dirmap.find dir !library_cache in
-    do_module false "register_library" load_objects 1 dir mp substobjs objects
+    Dirmap.find dir !library_cache
   with Not_found ->
     if mp <> Global.import cenv digest then
       anomaly "Unexpected disk module name";
-    let msid,substitute,keep = objs in
-    let substobjs = empty_subst, [], msid, substitute in
-    let objects = do_load_and_subst_module 1 dir mp substobjs keep in
-    let modobjs = substobjs, objects in
-    library_cache := Dirmap.add dir modobjs !library_cache
+    let mp,substitute,keep = objs in
+    let substobjs = [], mp, substitute in
+    let modobjs = substobjs, keep in
+    library_cache := Dirmap.add dir modobjs !library_cache;
+      modobjs
+  in
+    do_module false "register_library" load_objects 1 dir mp substobjs keep
 
-let start_library dir = 
+let start_library dir =
   let mp = Global.start_library dir in
-  openmod_info:=[],None,None;
+  openmod_info:=mp,[],None,[];
   Lib.start_compilation dir mp;
   Lib.add_frozen_state ()
 
+let end_library_hook = ref ignore
+let set_end_library_hook f = end_library_hook := f
 
-let end_library dir = 
+let end_library dir =
+  !end_library_hook();
   let prefix, lib_stack = Lib.end_compilation dir in
-  let cenv = Global.export dir in
-  let msid = msid_of_prefix prefix in
+  let mp,cenv = Global.export dir in
   let substitute, keep, _ = Lib.classify_segment lib_stack in
-    cenv,(msid,substitute,keep)
+    cenv,(mp,substitute,keep)
 
 
 (* implementation of Export M and Import M *)
 
 
-let really_import_module mp = 
+let really_import_module mp =
   let prefix,objects = MPmap.find mp !modtab_objects in
     open_objects 1 prefix objects
 
 
-let cache_import (_,(_,mp)) = 
-(* for non-substitutive exports: 
+let cache_import (_,(_,mp)) =
+(* for non-substitutive exports:
   let mp = Nametab.locate_module (qualid_of_dirpath dir) in  *)
   really_import_module mp
 
-let classify_import (_,(export,_ as obj)) = 
+let classify_import (export,_ as obj) =
   if export then Substitute obj else Dispose
 
-let subst_import (_,subst,(export,mp as obj)) =
-  let mp' = subst_mp subst mp in
+let subst_import (subst,(export,mp as obj)) =
+   let mp' = subst_mp subst mp in
     if mp'==mp then obj else
       (export,mp')
-	
-let (in_import,out_import) = 
+
+let (in_import,_) =
   declare_object {(default_object "IMPORT MODULE") with
 		    cache_function = cache_import;
 		    open_function = (fun i o -> if i=1 then cache_import o);
@@ -863,125 +660,89 @@ let (in_import,out_import) =
 		    classify_function = classify_import }
 
 
-let import_module export mp = 
+let import_module export mp =
   Lib.add_anonymous_leaf (in_import (export,mp))
 
 (************************************************************************)
 (* module types *)
-let start_modtype interp_modtype id args =
-  let fs = Summary.freeze_summaries () in
 
+let start_modtype_ interp_modtype id args mtys fs =
   let mp = Global.start_modtype id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-
+  let sub_mty_l = build_subtypes interp_modtype mp arg_entries mtys in
   let mbids = List.map fst arg_entries in
-  openmodtype_info := mbids;
+  openmodtype_info := mbids, sub_mty_l;
   let prefix = Lib.start_modtype id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
   Lib.add_frozen_state (); mp
 
 
-let end_modtype id =
-
-  let oldoname,prefix,fs,lib_stack = Lib.end_modtype id in
-  let ln = Global.end_modtype id in
+let end_modtype () =
+  let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in
+  let id = basename (fst oldoname) in
   let substitute, _, special = Lib.classify_segment lib_stack in
-
-  let msid = msid_of_prefix prefix in
-  let mbids = !openmodtype_info in
-
-  Summary.module_unfreeze_summaries fs;
-
-  let modtypeobjs = empty_subst, mbids, msid, substitute in
-
-  let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs)]) in
+  let mbids, sub_mty_l = !openmodtype_info in
+  let mp = Global.end_modtype fs id in
+  let modtypeobjs = mbids, mp, substitute in
+  check_subtypes_mt mp sub_mty_l;
+  let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs,[])])
+  in
   if fst oname <> fst oldoname then
     anomaly
       "Section paths generated on start_ and end_modtype do not match";
-  if (mp_of_kn (snd oname)) <> ln then
+  if (mp_of_kn (snd oname)) <> mp then
     anomaly
       "Kernel and Library names do not match";
 
   Lib.add_frozen_state ()(* to prevent recaching *);
-  ln
-
+  mp
 
-let declare_modtype interp_modtype id args mty = 
-  let fs = Summary.freeze_summaries () in
 
-  try
+let declare_modtype_ interp_modtype id args mtys (mty,inl) fs =
   let mmp = Global.start_modtype id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-
-  let base_mty = interp_modtype (Global.env()) mty in
-  let entry = 
-    List.fold_right 
-      (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte))
-      arg_entries
-      base_mty
-  in
-  let substobjs = get_modtype_substobjs (Global.env()) entry in
+  let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in
+  (* NB: check of subtyping will be done in cache_modtype *)
+  let sub_mty_l = build_subtypes interp_modtype mmp arg_entries mtys in
+  let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mmp inl entry in
   (* Undo the simulated interactive building of the module type *)
   (* and declare the module type as a whole *)
+
+  let substobjs = (mbids,mmp,
+		   subst_objects (map_mp mp_from mmp empty_delta_resolver) objs)
+  in
   Summary.unfreeze_summaries fs;
-    
-  ignore (add_leaf id (in_modtype (Some entry, substobjs)));
+  ignore (add_leaf id (in_modtype (Some (entry,inl), substobjs, sub_mty_l)));
   mmp
-  with e ->
-    (* Something wrong: undo the whole process *)
-    Summary.unfreeze_summaries fs; raise e
-			       
 
-let rec get_module_substobjs env = function
-  | MSEident mp -> MPmap.find mp !modtab_substobjs 
+
+(* Small function to avoid module typing during substobjs retrivial  *)
+let rec get_objs_module_application env = function
+| MSEident mp -> 
+    MPmap.find mp !modtab_substobjs,Environ.lookup_module mp env,[]
+| MSEapply (fexpr, MSEident mp) -> 
+    let objs,mtb,mp_l= get_objs_module_application env fexpr in
+      objs,mtb,mp::mp_l
+| MSEapply (_,mexpr) ->
+    Modops.error_application_to_not_path mexpr
+| _ -> error "Application of a non-functor."
+
+
+let rec get_module_substobjs env mp_from inl = function
+  | MSEident mp -> MPmap.find mp !modtab_substobjs
   | MSEfunctor (mbid,mty,mexpr) ->
-       let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
-	(subst, mbid::mbids, msid, objs)
-  | MSEapply (mexpr, MSEident mp) ->
-      let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in
-      let farg_id, farg_b, fbody_b = Modops.destr_functor env 
-	(Modops.eval_struct env ftb) in
-      let mp = Environ.scrape_alias mp env in
-      let sub_alias = (Environ.lookup_modtype mp env).typ_alias in
-      let sub_alias = match Modops.eval_struct env (SEBident mp) with
-	| SEBstruct (msid,sign) -> join_alias 
-	    (subst_key (map_msid msid mp) sub_alias)
-	      (map_msid msid mp)
-	| _ -> sub_alias in
-      let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
-      let mbid,mbids = 
-	(match mbids with
-	   | mbid::mbids ->mbid,mbids
-	       
-	   | [] -> match mexpr with
-	       | MSEident _  -> error "Application of a non-functor"
-	       | _ -> error "Application of a functor with too few arguments") in
-      let resolve =
-	Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
-      let sub3=
-	if sub1 = empty_subst then
-	  update_subst sub_alias (map_mbid farg_id mp (Some resolve))
-	else
-	  let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in
-	  let sub_alias' =  update_subst sub_alias sub1' in
-		     join sub1' sub_alias'
+       let (mbids, mp, objs) = get_module_substobjs env mp_from inl mexpr in
+	(mbid::mbids, mp, objs)
+  | MSEapply (fexpr, MSEident mp) as me ->
+      let (mbids, mp1, objs),mb_mp1,mp_l =
+	get_objs_module_application env me
       in
-      let sub3 = join sub3 (update_subst sub_alias 
-			      (map_mbid farg_id mp (Some resolve))) in
-	(* application outside the kernel, only for substitutive
-           objects (that are all non-logical objects) *)
-	((join 
-	    (join subst sub3)
-	    (map_mbid mbid mp (Some resolve)))
-	   , mbids, msid, objs)
-  | MSEapply (_,mexpr) ->
-      Modops.error_application_to_not_path mexpr
-  | MSEwith (mty, With_Definition _) -> get_module_substobjs env mty
-  | MSEwith (mty, With_Module (idl,mp)) -> 
-      let substobjs = get_module_substobjs env mty in
-      let modobjs = MPmap.find mp !modtab_substobjs in
-	replace_module_object idl substobjs modobjs mp
-
+      let mbids_left,subst =
+	compute_subst env mbids mb_mp1.mod_type (List.rev mp_l) inl in
+      (mbids_left, mp1,subst_objects subst objs)
+  | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr
+  | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from inl mty
+  | MSEwith (mty, With_Module (idl,mp)) -> assert false
 
 (* Include *)
 
@@ -995,58 +756,43 @@ let rec subst_inc_expr subst me =
 	let const1 = Mod_subst.from_val const in
 	let force = Mod_subst.force subst_mps in
 	MSEwith (subst_inc_expr subst me,
-		 With_Definition(idl,force (subst_substituted 
+		 With_Definition(idl,force (subst_substituted
 					   subst const1)))
-    | MSEapply (me1,me2) -> 
+    | MSEapply (me1,me2) ->
 	MSEapply (subst_inc_expr subst me1,
 		  subst_inc_expr subst me2)
-    | _ -> anomaly "You cannot Include a high-order structure"
+    | MSEfunctor(mbid,me1,me2) ->
+        MSEfunctor (mbid, subst_inc_expr subst me1, subst_inc_expr subst me2)
 
 let lift_oname (sp,kn) =
   let mp,_,_ = Names.repr_kn kn in
   let dir,_ = Libnames.repr_path sp in
     (dir,mp)
 
-let cache_include (oname,((me,is_mod),substobjs,substituted)) =
+let cache_include (oname,((me,is_mod),(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
-    Global.add_include me;
-    match substituted with
-	Some seg -> 
-	  load_objects 1 prefix seg;
-	  open_objects 1 prefix seg; 
-      | None ->  ()
-	  
-let load_include  i (oname,((me,is_mod),substobjs,substituted)) =
+    load_objects 1 prefix objs;
+    open_objects 1 prefix objs 
+    
+let load_include  i (oname,((me,is_mod),(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
-    match substituted with
-	Some seg -> 
-	  load_objects i prefix seg
-      | None ->  ()
-
-let open_include i (oname,((me,is_mod),substobjs,substituted)) =
+    load_objects i prefix objs
+      
+      
+let open_include i (oname,((me,is_mod),(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
-    match substituted with
-	Some seg -> 
-	  if is_mod then
-	  open_objects i prefix seg
-	  else 
-	    if i = 1 then	  
-	      open_objects i prefix seg
-      | None ->  ()
-
-let subst_include (oname,subst,((me,is_mod),substobj,_)) =
-  let dir,mp1 = lift_oname oname in
-  let (sub,mbids,msid,objs) = substobj in
-  let subst' = join sub subst in
-  let substobjs = (subst',mbids,msid,objs) in
-  let substituted = subst_substobjs dir mp1 substobjs in
-    ((subst_inc_expr subst' me,is_mod),substobjs,substituted)
-
-let classify_include (_,((me,is_mod),substobjs,_)) =
-  Substitute ((me,is_mod),substobjs,None)
+    open_objects i prefix objs
+      
+let subst_include (subst,((me,is_mod),substobj)) =
+  let (mbids,mp,objs) = substobj in
+  let substobjs = (mbids,subst_mp subst mp,subst_objects subst objs) in
+    ((subst_inc_expr subst me,is_mod),substobjs)
+      
+let classify_include ((me,is_mod),substobjs) =
+  Substitute ((me,is_mod),substobjs)
 
 let (in_include,out_include) =
   declare_object {(default_object "INCLUDE") with
@@ -1054,137 +800,182 @@ let (in_include,out_include) =
     load_function = load_include;
     open_function = open_include;
     subst_function = subst_include;
-    classify_function = classify_include;
-    export_function = (fun _ -> anomaly "No modules in section!") }
-
-let rec update_include (sub,mbids,msid,objs) =
-  let rec replace_include = function
-    | [] -> [] 
-    | (id,obj)::tail ->
-	if object_tag obj = "INCLUDE" then
-	  let ((me,is_mod),substobjs,substituted) = out_include obj in
-	  let substobjs' = update_include substobjs in
-            (id, in_include ((me,true),substobjs',substituted))::
-	      (replace_include tail)
-	else
-	  (id,obj)::(replace_include tail)
-  in
-    (sub,mbids,msid,replace_include objs)
-      
-      
-      
-let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
-  
-  let fs = Summary.freeze_summaries () in
+    classify_function = classify_include }
 
-  try
+
+let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   let mmp = Global.start_module id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
 
-  let mty_entry_o, mty_sub_o = match mty_o with
-      None -> None, None
-    | (Some (mty, true)) -> 
-	Some (List.fold_right 
-		(fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte))
-		arg_entries 
-		(interp_modtype (Global.env()) mty)), 
-	None
-    | (Some (mty, false)) -> 
-	None, 
-	Some (List.fold_right 
-		(fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte))
-		arg_entries 
-		(interp_modtype (Global.env()) mty))
+  let funct f m = funct_entry arg_entries (f (Global.env ()) m) in
+  let env = Global.env() in
+  let mty_entry_o, subs, inl_res = match res with
+    | Topconstr.Enforce (mty,inl) -> Some (funct interp_modtype mty), [], inl
+    | Topconstr.Check mtys ->
+	None, build_subtypes interp_modtype mmp arg_entries mtys, true
   in
-  let mexpr_entry_o = match mexpr_o with
-      None -> None
-    | Some mexpr -> 
-	Some (List.fold_right 
-		(fun (mbid,mte) me -> MSEfunctor(mbid,mte,me))
-		arg_entries
-		(interp_modexpr (Global.env()) mexpr))
+ 
+  (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in  *)
+  let mexpr_entry_o, inl_expr = match mexpr_o with
+    | None -> None, true
+    | Some (mexpr, inl) -> Some (funct interp_modexpr mexpr), inl
   in
-  let entry = 
-    {mod_entry_type = mty_entry_o;	    
+  let entry =
+    {mod_entry_type = mty_entry_o;
      mod_entry_expr = mexpr_entry_o }
   in
-  let env = Global.env() in
-  let substobjs =
+
+  let(mbids,mp_from,objs) =
     match entry with
-      | {mod_entry_type = Some mte} -> get_modtype_substobjs env mte
-      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr
+      | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp inl_res mte
+      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr
       | _ -> anomaly "declare_module: No type, no body ..."
   in
-  let substobjs = update_include substobjs in
-    (* Undo the simulated interactive building of the module *)
-    (* and declare the module as a whole *)
-    Summary.unfreeze_summaries fs;
-    match entry with 
-      |{mod_entry_type = None;	    
-	mod_entry_expr = Some (MSEident mp) } ->
-	 let dir,mp' = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
-	 let (sub,mbids,msid,objs) = substobjs in
-	 let mp1 = Environ.scrape_alias mp env in
-	 let prefix =  dir,(mp1,empty_dirpath) in
-	 let substituted = 
-	   match mbids with
-		    | [] -> 
-			Some (subst_objects prefix 
-				(join sub (join (map_msid msid mp1) (map_mp mp' mp1))) objs)
-		    | _ -> None in
-	   ignore (add_leaf
-		     id
-		     (in_module_alias (Some ({mod_entry_type = None;	    
-					      mod_entry_expr = Some (MSEident mp1) }, mty_sub_o), 
-				       substobjs, substituted)));
-	   mmp
-      | _ ->
-	  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
-	  let (sub,mbids,msid,objs) = substobjs in
-	  let sub' = join_alias (subst_key (map_msid msid mp) sub) (map_msid msid mp) in
-	  let substobjs = (join sub sub',mbids,msid,objs) in
-	  let substituted = subst_substobjs dir mp substobjs in
-	    ignore (add_leaf
-		      id
-		      (in_module (Some (entry, mty_sub_o), substobjs, substituted)));
-	    mmp
-	      
-  with e -> 
+  (* Undo the simulated interactive building of the module *)
+  (* and declare the module as a whole *)
+  Summary.unfreeze_summaries fs;
+  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
+  let mp_env,resolver = Global.add_module id entry (inl_expr&&inl_res) in
+
+  if mp_env <> mp then anomaly "Kernel and Library names do not match";
+
+  
+  check_subtypes mp subs;
+
+  let substobjs = (mbids,mp_env,
+		   subst_objects(map_mp mp_from mp_env resolver) objs) in
+  ignore (add_leaf
+	    id
+	    (in_module (Some (entry), substobjs)));
+  mmp
+
+
+let rec include_subst env mb mbids sign inline =
+  match mbids with
+    | [] -> empty_subst
+    | mbid::mbids ->
+	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
+	let subst = include_subst env mb mbids fbody_b inline in
+	let mp_delta = if not inline then mb.mod_delta else
+	  Modops.complete_inline_delta_resolver env mb.mod_mp
+	    farg_id farg_b mb.mod_delta
+	in
+	join (map_mbid mbid mb.mod_mp mp_delta) subst
+
+exception NothingToDo
+
+let get_includeself_substobjs env objs me is_mod inline =
+  try
+    let mb_mp = match me with
+      | MSEident mp ->
+	  if is_mod then
+	    Environ.lookup_module mp env
+	  else
+	    Modops.module_body_of_type mp (Environ.lookup_modtype mp env)
+      | MSEapply(fexpr, MSEident p) as mexpr ->
+	  let _,mb_mp,mp_l =
+	    if is_mod then
+	      get_objs_module_application env mexpr
+	    else
+	      let o,mtb_mp,mp_l = get_objs_modtype_application env mexpr in
+	      o,Modops.module_body_of_type mtb_mp.typ_mp mtb_mp,mp_l
+	  in
+	  List.fold_left
+	    (fun mb _ ->
+	       match mb.mod_type with
+		 |  SEBfunctor(_,_,str) -> {mb with mod_type = str}
+		 | _ -> error "Application of a functor with too much arguments.")
+	    mb_mp mp_l
+      | _ -> raise NothingToDo
+    in
+    let (mbids,mp_self,objects) = objs in
+    let mb = Global.pack_module() in
+    let subst = include_subst env mb mbids mb_mp.mod_type inline in
+    ([],mp_self,subst_objects subst objects)
+  with NothingToDo -> objs
+
+let declare_one_include_inner inl (me,is_mod) =
+  let env = Global.env() in
+  let mp1,_ = current_prefix () in
+  let (mbids,mp,objs)=
+    if is_mod then
+      get_module_substobjs env mp1 inl me
+    else
+      get_modtype_substobjs env mp1 inl me in
+  let (mbids,mp,objs) =
+    if mbids <> [] then
+      get_includeself_substobjs env (mbids,mp,objs) me is_mod inl
+    else
+      (mbids,mp,objs) in
+  let id = current_mod_id() in
+  let resolver =  Global.add_include me is_mod inl in
+  let substobjs = (mbids,mp1,
+		   subst_objects (map_mp mp mp1 resolver) objs) in
+  ignore (add_leaf id
+	    (in_include ((me,is_mod), substobjs)))
+
+let declare_one_include interp_struct me_ast =
+  declare_one_include_inner (snd me_ast)
+    (interp_struct (Global.env()) (fst me_ast))
+
+let declare_include_ interp_struct me_asts =
+  List.iter (declare_one_include interp_struct) me_asts
+
+(** Versions of earlier functions taking care of the freeze/unfreeze
+    of summaries *)
+
+let protect_summaries f =
+  let fs = Summary.freeze_summaries () in
+  try f fs
+  with e ->
     (* Something wrong: undo the whole process *)
     Summary.unfreeze_summaries fs; raise e
-      
 
-let declare_include interp_struct me_ast is_mod =
+let declare_include interp_struct me_asts =
+  protect_summaries
+    (fun _ -> declare_include_ interp_struct me_asts)
+
+let declare_modtype interp_mt interp_mix id args mtys mty_l =
+  let declare_mt fs = match mty_l with
+    | [] -> assert false
+    | [mty] -> declare_modtype_ interp_mt id args mtys mty fs
+    | mty_l ->
+	ignore (start_modtype_ interp_mt id args mtys fs);
+	declare_include_ interp_mix mty_l;
+	end_modtype ()
+  in
+  protect_summaries declare_mt
+
+let start_modtype interp_modtype id args mtys =
+  protect_summaries (start_modtype_ interp_modtype id args mtys)
+
+let declare_module interp_mt interp_me interp_mix id args mtys me_l =
+  let declare_me fs = match me_l with
+    | [] -> declare_module_ interp_mt interp_me id args mtys None fs
+    | [me] -> declare_module_ interp_mt interp_me id args mtys (Some me) fs
+    | me_l ->
+	ignore (start_module_ interp_mt None id args mtys fs);
+	declare_include_ interp_mix me_l;
+	end_module ()
+  in
+  protect_summaries declare_me
+
+let start_module interp_modtype export id args res =
+ protect_summaries (start_module_ interp_modtype export id args res)
 
-  let fs = Summary.freeze_summaries () in
 
-    try 
-      let env = Global.env() in
-      let me = interp_struct env me_ast in 
-      let substobjs = 	
-	if is_mod then
-	  get_module_substobjs env me
-	else
-	  get_modtype_substobjs env me in
-      let mp1,_ = current_prefix () in
-      let dir = dir_of_sp (Lib.path_of_include()) in
-      let substituted = subst_substobjs dir mp1 substobjs in
-      let id = current_mod_id() in
-	
-	ignore (add_leaf id
-		  (in_include ((me,is_mod), substobjs, substituted)))
-    with e -> 
-      (* Something wrong: undo the whole process *)
-      Summary.unfreeze_summaries fs; raise e
-	
-	
 (*s Iterators. *)
-	
+
 let iter_all_segments f =
-  let _ = 
-    MPmap.iter 
-      (fun _ (prefix,objects) -> 
-	 let apply_obj (id,obj) = f (make_oname prefix id) obj in
+  let _ =
+    MPmap.iter
+      (fun _ (prefix,objects) ->
+	 let rec apply_obj (id,obj) = match object_tag obj with 
+	   | "INCLUDE" -> 
+	       let (_,(_,_,objs)) =  out_include obj in 
+		 List.iter apply_obj objs
+		   
+	   | _ -> f (make_oname prefix id) obj in
 	   List.iter apply_obj objects)
       !modtab_objects
   in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 9c295451..e58f9674 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.mli 11065 2008-06-06 22:39:43Z msozeau $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Util
@@ -30,35 +30,41 @@ open Lib
    constructed by [interp_modtype] from functor arguments [fargs] and
    by [interp_modexpr] from [expr]. At least one of [typ], [expr] must
    be non-empty.
-   
+
    The [bool] in [typ] tells if the module must be abstracted [true]
    with respect to the module type or merely matched without any
    restriction [false].
 *)
 
-val declare_module : 
-  (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) ->
-  identifier -> 
-  (identifier located list * 'modtype) list -> ('modtype * bool) option -> 
-  'modexpr option -> module_path
- 
-val start_module : (env -> 'modtype -> module_struct_entry) -> 
-  bool option -> identifier -> (identifier located list * 'modtype) list ->
-   ('modtype * bool) option -> module_path
+val declare_module :
+  (env -> 'modast -> module_struct_entry) ->
+  (env -> 'modast -> module_struct_entry) ->
+  (env -> 'modast -> module_struct_entry * bool) ->
+  identifier ->
+  (identifier located list * ('modast * bool)) list ->
+  ('modast * bool) Topconstr.module_signature ->
+  ('modast * bool) list -> module_path
+
+val start_module : (env -> 'modast -> module_struct_entry) ->
+  bool option -> identifier -> (identifier located list * ('modast * bool)) list ->
+  ('modast * bool) Topconstr.module_signature -> module_path
 
-val end_module : identifier -> module_path
+val end_module : unit -> module_path
 
 
 
 (*s Module types *)
 
-val declare_modtype : (env -> 'modtype -> module_struct_entry) -> 
-  identifier -> (identifier located list * 'modtype) list -> 'modtype -> module_path
+val declare_modtype : (env -> 'modast -> module_struct_entry) ->
+  (env -> 'modast -> module_struct_entry * bool) ->
+  identifier -> (identifier located list * ('modast * bool)) list ->
+  ('modast * bool) list -> ('modast * bool) list -> module_path
 
-val start_modtype : (env -> 'modtype -> module_struct_entry) -> 
-  identifier -> (identifier located list * 'modtype) list -> module_path
+val start_modtype : (env -> 'modast -> module_struct_entry) ->
+  identifier -> (identifier located list * ('modast * bool)) list ->
+  ('modast * bool) list -> module_path
 
-val end_modtype : identifier -> module_path
+val end_modtype : unit -> module_path
 
 
 (*s Objects of a module. They come in two lists: the substitutive ones
@@ -73,8 +79,8 @@ type library_name = dir_path
 
 type library_objects
 
-val register_library : 
-  library_name -> 
+val register_library :
+  library_name ->
     Safe_typing.compiled_library -> library_objects -> Digest.t -> unit
 
 val start_library : library_name -> unit
@@ -82,6 +88,8 @@ val start_library : library_name -> unit
 val end_library :
   library_name -> Safe_typing.compiled_library * library_objects
 
+(* set a function to be executed at end_library *)
+val set_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
@@ -97,8 +105,8 @@ val import_module : bool -> module_path -> unit
 
 (* Include  *)
 
-val declare_include : (env -> 'struct_expr -> module_struct_entry) -> 
-  'struct_expr -> bool -> unit
+val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) ->
+  ('struct_expr * bool) list -> unit
 
 (*s [iter_all_segments] iterate over all segments, the modules'
     segments first and then the current segment. Modules are presented
@@ -114,5 +122,5 @@ val debug_print_modtab : unit -> Pp.std_ppcmds
 
 (* For translator *)
 val process_module_bindings : module_ident list ->
-  (mod_bound_id * module_struct_entry) list -> unit
+  (mod_bound_id * (module_struct_entry * bool)) list -> unit
 
diff --git a/library/decls.ml b/library/decls.ml
index 12808310..ac2203cc 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decls.ml 10841 2008-04-24 07:19:57Z herbelin $ *)
+(* $Id$ *)
 
 (** This module registers tables for some non-logical informations
      associated declarations *)
@@ -27,9 +27,7 @@ let vartab = ref (Idmap.empty : variable_data Idmap.t)
 let _ = Summary.declare_summary "VARIABLE"
   { Summary.freeze_function = (fun () -> !vartab);
     Summary.unfreeze_function = (fun ft -> vartab := ft);
-    Summary.init_function = (fun () -> vartab := Idmap.empty);
-    Summary.survive_module = false;
-    Summary.survive_section = false }
+    Summary.init_function = (fun () -> vartab := Idmap.empty) }
 
 let add_variable_data id o = vartab := Idmap.add id o !vartab
 
@@ -38,6 +36,10 @@ let variable_opacity id = let (_,opaq,_,_) = Idmap.find id !vartab in opaq
 let variable_kind id = let (_,_,_,k) = Idmap.find id !vartab in k
 let variable_constraints id = let (_,_,cst,_) = Idmap.find id !vartab in cst
 
+let variable_secpath id =
+  let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in
+  make_qualid dir id
+
 let variable_exists id = Idmap.mem id !vartab
 
 (** Datas associated to global parameters and constants *)
@@ -47,9 +49,7 @@ let csttab = ref (Cmap.empty : logical_kind Cmap.t)
 let _ = Summary.declare_summary "CONSTANT"
 	  { Summary.freeze_function = (fun () -> !csttab);
 	    Summary.unfreeze_function = (fun ft -> csttab := ft);
-	    Summary.init_function = (fun () -> csttab := Cmap.empty);
-	    Summary.survive_module = false;
-	    Summary.survive_section = false }
+	    Summary.init_function = (fun () -> csttab := Cmap.empty) }
 
 let add_constant_kind kn k = csttab := Cmap.add kn k !csttab
 
@@ -59,7 +59,7 @@ let constant_kind kn = Cmap.find kn !csttab
 
 let clear_proofs sign =
   List.fold_right
-    (fun (id,c,t as d) signv -> 
+    (fun (id,c,t as d) signv ->
       let d = if variable_opacity id then (id,None,t) else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
@@ -70,7 +70,3 @@ let last_section_hyps dir =
       with Not_found -> sec_ids)
     (Environ.named_context (Global.env()))
     ~init:[]
-
-let is_section_variable = function
-  | VarRef _ -> true
-  | _ -> false
diff --git a/library/decls.mli b/library/decls.mli
index 39d258b3..29fa13ae 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -6,19 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: decls.mli 10841 2008-04-24 07:19:57Z herbelin $ i*)
+(*i $Id$ i*)
 
 open Names
 open Sign
-(*
 open Libnames
-open Term
-open Declarations
-open Entries
-open Indtypes
-open Safe_typing
-open Nametab
-*)
 open Decl_kinds
 
 (** This module manages non-kernel informations about declarations. It
@@ -27,10 +19,12 @@ open Decl_kinds
 
 (** Registration and access to the table of variable *)
 
-type variable_data = 
+type variable_data =
     dir_path * bool (* opacity *) * Univ.constraints * logical_kind
 
 val add_variable_data : variable -> variable_data -> unit
+val variable_path : variable -> dir_path
+val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
 val variable_opacity : variable -> bool
 val variable_constraints : variable -> Univ.constraints
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index c7ccb3ae..85de6ab8 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dischargedhypsmap.ml 9902 2007-06-21 17:01:21Z herbelin $ *)
+(* $Id$ *)
 
 open Util
 open Libnames
@@ -20,11 +20,11 @@ open Libobject
 open Lib
 open Nametab
 
-type discharged_hyps = section_path list
+type discharged_hyps = full_path list
 
 let discharged_hyps_map = ref Spmap.empty
 
-let set_discharged_hyps sp hyps = 
+let set_discharged_hyps sp hyps =
   discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
 
 let get_discharged_hyps sp =
@@ -42,10 +42,8 @@ let freeze () = !discharged_hyps_map
 
 let unfreeze dhm = discharged_hyps_map := dhm
 
-let _ = 
+let _ =
   Summary.declare_summary "discharged_hypothesis"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_module = false;
-      Summary.survive_section = true }
+      Summary.init_function = init }
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
index 9a3259ce..f9d0f9b4 100644
--- a/library/dischargedhypsmap.mli
+++ b/library/dischargedhypsmap.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: dischargedhypsmap.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Libnames
@@ -15,10 +15,10 @@ open Environ
 open Nametab
 (*i*)
 
-type discharged_hyps = section_path list
+type discharged_hyps = full_path list
 
 (*s Discharged hypothesis. Here we store the discharged hypothesis of each *)
 (*  constant or inductive type declaration.                                *)
 
-val set_discharged_hyps : section_path -> discharged_hyps -> unit
-val get_discharged_hyps : section_path -> discharged_hyps
+val set_discharged_hyps : full_path -> discharged_hyps -> unit
+val get_discharged_hyps : full_path -> discharged_hyps
diff --git a/library/global.ml b/library/global.ml
index b2f9e127..d5fafbb8 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: global.ml 10664 2008-03-14 11:27:37Z soubiran $ *)
+(* $Id$ *)
 
 open Util
 open Names
@@ -27,13 +27,11 @@ let env () = env_of_safe_env !global_env
 
 let env_is_empty () = is_empty !global_env
 
-let _ = 
+let _ =
   declare_summary "Global environment"
     { freeze_function = (fun () -> !global_env);
       unfreeze_function = (fun fr -> global_env := fr);
-      init_function = (fun () -> global_env := empty_environment);
-      survive_module = true;
-      survive_section = false }
+      init_function = (fun () -> global_env := empty_environment) }
 
 (* Then we export the functions of [Typing] on that environment. *)
 
@@ -50,31 +48,32 @@ let push_named_def d =
   global_env := env;
   cst
 
-(*let add_thing add kn thing =
-  let _,dir,l = repr_kn kn in
-  let kn',newenv = add dir l thing !global_env in
-    if kn = kn' then
-      global_env := newenv
-    else
-      anomaly "Kernel names do not match."
-*)
 
-let add_thing add dir id thing = 
+let add_thing add dir id thing =
   let kn, newenv = add dir (label_of_id id) thing !global_env in
     global_env := newenv;
     kn
 
-let add_constant = add_thing add_constant 
+let add_constant = add_thing add_constant
 let add_mind = add_thing add_mind
-let add_modtype = add_thing (fun _ -> add_modtype) ()
-let add_module = add_thing (fun _ -> add_module) ()
-let add_alias = add_thing (fun _ -> add_alias) ()
+let add_modtype x y inl = add_thing (fun _ x y -> add_modtype x y inl) () x y
+
+
+let add_module id me inl =
+  let l = label_of_id id in
+  let mp,resolve,new_env = add_module l me inl !global_env in
+    global_env := new_env;
+    mp,resolve
+    
 
 let add_constraints c = global_env := add_constraints c !global_env
 
 let set_engagement c = global_env := set_engagement c !global_env
 
-let add_include me = global_env := add_include me !global_env
+let add_include me is_module inl =
+  let resolve,newenv = add_include me is_module inl !global_env in
+    global_env := newenv;
+    resolve
 
 let start_module id =
   let l = label_of_id id in
@@ -82,16 +81,18 @@ let start_module id =
     global_env := newenv;
     mp
 
-let end_module id mtyo =
+let end_module fs id mtyo =
   let l = label_of_id id in
-  let mp,newenv = end_module l mtyo !global_env in
+  let mp,resolve,newenv = end_module l mtyo !global_env in
+    Summary.unfreeze_summaries fs;
     global_env := newenv;
-    mp
+    mp,resolve
 
 
-let add_module_parameter mbid mte =
-  let newenv = add_module_parameter mbid mte !global_env in
-    global_env := newenv
+let add_module_parameter mbid mte inl =
+  let resolve,newenv = add_module_parameter mbid mte inl !global_env in
+    global_env := newenv;
+    resolve
 
 
 let start_modtype id =
@@ -100,12 +101,15 @@ let start_modtype id =
     global_env := newenv;
     mp
 
-let end_modtype id =
+let end_modtype fs id =
   let l = label_of_id id in
   let kn,newenv = end_modtype l !global_env in
+    Summary.unfreeze_summaries fs;
     global_env := newenv;
     kn
 
+let pack_module () = 
+  pack_module !global_env
 
 
 
@@ -117,19 +121,26 @@ let lookup_mind kn = lookup_mind kn (env())
 let lookup_module mp = lookup_module mp (env())
 let lookup_modtype kn = lookup_modtype kn (env())
 
-
-
-
-let start_library dir = 
+let constant_of_delta con = 
+  let resolver,resolver_param = (delta_of_senv !global_env) in
+    Mod_subst.constant_of_delta resolver_param
+      (Mod_subst.constant_of_delta resolver con)
+
+let mind_of_delta mind = 
+  let resolver,resolver_param = (delta_of_senv !global_env) in
+    Mod_subst.mind_of_delta resolver_param
+      (Mod_subst.mind_of_delta resolver mind)
+	
+let start_library dir =
   let mp,newenv = start_library dir !global_env in
-    global_env := newenv; 
+    global_env := newenv;
     mp
 
-let export s = snd (export !global_env s)
+let export s = export !global_env s
 
-let import cenv digest = 
-  let mp,newenv = import cenv digest !global_env in 
-    global_env := newenv; 
+let import cenv digest =
+  let mp,newenv = import cenv digest !global_env in
+    global_env := newenv;
     mp
 
 
@@ -137,13 +148,13 @@ let import cenv digest =
 (*s Function to get an environment from the constants part of the global
     environment and a given context. *)
 
-let env_of_context hyps = 
+let env_of_context hyps =
   reset_with_named_context hyps (env())
 
 open Libnames
 
 let type_of_reference env = function
-  | VarRef id -> Environ.named_type id env 
+  | VarRef id -> Environ.named_type id env
   | ConstRef c -> Typeops.type_of_constant env c
   | IndRef ind ->
      let specif = Inductive.lookup_mind_specif env ind in
@@ -161,3 +172,5 @@ let register field value by_clause =
   let entry = kind_of_term value in
   let senv = Safe_typing.register !global_env field entry by_clause in
   global_env := senv
+
+
diff --git a/library/global.mli b/library/global.mli
index cb717cdf..a8d76c4f 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: global.mli 10664 2008-03-14 11:27:37Z soubiran $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -15,6 +15,7 @@ open Term
 open Declarations
 open Entries
 open Indtypes
+open Mod_subst
 open Safe_typing
    (*i*)
 
@@ -44,35 +45,40 @@ val push_named_def   : (identifier * constr * types option) -> Univ.constraints
 (*s Adding constants, inductives, modules and module types.  All these
   functions verify that given names match those generated by kernel *)
 
-val add_constant : 
+val add_constant :
   dir_path -> identifier -> global_declaration -> constant
-val add_mind        : 
-  dir_path -> identifier -> mutual_inductive_entry -> kernel_name
+val add_mind        :
+  dir_path -> identifier -> mutual_inductive_entry -> mutual_inductive
 
-val add_module      : identifier -> module_entry -> module_path
-val add_modtype     : identifier -> module_struct_entry -> module_path
-val add_include : module_struct_entry -> unit
-val add_alias : identifier -> module_path -> module_path
+val add_module      :
+ identifier -> module_entry -> bool -> module_path * delta_resolver
+val add_modtype     :
+ identifier -> module_struct_entry -> bool -> module_path
+val add_include :
+ module_struct_entry -> bool -> bool -> delta_resolver
 
 val add_constraints : constraints -> unit
 
 val set_engagement : engagement -> unit
 
 (*s Interactive modules and module types *)
-(* Both [start_*] functions take the [dir_path] argument to create a 
+(* Both [start_*] functions take the [dir_path] argument to create a
    [mod_self_id]. This should be the name of the compilation unit. *)
 
 (* [start_*] functions return the [module_path] valid for components
    of the started module / module type *)
 
 val start_module : identifier -> module_path
-val end_module : identifier -> module_struct_entry option -> module_path
 
-val add_module_parameter : mod_bound_id -> module_struct_entry -> unit
+val end_module : Summary.frozen ->identifier ->
+  (module_struct_entry * bool) option -> module_path * delta_resolver
 
-val start_modtype : identifier -> module_path
-val end_modtype : identifier -> module_path
+val add_module_parameter :
+ mod_bound_id -> module_struct_entry -> bool -> delta_resolver
 
+val start_modtype : identifier -> module_path
+val end_modtype : Summary.frozen -> identifier -> module_path
+val pack_module : unit -> module_body
 
 
 (* Queries *)
@@ -82,15 +88,17 @@ val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body
 val lookup_mind      : mutual_inductive -> mutual_inductive_body
 val lookup_module    : module_path -> module_body
 val lookup_modtype   : module_path -> module_type_body
+val constant_of_delta : constant -> constant
+val mind_of_delta : mutual_inductive -> mutual_inductive
 
 (* Compiled modules *)
 val start_library : dir_path -> module_path
-val export : dir_path -> compiled_library
+val export : dir_path -> module_path * compiled_library
 val import : compiled_library -> Digest.t -> module_path
 
 (*s Function to get an environment from the constants part of the global
  * environment and a given context. *)
-  
+
 val type_of_global : Libnames.global_reference -> types
 val env_of_context : Environ.named_context_val -> Environ.env
 
diff --git a/library/goptions.ml b/library/goptions.ml
index 8625ee52..e6933287 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: goptions.ml 13196 2010-06-25 18:01:50Z herbelin $ *)
+(* $Id$ *)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -22,15 +22,9 @@ open Mod_subst
 (****************************************************************************)
 (* 0- Common things                                                         *)
 
-type option_name =
-  | PrimaryTable of string
-  | SecondaryTable of string * string
-  | TertiaryTable of string * string * string
+type option_name = string list
 
-let nickname = function
-  | PrimaryTable s         -> s
-  | SecondaryTable (s1,s2) -> s1^" "^s2
-  | TertiaryTable (s1,s2,s3) -> s1^" "^s2^" "^s3
+let nickname table = String.concat " " table
 
 let error_undeclared_key key =
   error ((nickname key)^": no table or option of this type")
@@ -75,14 +69,13 @@ module MakeTable =
 
     let _ =
       if List.mem_assoc nick !A.table then
-	error "Sorry, this table name is already used"
+	error "Sorry, this table name is already used."
 
-    module MyType = struct type t = A.t let compare = Pervasives.compare end
-    module MySet = Set.Make(MyType)
+    module MySet = Set.Make (struct type t = A.t let compare = compare end)
 
     let t = ref (MySet.empty : MySet.t)
 
-    let _ = 
+    let _ =
       if A.synchronous then
 	let freeze () = !t in
 	let unfreeze c = t := c in
@@ -90,9 +83,7 @@ module MakeTable =
 	Summary.declare_summary nick
           { Summary.freeze_function = freeze;
             Summary.unfreeze_function = unfreeze;
-            Summary.init_function = init;
-	    Summary.survive_module = false;
-	    Summary.survive_section = true }
+            Summary.init_function = init }
 
     let (add_option,remove_option) =
       if A.synchronous then
@@ -100,20 +91,18 @@ module MakeTable =
           | GOadd -> t := MySet.add p !t
           | GOrmv -> t := MySet.remove p !t in
         let load_options i o = if i=1 then cache_options o in
-	let subst_options (_,subst,(f,p as obj)) = 
+	let subst_options (subst,(f,p as obj)) = 
 	  let p' = A.subst subst p in
 	    if p' == p then obj else
 	      (f,p')
 	in
-	let export_options fp = Some fp in
         let (inGo,outGo) =
           Libobject.declare_object {(Libobject.default_object nick) with
                 Libobject.load_function = load_options;
 		Libobject.open_function = load_options;
 		Libobject.cache_function = cache_options;
 		Libobject.subst_function = subst_options;
-		Libobject.classify_function = (fun (_,x) -> Substitute x);
-		Libobject.export_function = export_options} 
+		Libobject.classify_function = (fun x -> Substitute x)}
 	in
         ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
          (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c))))
@@ -122,8 +111,8 @@ module MakeTable =
          (fun c -> t := MySet.remove c !t))
 
     let print_table table_name printer table =
-      msg (str table_name ++ 
-	   (hov 0 
+      msg (str table_name ++
+	   (hov 0
 	      (if MySet.is_empty table then str "None" ++ fnl ()
                else MySet.fold
 		 (fun a b -> printer a ++ spc () ++ b)
@@ -133,11 +122,11 @@ module MakeTable =
     object
       method add x = add_option (A.encode x)
       method remove x = remove_option (A.encode x)
-      method mem x = 
+      method mem x =
 	let y = A.encode x in
         let answer = MySet.mem y !t in
         msg (A.member_message y answer ++ fnl ())
-      method print = print_table A.title A.printer !t 
+      method print = print_table A.title A.printer !t
     end
 
     let _ = A.table := (nick,new table_of_A ())::!A.table
@@ -190,7 +179,7 @@ sig
   val synchronous : bool
 end
 
-module RefConvert = functor (A : RefConvertArg) -> 
+module RefConvert = functor (A : RefConvertArg) ->
 struct
   type t = A.t
   type key = reference
@@ -217,10 +206,10 @@ type 'a option_sig = {
   optread  : unit -> 'a;
   optwrite : 'a -> unit }
 
-type option_type = bool * (unit -> value) -> (value -> unit) 
+type option_type = bool * (unit -> value) -> (value -> unit)
 
-module Key = struct type t = option_name let compare = Pervasives.compare end
-module OptionMap = Map.Make(Key)
+module OptionMap =
+  Map.Make (struct  type t = option_name let compare = compare end)
 
 let value_tab = ref OptionMap.empty
 
@@ -228,47 +217,65 @@ let value_tab = ref OptionMap.empty
 
 let get_option key = OptionMap.find key !value_tab
 
-let check_key key = try 
+let check_key key = try
   let _ = get_option key in
-  error "Sorry, this option name is already used"
+  error "Sorry, this option name is already used."
 with Not_found ->
   if List.mem_assoc (nickname key) !string_table
     or List.mem_assoc (nickname key) !ref_table
-  then error "Sorry, this option name is already used"
+  then error "Sorry, this option name is already used."
 
 open Summary
 open Libobject
 open Lib
 
-let declare_option cast uncast 
+let declare_option cast uncast
   { optsync=sync; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
   let default = read() in
-  let write = if sync then 
-    let (decl_obj,_) = 
-      declare_object {(default_object (nickname key)) with
+  (* 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 _ = declare_summary (nickname key) 
-	      {freeze_function = read;
+    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 -> Keep v);
+		       discharge_function = (fun (_,v) -> Some v);
+		       load_function = (fun _ (_,v) -> write v)}
+    in
+    let _ = declare_summary (nickname key)
+	     { freeze_function = read;
 	       unfreeze_function = write;
-	       init_function = (fun () -> write default);
-	       survive_module = false;
-	       survive_section = false}
-    in 
-    fun v -> add_anonymous_leaf (decl_obj v)
-  else write
-  in 
+	       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 cread () = cast (read ()) in
-  let cwrite v = write (uncast v) in 
-  value_tab := OptionMap.add key (name,(sync,cread,cwrite)) !value_tab; 
+  let cwrite v = write (uncast v) in
+  let clwrite v = lwrite (uncast v) in
+  let cgwrite v = gwrite (uncast v) in
+  value_tab := OptionMap.add key (name,(sync,cread,cwrite,clwrite,cgwrite)) !value_tab;
   write
 
 type 'a write_function = 'a -> unit
 
 let declare_int_option =
-  declare_option 
+  declare_option
     (fun v -> IntValue v)
     (function IntValue v -> v | _ -> anomaly "async_option")
 let declare_bool_option =
@@ -284,29 +291,38 @@ let declare_string_option =
 
 (* Setting values of options *)
 
-let set_option_value check_and_cast key v =
-  let (name,(_,read,write)) =
+let set_option_value locality check_and_cast key v =
+  let (name,(_,read,write,lwrite,gwrite)) =
     try get_option key
     with Not_found -> error ("There is no option "^(nickname key)^".")
   in
+  let write = match locality with
+    | None -> write
+    | Some true -> lwrite
+    | Some false -> gwrite
+  in
   write (check_and_cast v (read ()))
 
-let bad_type_error () = error "Bad type of value for this option"
+let bad_type_error () = error "Bad type of value for this option."
 
-let set_int_option_value = set_option_value
-  (fun v -> function 
+let set_int_option_value_gen locality = set_option_value  locality
+  (fun v -> function
      | (IntValue _) -> IntValue v
      | _ -> bad_type_error ())
-let set_bool_option_value key v =
-  try set_option_value (fun v -> function
+let set_bool_option_value_gen locality key v =
+  try set_option_value locality (fun v -> function
      | (BoolValue _) -> BoolValue v
      | _ -> bad_type_error ()) key v
   with UserError (_,s) -> Flags.if_verbose msg_warning s
-let set_string_option_value = set_option_value
- (fun v -> function 
+let set_string_option_value_gen locality = set_option_value locality
+ (fun v -> function
     | (StringValue _) -> StringValue v
     | _ -> bad_type_error ())
 
+let set_int_option_value = set_int_option_value_gen None
+let set_bool_option_value = set_bool_option_value_gen None
+let set_string_option_value = set_string_option_value_gen None
+
 (* Printing options/tables *)
 
 let msg_option_value (name,v) =
@@ -319,11 +335,11 @@ let msg_option_value (name,v) =
     | IdentValue r    -> pr_global_env Idset.empty r
 
 let print_option_value key =
-  let (name,(_,read,_)) = get_option key in
-  let s = read () in 
+  let (name,(_,read,_,_,_)) = get_option key in
+  let s = read () in
   match s with
-    | BoolValue b -> 
-	msg (str ("The "^name^" mode is "^(if b then "on" else "off")) ++ 
+    | BoolValue b ->
+	msg (str ("The "^name^" mode is "^(if b then "on" else "off")) ++
 	     fnl ())
     | _ ->
 	msg (str ("Current value of "^name^" is ") ++
@@ -333,20 +349,20 @@ let print_option_value key =
 let print_tables () =
   msg
     (str "Synchronous options:" ++ fnl () ++
-     OptionMap.fold 
-       (fun key (name,(sync,read,write)) p -> 
-	  if sync then 
+     OptionMap.fold
+       (fun key (name,(sync,read,_,_,_)) p ->
+	  if sync then
 	    p ++ str ("  "^(nickname key)^": ") ++
 	    msg_option_value (name,read()) ++ fnl ()
-	  else 
+	  else
 	    p)
        !value_tab (mt ()) ++
      str "Asynchronous options:" ++ fnl () ++
-     OptionMap.fold 
-       (fun key (name,(sync,read,write)) p -> 
-	  if sync then 
+     OptionMap.fold
+       (fun key (name,(sync,read,_,_,_)) p ->
+	  if sync then
 	    p
-	  else 
+	  else
 	    p ++ str ("  "^(nickname key)^": ") ++
             msg_option_value (name,read()) ++ fnl ())
        !value_tab (mt ()) ++
diff --git a/library/goptions.mli b/library/goptions.mli
index e076a396..511986a5 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: goptions.mli 9810 2007-04-29 09:44:58Z herbelin $ i*)
+(*i $Id$ i*)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -15,11 +15,12 @@
    - Variables storing options value are created by applying one of the
    [declare_int_option], [declare_bool_option], ... functions.
 
-   Each table/option is uniquely identified by a key of type [option_name].
-   There are two kinds of table/option idenfiers: the primary ones
-   (supposed to be more global) and the secondary ones
+   Each table/option is uniquely identified by a key of type [option_name]
+   which consists in a list of strings. Note that for parsing constraints,
+   table names must not be made of more than 2 strings while option names
+   can be of arbitrary length.
 
-   The declaration of a table, say of name [SecondaryTable("Toto","Titi")] 
+   The declaration of a table, say of name [["Toto";"Titi"]]
    automatically makes available the following vernacular commands:
 
       Add Toto Titi foo.
@@ -28,26 +29,18 @@
       Test Toto Titi.
 
    The declaration of a non boolean option value, say of name
-   [SecondaryTable("Tata","Tutu")], automatically makes available the
+   [["Tata";"Tutu";"Titi"]], automatically makes available the
    following vernacular commands:
 
-       Set Tata Tutu val.
-       Print Table Tata Tutu.
+       Set Tata Tutu Titi val.
+       Print Table Tata Tutu Titi.
 
    If it is the declaration of a boolean value, the following
    vernacular commands are made available:
 
-       Set Tata Tutu.
-       Unset Tata Tutu.
-       Print Table Tata Tutu. (* synonym: Test Table Tata Tutu. *)
-
-   For a primary table, say of name [PrimaryTable("Bidule")], the
-   vernacular commands look like
-
-      Add Bidule foo.
-      Print Table Bidule foo.
-      Set Bidule foo.
-      ...
+       Set Tata Tutu Titi.
+       Unset Tata Tutu Titi.
+       Print Table Tata Tutu Titi. (* synonym: Test Table Tata Tutu Titi. *)
 
    The created table/option may be declared synchronous or not
    (synchronous = consistent with the resetting commands)                   *)
@@ -64,11 +57,8 @@ open Mod_subst
 
 (*s Things common to tables and options. *)
 
-(* The type of primary or secondary table/option keys *)
-type option_name =
-  | PrimaryTable of string
-  | SecondaryTable of string * string
-  | TertiaryTable of string * string * string
+(* The type of table/option keys *)
+type option_name = string list
 
 val error_undeclared_key : option_name -> 'a
 
@@ -126,18 +116,18 @@ module MakeRefTable :
 (*s Options. *)
 
 (* These types and function are for declaring a new option of name [key]
-   and access functions [read] and [write]; the parameter [name] is the option name 
+   and access functions [read] and [write]; the parameter [name] is the option name
    used when printing the option value (command "Print Toto Titi." *)
 
 type 'a option_sig = {
-  optsync    : bool; 
+  optsync    : bool;
   optname    : string;
   optkey     : option_name;
   optread    : unit -> 'a;
   optwrite   : 'a -> unit
 }
 
-(* When an option is declared synchronous ([optsync] is [true]), the output is 
+(* When an option is declared synchronous ([optsync] is [true]), the output is
    a synchronous write function. Otherwise it is [optwrite] *)
 
 type 'a write_function = 'a -> unit
@@ -163,6 +153,11 @@ val get_ref_table :
       mem : reference -> unit;
       print : unit >
 
+(* The first argument is a locality flag. [Some true] = "Local", [Some false]="Global". *)
+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_int_option_value    : option_name -> int option -> unit
 val set_bool_option_value   : option_name -> bool   -> unit
 val set_string_option_value : option_name -> string -> unit
diff --git a/library/heads.ml b/library/heads.ml
index 970ae87b..056f78a5 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: heads.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id$ *)
 
 open Pp
 open Util
@@ -22,8 +22,8 @@ open Lib
 (** Characterization of the head of a term *)
 
 (* We only compute an approximation to ensure the computation is not
-   arbitrary long (e.g. the head constant of [h] defined to be 
-   [g (fun x -> phi(x))] where [g] is [fun f => g O] does not launch 
+   arbitrary long (e.g. the head constant of [h] defined to be
+   [g (fun x -> phi(x))] where [g] is [fun f => g O] does not launch
    the evaluation of [phi(0)] and the head of [h] is declared unknown). *)
 
 type rigid_head_kind =
@@ -41,10 +41,18 @@ type head_approximation =
 
 module Evalreford = struct
   type t = evaluable_global_reference
-  let compare = Pervasives.compare
+  let compare x y = 
+     let make_name = function
+      | EvalConstRef con -> 
+	  EvalConstRef(constant_of_kn(canonical_con con))
+      | k -> k
+     in 
+       Pervasives.compare (make_name x) (make_name y)
 end
 
-module Evalrefmap = Map.Make(Evalreford)
+module Evalrefmap =
+  Map.Make (Evalreford)
+
 
 let head_map = ref Evalrefmap.empty
 
@@ -54,13 +62,11 @@ let freeze () = !head_map
 
 let unfreeze hm = head_map := hm
 
-let _ = 
+let _ =
   Summary.declare_summary "Head_decl"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_module = true;
-      Summary.survive_section = false }
+      Summary.init_function = init }
 
 let variable_head id  = Evalrefmap.find (EvalVarRef id) !head_map
 let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map
@@ -69,7 +75,7 @@ let kind_of_head env t =
   let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta t) with
   | Rel n when n > k -> NotImmediatelyComputableHead
   | Rel n -> FlexibleHead (k,k+1-n,List.length l,b)
-  | Var id -> 
+  | Var id ->
       (try on_subterm k l b (variable_head id)
        with Not_found ->
         (* a goal variable *)
@@ -77,7 +83,7 @@ let kind_of_head env t =
         | Some c -> aux k l c b
         | None -> NotImmediatelyComputableHead)
   | Const cst -> on_subterm k l b (constant_head cst)
-  | Construct _ | CoFix _ -> 
+  | Construct _ | CoFix _ ->
       if b then NotImmediatelyComputableHead else ConstructorHead
   | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
   | Cast (c,_,_) -> aux k l c b
@@ -94,7 +100,7 @@ let kind_of_head env t =
   and on_subterm k l with_case = function
   | FlexibleHead (n,i,q,with_subcase) ->
       let m = List.length l in
-      let k',rest,a = 
+      let k',rest,a =
         if n > m then
           (* eta-expansion *)
           let a =
@@ -121,12 +127,12 @@ let compute_head = function
      | Some c -> kind_of_head (Global.env()) c)
 | EvalVarRef id ->
     (match pi2 (Global.lookup_named id) with
-     | Some c when not (Decls.variable_opacity id) -> 
+     | Some c when not (Decls.variable_opacity id) ->
            kind_of_head (Global.env()) c
-     | _ -> 
+     | _ ->
            RigidHead (RigidVar id))
 
-let is_rigid env t = 
+let is_rigid env t =
   match kind_of_head env t with
   | RigidHead _ | ConstructorHead -> true
   | _ -> false
@@ -135,7 +141,7 @@ let is_rigid env t =
 
 let load_head _ (_,(ref,(k:head_approximation))) =
   head_map := Evalrefmap.add ref k !head_map
-  
+
 let cache_head o =
   load_head 1 o
 
@@ -150,7 +156,7 @@ let subst_head_approximation subst = function
         kind_of_head (Global.env()) c
   | x -> x
 
-let subst_head (_,subst,(ref,k)) =
+let subst_head (subst,(ref,k)) =
   (subst_evaluable_reference subst ref, subst_head_approximation subst k)
 
 let discharge_head (_,(ref,k)) =
@@ -161,17 +167,14 @@ let discharge_head (_,(ref,k)) =
 let rebuild_head (ref,k) =
   (ref, compute_head ref)
 
-let export_head o = Some o
-
 let (inHead, _) =
-  declare_object {(default_object "HEAD") with 
+  declare_object {(default_object "HEAD") with
     cache_function = cache_head;
     load_function = load_head;
     subst_function = subst_head;
-    classify_function = (fun (_,x) -> Substitute x);
+    classify_function = (fun x -> Substitute x);
     discharge_function = discharge_head;
-    rebuild_function = rebuild_head;
-    export_function = export_head }
+    rebuild_function = rebuild_head }
 
 let declare_head c =
   let hd = compute_head c in
diff --git a/library/heads.mli b/library/heads.mli
index 52270b49..203da612 100644
--- a/library/heads.mli
+++ b/library/heads.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: heads.mli 10841 2008-04-24 07:19:57Z herbelin $ *)
+(* $Id$ *)
 
 open Names
 open Term
diff --git a/library/impargs.ml b/library/impargs.ml
index 14f88728..fead921a 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: impargs.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id$ *)
 
 open Util
 open Names
@@ -22,6 +22,7 @@ open Nametab
 open Pp
 open Topconstr
 open Termops
+open Namegen
 
 (*s Flags governing the computation of implicit arguments *)
 
@@ -34,9 +35,9 @@ type implicits_flags = {
   maximal : bool
 }
 
-(* les implicites sont stricts par défaut en v8 *)
+(* les implicites sont stricts par défaut en v8 *)
 
-let implicit_args = ref { 
+let implicit_args = ref {
   auto = false;
   strict = true;
   strongly_strict = false;
@@ -72,7 +73,7 @@ let is_maximal_implicit_args () = !implicit_args.maximal
 
 let with_implicits flags f x =
   let oflags = !implicit_args in
-  try 
+  try
     implicit_args := flags;
     let rslt = f x in
     implicit_args := oflags;
@@ -169,7 +170,7 @@ let is_flexible_reference env bound depth f =
 let push_lift d (e,n) = (push_rel d e,n+1)
 
 let is_reversible_pattern bound depth f l =
-  isRel f & let n = destRel f in (n < bound+depth) & (n >= depth) & 
+  isRel f & let n = destRel f in (n < bound+depth) & (n >= depth) &
   array_for_all (fun c -> isRel c & destRel c < depth) l &
   array_distinct l
 
@@ -194,37 +195,35 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
     | Evar _ -> ()
     | _ ->
         iter_constr_with_full_binders push_lift (frec rig) ed c
-  in 
+  in
   frec true (env,1) m; acc
 
 (* calcule la liste des arguments implicites *)
 
-let concrete_name avoid_flags l env_names n all c =
-  if n = Anonymous & noccurn 1 c then
-    (Anonymous,l)
+let find_displayed_name_in all avoid na b =
+  if all then
+    compute_and_force_displayed_name_in (RenamingElsewhereFor b) avoid na b
   else
-    let fresh_id = next_name_not_occuring avoid_flags n l env_names c in
-    let idopt = if not all && noccurn 1 c then Anonymous else Name fresh_id in
-    (idopt, fresh_id::l)
+    compute_displayed_name_in (RenamingElsewhereFor b) avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rec aux env avoid n names t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
       | Prod (na,a,b) ->
-	  let na',avoid' = concrete_name None avoid names na all b in
+	  let na',avoid' = find_displayed_name_in all avoid na 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)
-      | _ -> 
+      | _ ->
 	  let names = List.rev names in
 	  let v = Array.map (fun na -> na,None) (Array.of_list names) in
 	  if contextual then
 	    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 
+  in
+  match kind_of_term (whd_betadeltaiota env t) with
     | Prod (na,a,b) ->
-	let na',avoid = concrete_name None [] [] na all b in
+	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
 	Array.to_list v
     | _ -> []
@@ -232,16 +231,16 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
 let rec prepare_implicits f = function
   | [] -> []
   | (Anonymous, Some _)::_ -> anomaly "Unnamed implicit"
-  | (Name id, Some imp)::imps -> 
+  | (Name id, Some imp)::imps ->
       let imps' = prepare_implicits f imps in
-      Some (id,imp,set_maximality imps' f.maximal) :: imps'
+      Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
   | _::imps -> None :: prepare_implicits f imps
 
-let compute_implicits_flags env f all t = 
-  compute_implicits_gen 
+let compute_implicits_flags env f all t =
+  compute_implicits_gen
     (f.strict or f.strongly_strict) f.strongly_strict
     f.reversible_pattern f.contextual all env t
-    
+
 let set_implicit id imp insmax =
   (id,(match imp with None -> Manual | Some imp -> imp),insmax)
 
@@ -256,44 +255,44 @@ let compute_manual_implicits env flags t enriching l =
     else compute_implicits_gen false false false true true env t in
   let n = List.length autoimps in
   let try_forced k l =
-    try 
-      let (id, (b, f)), l' = assoc_by_pos k l in
-	if f then
+    try
+      let (id, (b, fi, fo)), l' = assoc_by_pos k l in
+	if fo then
 	  let id = match id with Some id -> id | None -> id_of_string ("arg_" ^ string_of_int k) in
-	    l', Some (id,Manual,b)
+	    l', Some (id,Manual,(b,fi))
 	else l, None
     with Not_found -> l, None
   in
-  if not (list_distinct l) then 
+  if not (list_distinct l) then
     error ("Some parameters are referred more than once");
   (* Compare with automatic implicits to recover printing data and names *)
   let rec merge k l = function
   | (Name id,imp)::imps ->
       let l',imp,m =
-	try 
-	  let (b, f) = List.assoc (ExplByName id) l in
-	  List.remove_assoc (ExplByName id) l, (Some Manual), (Some b)
+	try
+	  let (b, fi, fo) = List.assoc (ExplByName id) l in
+	  List.remove_assoc (ExplByName id) l, (Some Manual), (Some (b, fi))
 	with Not_found ->
-	try 
-	  let (id, (b, f)), l' = assoc_by_pos k l in
-	    l', (Some Manual), (Some b)
+	try
+	  let (id, (b, fi, fo)), l' = assoc_by_pos k l in
+	    l', (Some Manual), (Some (b,fi))
 	with Not_found ->
-	  l,imp, if enriching && imp <> None then Some flags.maximal else None
+	  l,imp, if enriching && imp <> None then Some (flags.maximal,true) else None
       in
       let imps' = merge (k+1) l' imps in
-      let m = Option.map (set_maximality imps') m in
+      let m = Option.map (fun (b,f) -> set_maximality imps' b, f) m in
       Option.map (set_implicit id imp) m :: imps'
   | (Anonymous,imp)::imps ->
       let l', forced = try_forced k l in
 	forced :: merge (k+1) l' imps
   | [] when l = [] -> []
   | [] ->
-      List.iter (function 
-	| ExplByName id,(b,forced) -> 
+      List.iter (function
+	| ExplByName id,(b,fi,forced) ->
 	    if not forced then
 	      error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
 	| ExplByPos (i,_id),_t ->
-	    if i<1 or i>n then 
+	    if i<1 or i>n then
 	      error ("Bad implicit argument number: "^(string_of_int i))
 	    else
 	      errorlabstrm ""
@@ -307,19 +306,20 @@ let const v _ = v
 
 let compute_implicits_auto env f manual t =
   match manual with
-  | [] -> 
+  | [] ->
       if not f.auto then []
       else let l = compute_implicits_flags env f false t in
 	     prepare_implicits f l
   | _ -> compute_manual_implicits env f t f.auto manual
-	
+
 let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
 
 type maximal_insertion = bool (* true = maximal contextual insertion *)
+type force_inference = bool (* true = always infer, never turn into evar/subgoal *)
 
 type implicit_status =
     (* None = Not implicit *)
-    (identifier * implicit_explanation * maximal_insertion) option
+    (identifier * implicit_explanation * (maximal_insertion * force_inference)) option
 
 type implicits_list = implicit_status list
 
@@ -332,7 +332,11 @@ let name_of_implicit = function
   | Some (id,_,_) -> id
 
 let maximal_insertion_of = function
-  | Some (_,_,b) -> b
+  | Some (_,_,(b,_)) -> b
+  | None -> anomaly "Not an implicit argument"
+
+let force_inference_of = function
+  | Some (_, _, (_, b)) -> b
   | None -> anomaly "Not an implicit argument"
 
 (* [in_ctx] means we know the expected type, [n] is the index of the argument *)
@@ -361,7 +365,7 @@ let compute_constant_implicits flags manual cst =
 
 (*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
-   $i$ are the implicit arguments of the inductive and $v$ the array of 
+   $i$ are the implicit arguments of the inductive and $v$ the array of
    implicit arguments of the constructors. *)
 
 let compute_mib_implicits flags manual kn =
@@ -386,7 +390,7 @@ let compute_mib_implicits flags manual kn =
 
 let compute_all_mib_implicits flags manual kn =
   let imps = compute_mib_implicits flags manual kn in
-  List.flatten 
+  List.flatten
     (array_map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps)
 
 (*s Variables. *)
@@ -401,25 +405,18 @@ let compute_var_implicits flags manual id =
 let compute_global_implicits flags manual = function
   | VarRef id -> compute_var_implicits flags manual id
   | ConstRef kn -> compute_constant_implicits flags manual kn
-  | IndRef (kn,i) -> 
+  | IndRef (kn,i) ->
       let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps
-  | ConstructRef ((kn,i),j) -> 
+  | ConstructRef ((kn,i),j) ->
       let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1)
 
 (* Merge a manual explicitation with an implicit_status list *)
 
-let list_split_at index l = 
-  let rec aux i acc = function
-      tl when i = index -> (List.rev acc), tl
-    | hd :: tl -> aux (succ i) (hd :: acc) tl
-    | [] -> failwith "list_split_at: Invalid argument"
-  in aux 0 [] l
-    
 let merge_impls oldimpls newimpls =
-  let (before, news), olds = 
+  let (before, news), olds =
     let len = List.length newimpls - List.length oldimpls in
       if len >= 0 then list_split_at len newimpls, oldimpls
-      else 
+      else
 	let before, after = list_split_at (-len) oldimpls in
 	  (before, newimpls), after
   in
@@ -437,8 +434,8 @@ type implicit_interactive_request =
 type implicit_discharge_request =
   | ImplLocal
   | ImplConstant of constant * implicits_flags
-  | ImplMutualInductive of kernel_name * implicits_flags
-  | ImplInteractive of global_reference * implicits_flags * 
+  | ImplMutualInductive of mutual_inductive * implicits_flags
+  | ImplInteractive of global_reference * implicits_flags *
       implicit_interactive_request
 
 let implicits_table = ref Refmap.empty
@@ -457,11 +454,11 @@ let cache_implicits o =
 let subst_implicits_decl subst (r,imps as o) =
   let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
 
-let subst_implicits (_,subst,(req,l)) =
+let subst_implicits (subst,(req,l)) =
   (ImplLocal,list_smartmap (subst_implicits_decl subst) l)
 
 let impls_of_context ctx =
-  List.rev_map (fun (id,impl,_,_) -> if impl = Lib.Implicit then Some (id, Manual, true) else None)
+  List.rev_map (fun (id,impl,_,_) -> if impl = Lib.Implicit then Some (id, Manual, (true,true)) else None)
     (List.filter (fun (_,_,b,_) -> b = None) ctx)
 
 let section_segment_of_reference = function
@@ -473,9 +470,9 @@ let section_segment_of_reference = function
 let discharge_implicits (_,(req,l)) =
   match req with
   | ImplLocal -> None
-  | ImplInteractive (ref,flags,exp) -> 
+  | ImplInteractive (ref,flags,exp) ->
       let vars = section_segment_of_reference ref in
-      let ref' = pop_global_reference ref in
+      let ref' = if isVarRef ref then ref else pop_global_reference ref in
       let l' = [ref', impls_of_context vars @ snd (List.hd l)] in
       Some (ImplInteractive (ref',flags,exp),l')
   | ImplConstant (con,flags) ->
@@ -483,58 +480,61 @@ let discharge_implicits (_,(req,l)) =
       let l' = [ConstRef con',impls_of_context (section_segment_of_constant con) @ snd (List.hd l)] in
 	Some (ImplConstant (con',flags),l')
   | ImplMutualInductive (kn,flags) ->
-      let l' = List.map (fun (gr, l) -> 
+      let l' = List.map (fun (gr, l) ->
 	let vars = section_segment_of_reference gr in
-	  (pop_global_reference gr, impls_of_context vars @ l)) l 
+	((if isVarRef gr then gr else pop_global_reference gr),
+	 impls_of_context vars @ l)) l
       in
 	Some (ImplMutualInductive (pop_kn kn,flags),l')
 
 let rebuild_implicits (req,l) =
-  let l' = match req with
+  match req with
   | ImplLocal -> assert false
-  | ImplConstant (con,flags) -> 
+  | ImplConstant (con,flags) ->
       let oldimpls = snd (List.hd l) in
       let newimpls = compute_constant_implicits flags [] con in
-      [ConstRef con, merge_impls oldimpls newimpls]
+      req, [ConstRef con, merge_impls oldimpls newimpls]
   | ImplMutualInductive (kn,flags) ->
       let newimpls = compute_all_mib_implicits flags [] kn in
-      let rec aux olds news = 
+      let rec aux olds news =
 	match olds, news with
 	| (_, oldimpls) :: old, (gr, newimpls) :: tl ->
 	    (gr, merge_impls oldimpls newimpls) :: aux old tl
 	| [], [] -> []
 	| _, _ -> assert false
-      in aux l newimpls
+      in req, aux l newimpls
 
   | ImplInteractive (ref,flags,o) ->
+      (if isVarRef ref && is_in_section ref then ImplLocal else req),
       match o with
-      | ImplAuto -> 
+      | ImplAuto ->
 	  let oldimpls = snd (List.hd l) in
 	  let newimpls = compute_global_implicits flags [] ref in
 	    [ref,merge_impls oldimpls newimpls]
-      | ImplManual m -> 
+      | ImplManual m ->
 	  let oldimpls = snd (List.hd l) in
-	  let auto = 
+	  let auto =
 	    if flags.auto then
 	      let newimpls = compute_global_implicits flags [] ref in
 		merge_impls oldimpls newimpls
 	    else oldimpls
 	  in
-	  let l' = merge_impls auto m in [ref,l']
-  in (req,l')
+	  let l' = merge_impls auto m in
+	  [ref,l']
 
-let export_implicits (req,_ as x) = 
-  if req = ImplLocal then None else Some x
+let classify_implicits (req,_ as obj) =
+  if req = ImplLocal then Dispose else Substitute obj
 
 let (inImplicits, _) =
-  declare_object {(default_object "IMPLICITS") with 
+  declare_object {(default_object "IMPLICITS") with
     cache_function = cache_implicits;
     load_function = load_implicits;
     subst_function = subst_implicits;
-    classify_function = (fun (_,x) -> Substitute x);
+    classify_function = classify_implicits;
     discharge_function = discharge_implicits;
-    rebuild_function = rebuild_implicits;
-    export_function = export_implicits }
+    rebuild_function = rebuild_implicits }
+
+let is_local local ref = local || isVarRef ref && is_in_section ref
 
 let declare_implicits_gen req flags ref =
   let imps = compute_global_implicits flags [] ref in
@@ -542,10 +542,10 @@ let declare_implicits_gen req flags ref =
 
 let declare_implicits local ref =
   let flags = { !implicit_args with auto = true } in
-  let req = 
-    if local then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in
+  let req =
+    if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in
     declare_implicits_gen req flags ref
-      
+
 let declare_var_implicits id =
   let flags = !implicit_args in
     declare_implicits_gen ImplLocal flags (VarRef id)
@@ -561,11 +561,11 @@ let declare_mib_implicits kn =
     (compute_mib_implicits flags [] kn) in
     add_anonymous_leaf
       (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
-      
+
 (* Declare manual implicits *)
-type manual_explicitation = Topconstr.explicitation * (bool * bool) 
-  
-let compute_implicits_with_manual env typ enriching l = 
+type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
+
+let compute_implicits_with_manual env typ enriching l =
   compute_manual_implicits env !implicit_args typ enriching l
 
 let declare_manual_implicits local ref ?enriching l =
@@ -575,7 +575,7 @@ let declare_manual_implicits local ref ?enriching l =
   let enriching = Option.default flags.auto enriching in
   let l' = compute_manual_implicits env flags t enriching l in
   let req =
-    if local or isVarRef ref then ImplLocal
+    if is_local local ref then ImplLocal
     else ImplInteractive(ref,flags,ImplManual l')
   in
     add_anonymous_leaf (inImplicits (req,[ref,l']))
@@ -584,9 +584,9 @@ let maybe_declare_manual_implicits local ref ?enriching l =
   if l = [] then ()
   else declare_manual_implicits local ref ?enriching l
 
-let lift_implicits n = 
-  List.map (fun x -> 
-    match fst x with 
+let lift_implicits n =
+  List.map (fun x ->
+    match fst x with
 	ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
       | _ -> x)
 
@@ -596,10 +596,8 @@ let init () = implicits_table := Refmap.empty
 let freeze () = !implicits_table
 let unfreeze t = implicits_table := t
 
-let _ = 
+let _ =
   Summary.declare_summary "implicits"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_module = false;
-      Summary.survive_section = false }
+      Summary.init_function = init }
diff --git a/library/impargs.mli b/library/impargs.mli
index c1f119e6..e8191e86 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: impargs.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -16,7 +16,7 @@ open Environ
 open Nametab
 (*i*)
 
-(*s Implicit arguments. Here we store the implicit arguments. Notice that we 
+(*s Implicit arguments. Here we store the implicit arguments. Notice that we
     are outside the kernel, which knows nothing about implicit arguments. *)
 
 val make_implicit_args : bool -> unit
@@ -50,13 +50,14 @@ type implicit_explanation =
   | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
   | Manual
 
-type implicit_status = (identifier * implicit_explanation * bool) option
+type implicit_status = (identifier * implicit_explanation * (bool * bool)) option
 type implicits_list = implicit_status list
 
 val is_status_implicit : implicit_status -> bool
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
 val name_of_implicit : implicit_status -> identifier
 val maximal_insertion_of : implicit_status -> bool
+val force_inference_of : implicit_status -> bool
 
 val positions_of_implicits : implicits_list -> int list
 
@@ -65,10 +66,11 @@ val positions_of_implicits : implicits_list -> int list
 val compute_implicits : env -> types -> implicits_list
 
 (* A [manual_explicitation] is a tuple of a positional or named explicitation with
-   maximal insertion and forcing flags. *)
-type manual_explicitation = Topconstr.explicitation * (bool * bool)
+   maximal insertion, force inference and force usage flags. Forcing usage makes
+   the argument implicit even if the automatic inference considers it not inferable. *)
+type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
 
-val compute_implicits_with_manual : env -> types -> bool -> 
+val compute_implicits_with_manual : env -> types -> bool ->
   manual_explicitation list -> implicits_list
 
 (*s Computation of implicits (done using the global environment). *)
@@ -106,18 +108,7 @@ type implicit_interactive_request =
 type implicit_discharge_request =
   | ImplLocal
   | ImplConstant of constant * implicits_flags
-  | ImplMutualInductive of kernel_name * implicits_flags
-  | ImplInteractive of global_reference * implicits_flags * 
+  | ImplMutualInductive of mutual_inductive * implicits_flags
+  | ImplInteractive of global_reference * implicits_flags *
       implicit_interactive_request
 
-val discharge_implicits :     'a *
-    (implicit_discharge_request *
-     (Libnames.global_reference *
-      (Names.identifier * implicit_explanation * bool) option list)
-     list) ->
-    (implicit_discharge_request *
-     (Libnames.global_reference *
-      (Names.identifier * implicit_explanation * bool) option list)
-     list)
-    option
-
diff --git a/library/lib.ml b/library/lib.ml
index f0ec488b..c8f5c625 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml 12496 2009-11-11 13:37:57Z herbelin $ *)
+(* $Id$ *)
 
 open Pp
 open Util
@@ -14,10 +14,7 @@ open Libnames
 open Nameops
 open Libobject
 open Summary
-
-
-
-type node = 
+type node =
   | Leaf of obj
   | CompilingLibrary of object_prefix
   | OpenedModule of bool option * object_prefix * Summary.frozen
@@ -40,31 +37,31 @@ let iter_objects f i prefix =
 let load_objects = iter_objects load_object
 let open_objects = iter_objects open_object
 
-let subst_objects prefix subst seg = 
+let subst_objects subst seg = 
   let subst_one = fun (id,obj as node) ->
-    let obj' = subst_object (make_oname prefix id, subst, obj) in
+    let obj' = subst_object (subst,obj) in
       if obj' == obj then node else
 	(id, obj')
   in
     list_smartmap subst_one seg
 
-let load_and_subst_objects i prefix subst seg =
+(*let load_and_subst_objects i prefix subst seg =
   List.rev (List.fold_left (fun seg (id,obj as node) ->
     let obj' =  subst_object (make_oname prefix id, subst, obj) in
     let node = if obj == obj' then node else (id, obj') in
     load_object i (make_oname prefix id, obj');
     node :: seg) [] seg)
-
+*)
 let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
-    | ((sp,kn as oname),Leaf o) :: stk -> 
+    | ((sp,kn),Leaf o) :: stk ->
 	let id = Names.id_of_label (Names.label kn) in
-	  (match classify_object (oname,o) with 
+	  (match classify_object o with
 	     | Dispose -> clean acc stk
-	     | Keep o' -> 
+	     | Keep o' ->
 		 clean (substl, (id,o')::keepl, anticipl) stk
-	     | Substitute o' -> 
+	     | Substitute o' ->
 		 clean ((id,o')::substl, keepl, anticipl) stk
 	     | Anticipate o' ->
 		 clean (substl, keepl, o'::anticipl) stk)
@@ -84,12 +81,12 @@ let classify_segment seg =
 let segment_of_objects prefix =
   List.map (fun (id,obj) -> (make_oname prefix id, Leaf obj))
 
-(* We keep trace of operations in the stack [lib_stk]. 
-   [path_prefix] is the current path of sections, where sections are stored in 
-   ``correct'' order, the oldest coming first in the list. It may seems 
+(* We keep trace of operations in the stack [lib_stk].
+   [path_prefix] is the current path of sections, where sections are stored in
+   ``correct'' order, the oldest coming first in the list. It may seems
    costly, but in practice there is not so many openings and closings of
    sections, but on the contrary there are many constructions of section
-   paths based on the library path. *) 
+   paths based on the library path. *)
 
 let initial_prefix = default_library,(Names.initial_path,Names.empty_dirpath)
 
@@ -114,13 +111,17 @@ let sections_are_opened () =
 
 let cwd () = fst !path_prefix
 
+let cwd_except_section () =
+  Libnames.pop_dirpath_n (sections_depth ()) (cwd ())
+
 let current_dirpath sec =
-  Libnames.drop_dirpath_prefix (library_dp ()) 
-    (if sec then cwd () 
-      else Libnames.extract_dirpath_prefix (sections_depth ()) (cwd ()))
-    
+  Libnames.drop_dirpath_prefix (library_dp ())
+    (if sec then cwd () else cwd_except_section ())
+
 let make_path id = Libnames.make_path (cwd ()) id
 
+let make_path_except_section id = Libnames.make_path (cwd_except_section ()) id
+
 let path_of_include () =
   let dir = Names.repr_dirpath (cwd ()) in
   let new_dir = List.tl dir in
@@ -129,11 +130,11 @@ let path_of_include () =
 
 let current_prefix () = snd !path_prefix
 
-let make_kn id = 
+let make_kn id =
   let mp,dir = current_prefix () in
     Names.make_kn mp dir (Names.label_of_id id)
 
-let make_con id = 
+let make_con id =
   let mp,dir = current_prefix () in
     Names.make_con mp dir (Names.label_of_id id)
 
@@ -151,25 +152,25 @@ let recalc_path_prefix () =
   in
   path_prefix := recalc !lib_stk
 
-let pop_path_prefix () = 
+let pop_path_prefix () =
   let dir,(mp,sec) = !path_prefix in
     path_prefix := fst (split_dirpath dir), (mp, fst (split_dirpath sec))
 
-let find_entry_p p = 
+let find_entry_p p =
   let rec find = function
     | [] -> raise Not_found
     | ent::l -> if p ent then ent else find l
   in
   find !lib_stk
 
-let find_split_p p = 
+let find_split_p p =
   let rec find = function
     | [] -> raise Not_found
     | ent::l -> if p ent then ent,l else find l
   in
   find !lib_stk
 
-let split_lib_gen test = 
+let split_lib_gen test =
   let rec collect after equal = function
     | hd::before when test hd -> collect after (hd::equal) before
     | before -> after,equal,before
@@ -196,18 +197,20 @@ let split_lib_gen test =
 let split_lib sp = split_lib_gen (fun x -> fst x = sp)
 
 let split_lib_at_opening sp =
-  split_lib_gen (function
+  let a,s,b = split_lib_gen (function
     | x,(OpenedSection _|OpenedModule _|OpenedModtype _|CompilingLibrary _) ->
 	x = sp
     | _ ->
-	false)
+	false) in
+  assert (List.tl s = []);
+  (a,List.hd s,b)
 
 (* Adding operations. *)
 
 let add_entry sp node =
   lib_stk := (sp,node) :: !lib_stk
 
-let anonymous_id = 
+let anonymous_id =
   let n = ref 0 in
   fun () -> incr n; Names.id_of_string ("_" ^ (string_of_int !n))
 
@@ -217,12 +220,8 @@ let add_anonymous_entry node =
   add_entry name node;
   name
 
-let add_absolutely_named_leaf sp obj =
-  cache_object (sp,obj);
-  add_entry sp (Leaf obj)
-
 let add_leaf id obj =
-  if fst (current_prefix ()) = Names.initial_path then 
+  if fst (current_prefix ()) = Names.initial_path then
     error ("No session module started (use -top dir)");
   let oname = make_oname id in
   cache_object (oname,obj);
@@ -237,9 +236,9 @@ let add_discharged_leaf id obj =
 
 let add_leaves id objs =
   let oname = make_oname id in
-  let add_obj obj = 
+  let add_obj obj =
     add_entry oname (Leaf obj);
-    load_object 1 (oname,obj) 
+    load_object 1 (oname,obj)
   in
   List.iter add_obj objs;
   oname
@@ -256,58 +255,55 @@ let add_frozen_state () =
 (* Modules. *)
 
 
-let is_something_opened = function 
-    (_,OpenedSection _) -> true 
-  | (_,OpenedModule _) -> true
-  | (_,OpenedModtype _) -> true
+let is_opened id = function
+    oname,(OpenedSection _ | OpenedModule _ | OpenedModtype _) when
+      basename (fst oname) = id -> true
+  | _ -> false
+
+let is_opening_node = function
+    _,(OpenedSection _ | OpenedModule _ | OpenedModtype _) -> true
   | _ -> false
 
 
-let current_mod_id () = 
-  try match find_entry_p is_something_opened with
-    | oname,OpenedModule (_,_,nametab) -> 
+let current_mod_id () =
+  try match find_entry_p is_opening_node with
+    | oname,OpenedModule (_,_,fs) ->
 	basename (fst oname)
-    | oname,OpenedModtype (_,nametab) -> 
+    | oname,OpenedModtype (_,fs) ->
 	basename (fst oname)
     | _ -> error "you are not in a module"
   with Not_found ->
     error "no opened modules"
 
 
-let start_module export id mp nametab = 
-  let dir = extend_dirpath (fst !path_prefix) id in
+let start_module export id mp fs =
+  let dir = add_dirpath_suffix (fst !path_prefix) id in
   let prefix = dir,(mp,Names.empty_dirpath) in
   let oname = make_path id, make_kn id in
   if Nametab.exists_module dir then
     errorlabstrm "open_module" (pr_id id ++ str " already exists") ;
-  add_entry oname (OpenedModule (export,prefix,nametab));
+  add_entry oname (OpenedModule (export,prefix,fs));
   path_prefix := prefix;
   prefix
 (*  add_frozen_state () must be called in declaremods *)
- 
-let end_module id = 
-  let oname,nametab = 
-    try match find_entry_p is_something_opened with
-      | oname,OpenedModule (_,_,nametab) -> 
-	  let id' = basename (fst oname) in
-	    if id<>id' then 
-	      errorlabstrm "end_module" (str "last opened module is " ++ pr_id id'); 
-	    oname,nametab
-      | oname,OpenedModtype _ ->
-	  let id' = basename (fst oname) in
-	    errorlabstrm "end_module" 
-	      (str "module type " ++ pr_id id' ++ str " is still opened")
-      | oname,OpenedSection _ ->
-	  let id' = basename (fst oname) in
-	    errorlabstrm  "end_module" 
-	      (str "section " ++ pr_id id' ++ str " is still opened")
+
+let error_still_opened string oname =
+  let id = basename (fst oname) in
+  errorlabstrm "" (str string ++ spc () ++ pr_id id ++ str " is still opened.")
+
+let end_module () =
+  let oname,fs =
+    try match find_entry_p is_opening_node with
+      | oname,OpenedModule (_,_,fs) -> oname,fs
+      | oname,OpenedModtype _ -> error_still_opened "Module Type" oname
+      | oname,OpenedSection _ -> error_still_opened "Section" oname
       | _ -> assert false
     with Not_found ->
-      error "no opened modules"
+      error "No opened modules."
   in
-  let (after,modopening,before) = split_lib_at_opening oname in
+  let (after,mark,before) = split_lib_at_opening oname in
   lib_stk := before;
-  add_entry (make_oname id) (ClosedModule (List.rev_append after (List.rev modopening)));
+  add_entry oname (ClosedModule (List.rev (mark::after)));
   let prefix = !path_prefix in
   (* LEM: This module business seems more complicated than sections;
           shouldn't a backtrack into a closed module also do something
@@ -315,50 +311,39 @@ let end_module id =
      TODO
    *)
   recalc_path_prefix ();
-  (* add_frozen_state must be called after processing the module, 
-     because we cannot recache interactive modules  *) 
-  (oname, prefix, nametab,after)
+  (* add_frozen_state must be called after processing the module,
+     because we cannot recache interactive modules  *)
+  (oname, prefix, fs, after)
 
-let start_modtype id mp nametab = 
-  let dir = extend_dirpath (fst !path_prefix) id in
+let start_modtype id mp fs =
+  let dir = add_dirpath_suffix (fst !path_prefix) id in
   let prefix = dir,(mp,Names.empty_dirpath) in
   let sp = make_path id in
   let name = sp, make_kn id in
   if Nametab.exists_cci sp then
     errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ;
-  add_entry name (OpenedModtype (prefix,nametab));
+  add_entry name (OpenedModtype (prefix,fs));
   path_prefix := prefix;
   prefix
 
-let end_modtype id = 
-  let sp,nametab = 
-    try match find_entry_p is_something_opened with
-      | oname,OpenedModtype (_,nametab) -> 
-	  let id' = basename (fst oname) in
-	  if id<>id' then 
-	    errorlabstrm "end_modtype" (str "last opened module type is " ++ pr_id id'); 
-	    oname,nametab
-      | oname,OpenedModule _ ->
-	  let id' = basename (fst oname) in
-	    errorlabstrm "end_modtype" 
-	      (str "module " ++ pr_id id' ++ str " is still opened")
-      | oname,OpenedSection _ ->
-	  let id' = basename (fst oname) in
-	    errorlabstrm "end_modtype" 
-	      (str "section " ++ pr_id id' ++ str " is still opened")
+let end_modtype () =
+  let oname,fs =
+    try match find_entry_p is_opening_node with
+      | oname,OpenedModtype (_,fs) -> oname,fs
+      | oname,OpenedModule _ -> error_still_opened "Module" oname
+      | oname,OpenedSection _ -> error_still_opened "Section" oname
       | _ -> assert false
     with Not_found ->
       error "no opened module types"
   in
-  let (after,modtypeopening,before) = split_lib_at_opening sp in
+  let (after,mark,before) = split_lib_at_opening oname in
   lib_stk := before;
-  add_entry (make_oname id) (ClosedModtype (List.rev_append after (List.rev modtypeopening)));
+  add_entry oname (ClosedModtype (List.rev (mark::after)));
   let dir = !path_prefix in
   recalc_path_prefix ();
   (* add_frozen_state must be called after processing the module type.
-     This is because we cannot recache interactive module types *) 
-  (sp,dir,nametab,after)
-
+     This is because we cannot recache interactive module types *)
+  (oname,dir,fs,after)
 
 
 let contents_after = function
@@ -387,61 +372,68 @@ let start_compilation s mp =
 
 let end_compilation dir =
   let _ =
-    try match find_entry_p is_something_opened with
-      | _, OpenedSection _ -> error "There are some open sections"
-      | _, OpenedModule _ -> error "There are some open modules"
-      | _, OpenedModtype _ -> error "There are some open module types"
+    try match snd (find_entry_p is_opening_node) with
+      | OpenedSection _ -> error "There are some open sections."
+      | OpenedModule _ -> error "There are some open modules."
+      | OpenedModtype _ -> error "There are some open module types."
       | _ -> assert false
     with
-	Not_found -> () 
+	Not_found -> ()
   in
   let module_p =
-    function (_,CompilingLibrary _) -> true | x -> is_something_opened x
+    function (_,CompilingLibrary _) -> true | x -> is_opening_node x
   in
-  let oname = 
+  let oname =
     try match find_entry_p module_p with
 	(oname, CompilingLibrary prefix) -> oname
       | _ -> assert false
     with
 	Not_found -> anomaly "No module declared"
   in
-  let _ =  
+  let _ =
     match !comp_name with
       | None -> anomaly "There should be a module name..."
       | Some m ->
-	  if m <> dir then anomaly 
-	    ("The current open module has name "^ (Names.string_of_dirpath m) ^ 
+	  if m <> dir then anomaly
+	    ("The current open module has name "^ (Names.string_of_dirpath m) ^
 	       " and not " ^ (Names.string_of_dirpath m));
   in
-  let (after,_,before) = split_lib_at_opening oname in
+  let (after,mark,before) = split_lib_at_opening oname in
     comp_name := None;
     !path_prefix,after
 
 (* Returns true if we are inside an opened module type *)
-let is_modtype () = 
+let is_modtype () =
   let opened_p = function
-    | _, OpenedModtype _ -> true 
+    | _, OpenedModtype _ -> true
     | _ -> false
   in
-    try 
+    try
       let _ = find_entry_p opened_p in true
     with
 	Not_found -> false
 
 (* Returns true if we are inside an opened module *)
-let is_module () = 
+let is_module () =
   let opened_p = function
-    | _, OpenedModule _ -> true 
+    | _, OpenedModule _ -> true
     | _ -> false
   in
-    try 
+    try
       let _ = find_entry_p opened_p in true
     with
 	Not_found -> false
 
 
-(* Returns the most recent OpenedThing node *)
-let what_is_opened () = find_entry_p is_something_opened
+(* Returns the opening node of a given name *)
+let find_opening_node id =
+  try
+    let oname,entry = find_entry_p is_opening_node in
+    let id' = basename (fst oname) in
+    if id <> id' then
+      error ("Last block to end has name "^(Names.string_of_id id')^".");
+    entry
+  with Not_found -> error "There is nothing to end."
 
 (* Discharge tables *)
 
@@ -449,33 +441,29 @@ let what_is_opened () = find_entry_p is_something_opened
    - the list of variables in this section
    - the list of variables on which each constant depends in this section
    - the list of variables on which each inductive depends in this section
-   - the list of substitution to do at section closing 
+   - the list of substitution to do at section closing
 *)
 type binding_kind = Explicit | Implicit
 
 type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types
 type variable_context = variable_info list
-type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
+type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap.t
 
 let sectab =
-  ref ([] : ((Names.identifier * binding_kind * (Term.types * Names.identifier list) option) list * Cooking.work_list * abstr_list) list)
+  ref ([] : ((Names.identifier * binding_kind) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
-  sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
+  sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
 
-let add_section_variable id impl keep =
+let add_section_variable id impl =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-	sectab := ((id,impl,keep)::vars,repl,abs)::sl
+	sectab := ((id,impl)::vars,repl,abs)::sl
 
 let extract_hyps (secs,ohyps) =
   let rec aux = function
-    | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: aux (idl,hyps)
-    | ((id,impl,Some (ty,keep))::idl,hyps) -> 
-	if List.exists (fun (id,_,_) -> List.mem id keep) ohyps then
-	  (id,impl,None,ty) :: aux (idl,hyps)
-	else aux (idl,hyps)
+    | ((id,impl)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: aux (idl,hyps)
     | (id::idl,hyps) -> aux (idl,hyps)
     | [], _ -> []
   in aux (secs,ohyps)
@@ -496,9 +484,9 @@ let add_section_replacement f g hyps =
     let sechyps = extract_hyps (vars,hyps) in
     let args = instance_from_variable_context (List.rev sechyps) in
     sectab := (vars,f args exps,g sechyps abs)::sl
-	
+
 let add_section_kn kn =
-  let f x (l1,l2) = (l1,Names.KNmap.add kn x l2) in
+  let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
   add_section_replacement f f
 
 let add_section_constant kn =
@@ -513,20 +501,20 @@ let section_segment_of_constant con =
   Names.Cmap.find con (fst (pi3 (List.hd !sectab)))
 
 let section_segment_of_mutual_inductive kn =
-  Names.KNmap.find kn (snd (pi3 (List.hd !sectab)))
+  Names.Mindmap.find kn (snd (pi3 (List.hd !sectab)))
 
-let rec list_mem_assoc_in_triple x = function
-    [] -> raise Not_found
-  | (a,_,_)::l -> compare a x = 0 or list_mem_assoc_in_triple x l
+let rec list_mem_assoc x = function
+  | [] -> raise Not_found
+  | (a,_)::l -> compare a x = 0 or list_mem_assoc x l
 
 let section_instance = function
   | VarRef id ->
-      if list_mem_assoc_in_triple id (pi1 (List.hd !sectab)) then [||]
+      if list_mem_assoc id (pi1 (List.hd !sectab)) then [||]
       else raise Not_found
   | ConstRef con ->
       Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      Names.KNmap.find kn (snd (pi2 (List.hd !sectab)))
+      Names.Mindmap.find kn (snd (pi2 (List.hd !sectab)))
 
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
@@ -535,13 +523,11 @@ let init_sectab () = sectab := []
 let freeze_sectab () = !sectab
 let unfreeze_sectab s = sectab := s
 
-let _ = 
+let _ =
   Summary.declare_summary "section-context"
     { Summary.freeze_function = freeze_sectab;
       Summary.unfreeze_function = unfreeze_sectab;
-      Summary.init_function = init_sectab;
-      Summary.survive_module = false;
-      Summary.survive_section = false }
+      Summary.init_function = init_sectab }
 
 (*************)
 (* Sections. *)
@@ -555,18 +541,18 @@ let set_xml_close_section f = xml_close_section := f
 
 let open_section id =
   let olddir,(mp,oldsec) = !path_prefix in
-  let dir = extend_dirpath olddir id in
-  let prefix = dir, (mp, extend_dirpath oldsec id) in
+  let dir = add_dirpath_suffix olddir id in
+  let prefix = dir, (mp, add_dirpath_suffix oldsec id) in
   let name = make_path id, make_kn id (* this makes little sense however *) in
-    if Nametab.exists_section dir then
-      errorlabstrm "open_section" (pr_id id ++ str " already exists");
-    let sum = freeze_summaries() in
-      add_entry name (OpenedSection (prefix, sum));
-      (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
-      Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
-      path_prefix := prefix;
-      if !Flags.xml_export then !xml_open_section id;
-      add_section ()
+  if Nametab.exists_section dir then
+    errorlabstrm "open_section" (pr_id id ++ str " already exists.");
+  let fs = freeze_summaries() in
+  add_entry name (OpenedSection (prefix, fs));
+  (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
+  Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
+  path_prefix := prefix;
+  if !Flags.xml_export then !xml_open_section id;
+  add_section ()
 
 
 (* Restore lib_stk and summaries as before the section opening, and
@@ -581,26 +567,22 @@ let discharge_item ((sp,_ as oname),e) =
   | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ ->
       anomaly "discharge_item"
 
-let close_section id =
-  let oname,fs = 
-    try match find_entry_p is_something_opened with
-      | oname,OpenedSection (_,fs) -> 
-	  let id' = basename (fst oname) in 
-	    if id <> id' then 
-	      errorlabstrm "close_section" (str "Last opened section is " ++ pr_id id' ++ str ".");
-	    (oname,fs)
-      | _ -> assert false 
+let close_section () =
+  let oname,fs =
+    try match find_entry_p is_opening_node with
+      | oname,OpenedSection (_,fs) -> oname,fs
+      | _ -> assert false
     with Not_found ->
       error "No opened section."
   in
-  let (secdecls,secopening,before) = split_lib_at_opening oname in
+  let (secdecls,mark,before) = split_lib_at_opening oname in
   lib_stk := before;
   let full_olddir = fst !path_prefix in
   pop_path_prefix ();
-  add_entry (make_oname id) (ClosedSection (List.rev_append secdecls (List.rev secopening)));
-  if !Flags.xml_export then !xml_close_section id;
+  add_entry oname (ClosedSection (List.rev (mark::secdecls)));
+  if !Flags.xml_export then !xml_close_section (basename (fst oname));
   let newdecls = List.map discharge_item secdecls in
-  Summary.section_unfreeze_summaries fs;
+  Summary.unfreeze_summaries fs;
   List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
   Cooking.clear_cooking_sharing ();
   Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
@@ -627,7 +609,7 @@ let has_top_frozen_state () =
   | (sp, FrozenState _)::_ -> Some sp
   | (sp, Leaf o)::t when object_tag o = "DOT" -> aux t
   | _ -> None
-  in aux !lib_stk 
+  in aux !lib_stk
 
 let set_lib_stk new_lib_stk =
   lib_stk := new_lib_stk;
@@ -652,7 +634,7 @@ let reset_to_state sp =
   let (_,eq,before) = split_lib sp in
   (* if eq a frozen state, we'll reset to it *)
   match eq with
-  | [_,FrozenState f] -> lib_stk := eq@before;  unfreeze_summaries f
+  | [_,FrozenState f] -> lib_stk := eq@before; recalc_path_prefix (); unfreeze_summaries f
   | _ -> error "Not a frozen state"
 
 
@@ -676,7 +658,7 @@ let delete_gen test =
 let delete sp = delete_gen (fun x -> fst x = sp)
 
 let reset_name (loc,id) =
-  let (sp,_) = 
+  let (sp,_) =
     try
       find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
     with Not_found ->
@@ -693,21 +675,21 @@ let remove_name (loc,id) =
   in
     delete sp
 
-let is_mod_node = function 
-  | OpenedModule _ | OpenedModtype _ | OpenedSection _ 
-  | ClosedModule _ | ClosedModtype _ | ClosedSection _  -> true 
-  | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" 
+let is_mod_node = function
+  | OpenedModule _ | OpenedModtype _ | OpenedSection _
+  | ClosedModule _ | ClosedModtype _ | ClosedSection _  -> true
+  | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
 	|| t = "MODULE ALIAS"
   | _ -> false
 
-(* Reset on a module or section name in order to bypass constants with 
-   the same name *) 
+(* Reset on a module or section name in order to bypass constants with
+   the same name *)
 
 let reset_mod (loc,id) =
-  let (_,before) = 
+  let (_,before) =
     try
-      find_split_p (fun (sp,node) -> 
-                    let (_,spi) = repr_path (fst sp) in id = spi 
+      find_split_p (fun (sp,node) ->
+                    let (_,spi) = repr_path (fst sp) in id = spi
                     && is_mod_node node)
     with Not_found ->
       user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry")
@@ -729,7 +711,7 @@ let is_label_n n x =
     | _ -> false
 
 (* Reset the label registered by [mark_end_of_command()] with number n. *)
-let reset_label n = 
+let reset_label n =
   let current = current_command_label() in
   if n < current then
     let res = reset_to_gen (is_label_n n) in
@@ -739,7 +721,7 @@ let reset_label n =
     match !lib_stk with
       | [] -> ()
       | x :: ls -> (lib_stk := ls;set_command_label (n-1))
-    
+
 let rec back_stk n stk =
   match stk with
       (sp,Leaf o)::tail when object_tag o = "DOT" ->
@@ -771,15 +753,15 @@ let init () =
 
 let initial_state = ref None
 
-let declare_initial_state () = 
+let declare_initial_state () =
   let name = add_anonymous_entry (FrozenState (freeze_summaries())) in
   initial_state := Some name
 
 let reset_initial () =
   match !initial_state with
-    | None -> 
+    | None ->
         error "Resetting to the initial state is possible only interactively"
-    | Some sp -> 
+    | Some sp ->
   	begin match split_lib sp with
 	  | (_,[_,FrozenState fs as hd],before) ->
 	      lib_stk := hd::before;
@@ -792,7 +774,7 @@ let reset_initial () =
 
 (* Misc *)
 
-let mp_of_global ref = 
+let mp_of_global ref =
   match ref with
     | VarRef id -> fst (current_prefix ())
     | ConstRef cst -> Names.con_modpath cst
@@ -802,45 +784,43 @@ let mp_of_global ref =
 let rec dp_of_mp modp =
   match modp with
     | Names.MPfile dp -> dp
-    | Names.MPbound _ | Names.MPself _ -> library_dp ()
+    | Names.MPbound _ -> library_dp ()
     | Names.MPdot (mp,_) -> dp_of_mp mp
 
-let rec split_mp mp = 
-  match mp with 
+let rec split_mp mp =
+  match mp with
     | Names.MPfile dp -> dp,  Names.empty_dirpath
-    | Names.MPdot (prfx, lbl) -> 
-	let mprec, dprec = split_mp prfx in 
+    | Names.MPdot (prfx, lbl) ->
+	let mprec, dprec = split_mp prfx in
 	  mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
-    | Names.MPself msid -> let (_, id, dp) = Names.repr_msid msid in  library_dp(), Names.make_dirpath [Names.id_of_string id]
     | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.make_dirpath [Names.id_of_string id]
 
 let split_modpath mp =
   let rec aux = function
     | Names.MPfile dp -> dp, []
-    | Names.MPbound mbid -> 
+    | Names.MPbound mbid ->
 	library_dp (), [Names.id_of_mbid mbid]
-    | Names.MPself msid -> library_dp (), [Names.id_of_msid msid]
     | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in
 			      (mp', Names.id_of_label l :: lab)
-  in 
+  in
   let (mp, l) = aux mp in
     mp, l
-			
+
 let library_part ref =
-  match ref with 
+  match ref with
     | VarRef id -> library_dp ()
     | _ -> dp_of_mp (mp_of_global ref)
 
 let remove_section_part ref =
-  let sp = Nametab.sp_of_global ref in
+  let sp = Nametab.path_of_global ref in
   let dir,_ = repr_path sp in
   match ref with
-  | VarRef id -> 
+  | VarRef id ->
       anomaly "remove_section_part not supported on local variables"
   | _ ->
       if is_dirpath_prefix_of dir (cwd ()) then
         (* Not yet (fully) discharged *)
-        extract_dirpath_prefix (sections_depth ()) (cwd ())
+        pop_dirpath_n (sections_depth ()) (cwd ())
       else
 	(* Theorem/Lemma outside its outer section of definition *)
 	dir
@@ -849,19 +829,19 @@ let remove_section_part ref =
 (* Discharging names *)
 
 let pop_kn kn =
-  let (mp,dir,l) = Names.repr_kn kn in
-  Names.make_kn mp (dirpath_prefix dir) l
+  let (mp,dir,l) = Names.repr_mind kn in
+  Names.make_mind mp (pop_dirpath dir) l
 
-let pop_con con = 
+let pop_con con =
   let (mp,dir,l) = Names.repr_con con in
-  Names.make_con mp (dirpath_prefix dir) l
+  Names.make_con mp (pop_dirpath dir) l
 
-let con_defined_in_sec kn = 
+let con_defined_in_sec kn =
   let _,dir,_ = Names.repr_con kn in
   dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
 
-let defined_in_sec kn = 
-  let _,dir,_ = Names.repr_kn kn in
+let defined_in_sec kn =
+  let _,dir,_ = Names.repr_mind kn in
   dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
 
 let discharge_global = function
@@ -873,10 +853,10 @@ let discharge_global = function
       ConstructRef ((pop_kn kn,i),j)
   | r -> r
 
-let discharge_kn kn = 
+let discharge_kn kn =
   if defined_in_sec kn then pop_kn kn else kn
 
-let discharge_con cst = 
+let discharge_con cst =
   if con_defined_in_sec cst then pop_con cst else cst
 
 let discharge_inductive (kn,i) =
diff --git a/library/lib.mli b/library/lib.mli
index dacfed59..13c9baf6 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -6,14 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: lib.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id$ i*)
 
 
 (*s This module provides a general mechanism to keep a trace of all operations
    and to backtrack (undo) those operations. It provides also the section
    mechanism (at a low level; discharge is not known at this step). *)
 
-type node = 
+type node =
   | Leaf of Libobject.obj
   | CompilingLibrary of Libnames.object_prefix
   | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen
@@ -32,15 +32,15 @@ type lib_objects = (Names.identifier * Libobject.obj) list
 
 val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit
 val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit
-val subst_objects : Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
-val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
+val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects
+(*val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*)
 
 (* [classify_segment seg] verifies that there are no OpenedThings,
    clears ClosedSections and FrozenStates and divides Leafs according
    to their answers to the [classify_object] function in three groups:
    [Substitute], [Keep], [Anticipate] respectively.  The order of each
    returned list is the same as in the input list. *)
-val classify_segment : 
+val classify_segment :
   library_segment -> lib_objects * lib_objects * Libobject.obj list
 
 (* [segment_of_objects prefix objs] forms a list of Leafs *)
@@ -52,7 +52,6 @@ val segment_of_objects :
   current list of operations (most recent ones coming first). *)
 
 val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name
-val add_absolutely_named_leaf : Libnames.object_name -> Libobject.obj -> unit
 val add_anonymous_leaf : Libobject.obj -> unit
 
 (* this operation adds all objects with the same name and calls [load_object]
@@ -70,7 +69,7 @@ val current_command_label : unit -> int
    registered after it. *)
 val reset_label : int -> unit
 
-(*s The function [contents_after] returns the current library segment, 
+(*s The function [contents_after] returns the current library segment,
   starting from a given section path. If not given, the entire segment
   is returned. *)
 
@@ -80,9 +79,11 @@ val contents_after : Libnames.object_name option -> library_segment
 
 (* User-side names *)
 val cwd : unit -> Names.dir_path
-val current_dirpath : bool -> Names.dir_path
-val make_path : Names.identifier -> Libnames.section_path
-val path_of_include : unit -> Libnames.section_path
+val cwd_except_section : unit -> Names.dir_path
+val current_dirpath : bool -> Names.dir_path (* false = except sections *)
+val make_path : Names.identifier -> Libnames.full_path
+val make_path_except_section : Names.identifier -> Libnames.full_path
+val path_of_include : unit -> Libnames.full_path
 
 (* Kernel-side names *)
 val current_prefix : unit -> Names.module_path * Names.dir_path
@@ -98,20 +99,19 @@ val is_modtype : unit -> bool
 val is_module : unit -> bool
 val current_mod_id : unit -> Names.module_ident
 
-(* Returns the most recent OpenedThing node *)
-val what_is_opened : unit -> Libnames.object_name * node
-
+(* Returns the opening node of a given name *)
+val find_opening_node : Names.identifier -> node
 
 (*s Modules and module types *)
 
-val start_module : 
+val start_module :
   bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
-val end_module : Names.module_ident 
+val end_module : unit
   -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
 
-val start_modtype : 
+val start_modtype :
   Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
-val end_modtype : Names.module_ident 
+val end_modtype : unit
   -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
 (* [Lib.add_frozen_state] must be called after each of the above functions *)
 
@@ -134,7 +134,7 @@ val remove_section_part : Libnames.global_reference -> Names.dir_path
 (*s Sections *)
 
 val open_section : Names.identifier -> unit
-val close_section : Names.identifier -> unit
+val close_section : unit -> unit
 
 (*s Backtracking (undo). *)
 
@@ -146,7 +146,7 @@ val reset_to_state : Libnames.object_name -> unit
 
 val has_top_frozen_state : unit -> Libnames.object_name option
 
-(* [back n] resets to the place corresponding to the $n$-th call of 
+(* [back n] resets to the place corresponding to the $n$-th call of
    [mark_end_of_command] (counting backwards) *)
 val back : int -> unit
 
@@ -182,17 +182,16 @@ val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_cont
 val section_instance : Libnames.global_reference -> Names.identifier array
 val is_in_section : Libnames.global_reference -> bool
 
-val add_section_variable : Names.identifier -> binding_kind -> 
-  (Term.types * Names.identifier list) option -> unit
+val add_section_variable : Names.identifier -> binding_kind -> unit
 
 val add_section_constant : Names.constant -> Sign.named_context -> unit
-val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
+val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit
 val replacement_context : unit ->
-  (Names.identifier array Names.Cmap.t * Names.identifier array Names.KNmap.t)
+  (Names.identifier array Names.Cmap.t * Names.identifier array Names.Mindmap.t)
 
 (*s Discharge: decrease the section level if in the current section *)
 
-val discharge_kn :  Names.kernel_name -> Names.kernel_name
+val discharge_kn :  Names.mutual_inductive -> Names.mutual_inductive
 val discharge_con : Names.constant -> Names.constant
 val discharge_global : Libnames.global_reference -> Libnames.global_reference
 val discharge_inductive : Names.inductive -> Names.inductive
diff --git a/library/libnames.ml b/library/libnames.ml
index 89a77128..9a7135ea 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.ml 11878 2009-02-03 12:48:18Z soubiran $ i*)
+(*i $Id$ i*)
 
 open Pp
 open Util
@@ -23,24 +23,49 @@ type global_reference =
   | ConstructRef of constructor
 
 let isVarRef = function VarRef _ -> true | _ -> false
+let isConstRef = function ConstRef _ -> true | _ -> false
+let isIndRef = function IndRef _ -> true | _ -> false
+let isConstructRef = function ConstructRef _ -> true | _ -> false
+
+let eq_gr gr1 gr2 =
+  match gr1,gr2 with 
+      ConstRef con1, ConstRef con2 ->
+	eq_constant con1 con2
+    | IndRef kn1,IndRef kn2 -> eq_ind kn1 kn2
+    | ConstructRef kn1,ConstructRef kn2 -> eq_constructor kn1 kn2
+    | _,_ -> gr1=gr2
+
+let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
+let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
+let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
+let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef"
 
 let subst_constructor subst ((kn,i),j as ref) =
-  let kn' = subst_kn subst kn in 
+  let kn' = subst_ind subst kn in
     if kn==kn' then ref, mkConstruct ref
     else ((kn',i),j), mkConstruct ((kn',i),j)
-      
+
 let subst_global subst ref = match ref with
   | VarRef var -> ref, mkVar var
   | ConstRef kn ->
      let kn',t = subst_con subst kn in
       if kn==kn' then ref, mkConst kn else ConstRef kn', t
   | IndRef (kn,i) ->
-      let kn' = subst_kn subst kn in
+      let kn' = subst_ind subst kn in
       if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
   | ConstructRef ((kn,i),j as c) ->
       let c',t = subst_constructor subst c in
 	if c'==c then ref,t else ConstructRef c', t
 
+let canonical_gr = function
+  | ConstRef con -> 
+      ConstRef(constant_of_kn(canonical_con con))
+  | IndRef (kn,i) ->
+      IndRef(mind_of_kn(canonical_mind kn),i)
+  | ConstructRef ((kn,i),j )->
+	  ConstructRef((mind_of_kn(canonical_mind kn),i),j)
+  | VarRef id ->  VarRef id
+
 let global_of_constr c = match kind_of_term c with
   | Const sp -> ConstRef sp
   | Ind ind_sp -> IndRef ind_sp
@@ -57,16 +82,32 @@ let constr_of_global = function
 let constr_of_reference = constr_of_global
 let reference_of_constr = global_of_constr
 
-module RefOrdered =
-  struct
-    type t = global_reference
-    let compare = Pervasives.compare
-  end
-
+(* outside of the kernel, names are ordered on their canonical part *)
+module RefOrdered = struct
+  type t = global_reference
+  let compare x y = 
+    let make_name = function
+      | ConstRef con -> 
+	  ConstRef(constant_of_kn(canonical_con con))
+      | IndRef (kn,i) ->
+	  IndRef(mind_of_kn(canonical_mind kn),i)
+      | ConstructRef ((kn,i),j )->
+	  ConstructRef((mind_of_kn(canonical_mind kn),i),j)
+      | VarRef id ->  VarRef id
+    in
+	Pervasives.compare (make_name x) (make_name y)
+end
+  
 module Refset = Set.Make(RefOrdered)
 module Refmap = Map.Make(RefOrdered)
+  
+(* Extended global references *)
+
+type syndef_name = kernel_name
 
-let inductives_table = ref Indmap.empty
+type extended_global_reference =
+  | TrueGlobal of global_reference
+  | SynDef of syndef_name
 
 (**********************************************)
 
@@ -75,10 +116,10 @@ let pr_dirpath sl = (str (string_of_dirpath sl))
 (*s Operations on dirpaths *)
 
 (* Pop the last n module idents *)
-let extract_dirpath_prefix n dir =
+let pop_dirpath_n n dir =
   make_dirpath (list_skipn n (repr_dirpath dir))
 
-let dirpath_prefix p = match repr_dirpath p with
+let pop_dirpath p = match repr_dirpath p with
   | [] -> anomaly "dirpath_prefix: empty dirpath"
   | _::l -> make_dirpath l
 
@@ -101,24 +142,8 @@ let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])
 let split_dirpath d =
   let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
 
-let extend_dirpath p id = make_dirpath (id :: repr_dirpath p)
+let add_dirpath_suffix p id = make_dirpath (id :: repr_dirpath p)
 
-
-(*
-let path_of_constructor env ((sp,tyi),ind) =
-   let mib = Environ.lookup_mind sp env in
-   let mip = mib.mind_packets.(tyi) in 
-   let (pa,_) = repr_path sp in 
-   Names.make_path pa (mip.mind_consnames.(ind-1))
-
-let path_of_inductive env (sp,tyi) =
-  if tyi = 0 then sp
-  else
-    let mib = Environ.lookup_mind sp env in
-    let mip = mib.mind_packets.(tyi) in 
-    let (pa,_) = repr_path sp in 
-    Names.make_path pa (mip.mind_typename) 
-*)
 (* parsing *)
 let parse_dir s =
   let len = String.length s in
@@ -127,24 +152,27 @@ let parse_dir s =
     if n >= len then dirs else
     let pos =
       try
-	String.index_from s n '.' 
+	String.index_from s n '.'
       with Not_found -> len
     in
     if pos = n then error (s ^ " is an invalid path.");
     let dir = String.sub s n (pos-n) in
-    decoupe_dirs ((id_of_string dir)::dirs) (pos+1)	  
+    decoupe_dirs ((id_of_string dir)::dirs) (pos+1)
   in
     decoupe_dirs [] 0
 
 let dirpath_of_string s =
   make_dirpath (if s = "" then [] else parse_dir s)
 
+let string_of_dirpath = Names.string_of_dirpath
+
+
 module Dirset = Set.Make(struct type t = dir_path let compare = compare end)
 module Dirmap = Map.Make(struct type t = dir_path let compare = compare end)
 
 (*s Section paths are absolute names *)
 
-type section_path = {
+type full_path = {
   dirpath : dir_path ;
   basename : identifier }
 
@@ -165,7 +193,7 @@ let sp_ord sp1 sp2 =
 
 module SpOrdered =
   struct
-    type t = section_path
+    type t = full_path
     let compare = sp_ord
   end
 
@@ -183,41 +211,33 @@ let path_of_string s =
   with
     | Invalid_argument _ -> invalid_arg "path_of_string"
 
-let pr_sp sp = str (string_of_path sp) 
+let pr_path sp = str (string_of_path sp)
 
 let restrict_path n sp =
   let dir, s = repr_path sp in
   let dir' = list_firstn n (repr_dirpath dir) in
   make_path (make_dirpath dir') s
 
-type extended_global_reference =
-  | TrueGlobal of global_reference
-  | SyntacticDef of kernel_name
-
-let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id)
+let encode_mind dir id = make_mind (MPfile dir) empty_dirpath (label_of_id id)
 
 let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
 
-let decode_kn kn = 
+let decode_mind kn =
   let rec dir_of_mp = function
     | MPfile dir -> repr_dirpath dir
     | MPbound mbid -> 
 	let _,_,dp = repr_mbid mbid in
 	let id = id_of_mbid mbid in
 	  id::(repr_dirpath dp)
-    | MPself msid -> 
-	let _,_,dp = repr_msid msid in
-	let id = id_of_msid msid in
-	  id::(repr_dirpath dp) 
     | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
   in
-  let mp,sec_dir,l = repr_kn kn in
+  let mp,sec_dir,l = repr_mind kn in
     if (repr_dirpath sec_dir) = [] then
      (make_dirpath (dir_of_mp mp)),id_of_label l
     else
       anomaly "Section part should be empty!"
 
-let decode_con kn = 
+let decode_con kn =
   let mp,sec_dir,l = repr_con kn in
     match mp,(repr_dirpath sec_dir) with
 	MPfile dir,[] -> (dir,id_of_label l)
@@ -225,31 +245,31 @@ let decode_con kn =
       | _ -> anomaly "Section part should be empty!"
 
 (*s qualified names *)
-type qualid = section_path
+type qualid = full_path
 
 let make_qualid = make_path
 let repr_qualid = repr_path
 
 let string_of_qualid = string_of_path
-let pr_qualid = pr_sp
+let pr_qualid = pr_path
 
 let qualid_of_string = path_of_string
 
-let qualid_of_sp sp = sp
-let make_short_qualid id = make_qualid empty_dirpath id
-let qualid_of_dirpath dir = 
+let qualid_of_path sp = sp
+let qualid_of_ident id = make_qualid empty_dirpath id
+let qualid_of_dirpath dir =
   let (l,a) = split_dirpath dir in
   make_qualid l a
 
-type object_name = section_path * kernel_name
+type object_name = full_path * kernel_name
 
 type object_prefix = dir_path * (module_path * dir_path)
 
-let make_oname (dirpath,(mp,dir)) id = 
+let make_oname (dirpath,(mp,dir)) id =
   make_path dirpath id, make_kn mp dir (label_of_id id)
 
 (* to this type are mapped dir_path's in the nametab *)
-type global_dir_reference = 
+type global_dir_reference =
   | DirOpenModule of object_prefix
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
@@ -265,19 +285,19 @@ type global_dir_reference =
           ModTypeRef kn'
 *)
 
-type reference = 
+type reference =
   | Qualid of qualid located
   | Ident of identifier located
 
 let qualid_of_reference = function
   | Qualid (loc,qid) -> loc, qid
-  | Ident (loc,id) -> loc, make_short_qualid id
+  | Ident (loc,id) -> loc, qualid_of_ident id
 
 let string_of_reference = function
   | Qualid (loc,qid) -> string_of_qualid qid
   | Ident (loc,id) -> string_of_id id
 
-let pr_reference = function 
+let pr_reference = function
   | Qualid (_,qid) -> pr_qualid qid
   | Ident (_,id) -> pr_id id
 
@@ -289,14 +309,19 @@ let loc_of_reference = function
 
 let pop_con con =
   let (mp,dir,l) = repr_con con in
-  Names.make_con mp (dirpath_prefix dir) l
+  Names.make_con mp (pop_dirpath dir) l
 
 let pop_kn kn =
-  let (mp,dir,l) = repr_kn kn in
-  Names.make_kn mp (dirpath_prefix dir) l
+  let (mp,dir,l) = repr_mind kn in
+  Names.make_mind mp (pop_dirpath dir) l
 
 let pop_global_reference = function
   | ConstRef con -> ConstRef (pop_con con)
   | IndRef (kn,i) -> IndRef (pop_kn kn,i)
   | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
   | VarRef id -> anomaly "VarRef not poppable"
+
+(* Deprecated synonyms *)
+
+let make_short_qualid = qualid_of_ident
+let qualid_of_sp = qualid_of_path
diff --git a/library/libnames.mli b/library/libnames.mli
index cc664a08..9ee7d0ab 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
@@ -24,6 +24,18 @@ type global_reference =
   | ConstructRef of constructor
 
 val isVarRef : global_reference -> bool
+val isConstRef : global_reference -> bool
+val isIndRef : global_reference -> bool
+val isConstructRef : global_reference -> bool
+
+val eq_gr : global_reference -> global_reference -> bool
+val canonical_gr : global_reference -> global_reference
+
+val destVarRef : global_reference -> variable
+val destConstRef : global_reference -> constant
+val destIndRef : global_reference -> inductive
+val destConstructRef : global_reference -> constructor
+
 
 val subst_constructor : substitution -> constructor -> constructor * constr
 val subst_global : substitution -> global_reference -> global_reference * constr
@@ -39,97 +51,112 @@ val global_of_constr : constr -> global_reference
 val constr_of_reference : global_reference -> constr
 val reference_of_constr : constr -> global_reference
 
-module Refset : Set.S with type elt = global_reference 
+module RefOrdered : sig
+  type t = global_reference
+  val compare : global_reference -> global_reference -> int
+end
+  
+
+module Refset : Set.S with type elt = global_reference
 module Refmap : Map.S with type key = global_reference
 
+(*s Extended global references *)
+
+type syndef_name = kernel_name
+
+type extended_global_reference =
+  | TrueGlobal of global_reference
+  | SynDef of syndef_name
+
 (*s Dirpaths *)
 val pr_dirpath : dir_path -> Pp.std_ppcmds
 
 val dirpath_of_string : string -> dir_path
+val string_of_dirpath : dir_path -> string
 
-(* Give the immediate prefix of a [dir_path] *)
-val dirpath_prefix : dir_path -> dir_path 
+(* Pop the suffix of a [dir_path] *)
+val pop_dirpath : dir_path -> dir_path
+
+(* Pop the suffix n times *)
+val pop_dirpath_n : int -> dir_path -> dir_path
 
 (* Give the immediate prefix and basename of a [dir_path] *)
 val split_dirpath : dir_path -> dir_path * identifier
 
-val extend_dirpath : dir_path -> module_ident -> dir_path
+val add_dirpath_suffix : dir_path -> module_ident -> dir_path
 val add_dirpath_prefix : module_ident -> dir_path -> dir_path
 
 val chop_dirpath : int -> dir_path -> dir_path * dir_path
+val append_dirpath : dir_path -> dir_path -> dir_path
+
 val drop_dirpath_prefix : dir_path -> dir_path -> dir_path
-val extract_dirpath_prefix : int -> dir_path -> dir_path
 val is_dirpath_prefix_of : dir_path -> dir_path -> bool
-val append_dirpath : dir_path -> dir_path -> dir_path
 
 module Dirset : Set.S with type elt = dir_path
 module Dirmap : Map.S with type key = dir_path
 
-(*s Section paths are {\em absolute} names *)
-type section_path
+(*s Full paths are {\em absolute} paths of declarations *)
+type full_path
 
-(* Constructors of [section_path] *)
-val make_path : dir_path -> identifier -> section_path
+(* Constructors of [full_path] *)
+val make_path : dir_path -> identifier -> full_path
 
-(* Destructors of [section_path] *)
-val repr_path : section_path -> dir_path * identifier
-val dirpath : section_path -> dir_path
-val basename : section_path -> identifier
+(* Destructors of [full_path] *)
+val repr_path : full_path -> dir_path * identifier
+val dirpath : full_path -> dir_path
+val basename : full_path -> identifier
 
 (* Parsing and printing of section path as ["coq_root.module.id"] *)
-val path_of_string : string -> section_path
-val string_of_path : section_path -> string
-val pr_sp : section_path -> std_ppcmds
-
-module Sppred : Predicate.S with type elt = section_path
-module Spmap  : Map.S with type key = section_path
+val path_of_string : string -> full_path
+val string_of_path : full_path -> string
+val pr_path : full_path -> std_ppcmds
 
-val restrict_path : int -> section_path -> section_path
+module Sppred : Predicate.S with type elt = full_path
+module Spmap  : Map.S with type key = full_path
 
-type extended_global_reference =
-  | TrueGlobal of global_reference
-  | SyntacticDef of kernel_name
+val restrict_path : int -> full_path -> full_path
 
 (*s Temporary function to brutally form kernel names from section paths *)
 
-val encode_kn : dir_path -> identifier -> kernel_name
-val decode_kn : kernel_name -> dir_path * identifier
+val encode_mind : dir_path -> identifier -> mutual_inductive
+val decode_mind : mutual_inductive -> dir_path * identifier
 val encode_con : dir_path -> identifier -> constant
 val decode_con : constant -> dir_path * identifier
 
 
 (*s A [qualid] is a partially qualified ident; it includes fully
     qualified names (= absolute names) and all intermediate partial
-    qualifications of absolute names, including single identifiers *)
+    qualifications of absolute names, including single identifiers.
+    The [qualid] are used to access the name table. *)
+
 type qualid
 
 val make_qualid : dir_path -> identifier -> qualid
 val repr_qualid : qualid -> dir_path * identifier
 
-val string_of_qualid : qualid -> string
 val pr_qualid : qualid -> std_ppcmds
-
+val string_of_qualid : qualid -> string
 val qualid_of_string : string -> qualid
 
-(* Turns an absolute name into a qualified name denoting the same name *)
-val qualid_of_sp : section_path -> qualid
+(* Turns an absolute name, a dirpath, or an identifier into a
+   qualified name denoting the same name *)
 
+val qualid_of_path : full_path -> qualid
 val qualid_of_dirpath : dir_path -> qualid
-
-val make_short_qualid : identifier -> qualid
+val qualid_of_ident : identifier -> qualid
 
 (* Both names are passed to objects: a "semantic" [kernel_name], which
-   can be substituted and a "syntactic" [section_path] which can be printed
+   can be substituted and a "syntactic" [full_path] which can be printed
 *)
 
-type object_name = section_path * kernel_name
+type object_name = full_path * kernel_name
 
 type object_prefix = dir_path * (module_path * dir_path)
 
 val make_oname : object_prefix -> identifier -> object_name
 
 (* to this type are mapped [dir_path]'s in the nametab *)
-type global_dir_reference = 
+type global_dir_reference =
   | DirOpenModule of object_prefix
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
@@ -137,7 +164,11 @@ type global_dir_reference =
   | DirClosedSection of dir_path
       (* this won't last long I hope! *)
 
-type reference = 
+(*s A [reference] is the user-level notion of name. It denotes either a
+    global name (referred either by a qualified name or by a single
+    name) or a variable *)
+
+type reference =
   | Qualid of qualid located
   | Ident of identifier located
 
@@ -146,8 +177,13 @@ val string_of_reference : reference -> string
 val pr_reference : reference -> std_ppcmds
 val loc_of_reference : reference -> loc
 
-(* popping one level of section in global names *)
+(*s Popping one level of section in global names *)
 
 val pop_con : constant -> constant
-val pop_kn : kernel_name -> kernel_name
+val pop_kn : mutual_inductive-> mutual_inductive
 val pop_global_reference : global_reference -> global_reference
+
+(* Deprecated synonyms *)
+
+val make_short_qualid : identifier -> qualid (* = qualid_of_ident *)
+val qualid_of_sp : full_path -> qualid (* = qualid_of_path *)
diff --git a/library/libobject.ml b/library/libobject.ml
index b455e2b3..ecdcacf1 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: libobject.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
+(* $Id$ *)
 
 open Util
 open Names
@@ -25,7 +25,7 @@ let relax_flag = ref false;;
 
 let relax b = relax_flag := b;;
 
-type 'a substitutivity = 
+type 'a substitutivity =
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
 type 'a object_declaration = {
@@ -33,11 +33,10 @@ type 'a object_declaration = {
   cache_function : object_name * 'a -> unit;
   load_function : int -> object_name * 'a -> unit;
   open_function : int -> object_name * 'a -> unit;
-  classify_function : object_name * 'a -> 'a substitutivity;
-  subst_function : object_name * substitution * 'a -> 'a;
+  classify_function : 'a -> 'a substitutivity;
+  subst_function :  substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
-  rebuild_function : 'a -> 'a;
-  export_function : 'a -> 'a option }
+  rebuild_function : 'a -> 'a }
 
 let yell s = anomaly s
 
@@ -46,12 +45,11 @@ let default_object s = {
   cache_function = (fun _ -> ());
   load_function = (fun _ _ -> ());
   open_function = (fun _ _ -> ());
-  subst_function = (fun _ -> 
+  subst_function = (fun _ ->
     yell ("The object "^s^" does not know how to substitute!"));
-  classify_function = (fun (_,obj) -> Keep obj);
+  classify_function = (fun obj -> Keep obj);
   discharge_function = (fun _ -> None);
-  rebuild_function = (fun x -> x);
-  export_function = (fun _ -> None)} 
+  rebuild_function = (fun x -> x)}
 
 
 (* The suggested object declaration is the following:
@@ -59,13 +57,13 @@ let default_object s = {
    declare_object { (default_object "MY OBJECT") with
        cache_function = fun (sp,a) -> Mytbl.add sp a}
 
-   and the listed functions are only those which definitions accually 
+   and the listed functions are only those which definitions accually
    differ from the default.
 
    This helps introducing new functions in objects.
 *)
 
-let ident_subst_function (_,_,a) = a
+let ident_subst_function (_,a) = a
 
 type obj = Dyn.t (* persistent dynamic objects *)
 
@@ -73,15 +71,14 @@ type dynamic_object_declaration = {
   dyn_cache_function : object_name * obj -> unit;
   dyn_load_function : int -> object_name * obj -> unit;
   dyn_open_function : int -> object_name * obj -> unit;
-  dyn_subst_function : object_name * substitution * obj -> obj;
-  dyn_classify_function : object_name * obj -> obj substitutivity;
+  dyn_subst_function : substitution * obj -> obj;
+  dyn_classify_function : obj -> obj substitutivity;
   dyn_discharge_function : object_name * obj -> obj option;
-  dyn_rebuild_function : obj -> obj;
-  dyn_export_function : obj -> obj option }
+  dyn_rebuild_function : obj -> obj }
 
 let object_tag lobj = Dyn.tag lobj
 
-let cache_tab = 
+let cache_tab =
   (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
 
 let declare_object odecl =
@@ -96,85 +93,79 @@ let declare_object odecl =
   and opener i (oname,lobj) =
     if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj)
     else anomaly "somehow we got the wrong dynamic object in the openfun"
-  and substituter (oname,sub,lobj) = 
+  and substituter (sub,lobj) = 
     if Dyn.tag lobj = na then 
-      infun (odecl.subst_function (oname,sub,outfun lobj))
+      infun (odecl.subst_function (sub,outfun lobj))
     else anomaly "somehow we got the wrong dynamic object in the substfun"
-  and classifier (spopt,lobj) = 
-    if Dyn.tag lobj = na then 
-      match odecl.classify_function (spopt,outfun lobj) with
+  and classifier lobj =
+    if Dyn.tag lobj = na then
+      match odecl.classify_function (outfun lobj) with
 	| Dispose -> Dispose
 	| Substitute obj -> Substitute (infun obj)
 	| Keep obj -> Keep (infun obj)
 	| Anticipate (obj) -> Anticipate (infun obj)
-    else 
+    else
       anomaly "somehow we got the wrong dynamic object in the classifyfun"
-  and discharge (oname,lobj) = 
-    if Dyn.tag lobj = na then 
+  and discharge (oname,lobj) =
+    if Dyn.tag lobj = na then
       Option.map infun (odecl.discharge_function (oname,outfun lobj))
-    else 
+    else
       anomaly "somehow we got the wrong dynamic object in the dischargefun"
-  and rebuild lobj = 
+  and rebuild lobj =
     if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj))
     else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
-  and exporter lobj = 
-    if Dyn.tag lobj = na then 
-      Option.map infun (odecl.export_function (outfun lobj))
-    else 
-      anomaly "somehow we got the wrong dynamic object in the exportfun"
-
-  in 
+  in
   Hashtbl.add cache_tab na { dyn_cache_function = cacher;
 			     dyn_load_function = loader;
                              dyn_open_function = opener;
 			     dyn_subst_function = substituter;
 			     dyn_classify_function = classifier;
 			     dyn_discharge_function = discharge;
-			     dyn_rebuild_function = rebuild;
-                             dyn_export_function = exporter };
+			     dyn_rebuild_function = rebuild };
   (infun,outfun)
 
+let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t)
+
 (* 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. *)
 
 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 -> 
-	  if !relax_flag then
-	    failwith "local to_apply_dyn_fun"
-	  else
-	    error
-	      ("Cannot find library functions for an object with tag "^tag^
-	       " (maybe a plugin is missing)") in 
-	f dodecl
-    with
-	Failure "local to_apply_dyn_fun" -> deflt;;
+  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.warning ("Cannot find library functions for an object with tag "
+                      ^ tag ^ " (a plugin may be missing)");
+          Hashtbl.add missing_tab tag ()
+        end;
+      deflt
 
 let cache_object ((_,lobj) as node) =
   apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj
 
-let load_object i ((_,lobj) as node) = 
+let load_object i ((_,lobj) as node) =
   apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj
 
-let open_object i ((_,lobj) as node) = 
+let open_object i ((_,lobj) as node) =
   apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj
 
-let subst_object ((_,_,lobj) as node) = 
+let subst_object ((_,lobj) as node) = 
   apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj
 
-let classify_object ((_,lobj) as node) = 
-  apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj
+let classify_object lobj =
+  apply_dyn_fun Dispose (fun d -> d.dyn_classify_function lobj) lobj
 
-let discharge_object ((_,lobj) as node) = 
+let discharge_object ((_,lobj) as node) =
   apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
 
-let rebuild_object (lobj as node) =
-  apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj
-
-let export_object lobj =
-  apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj
+let rebuild_object lobj =
+  apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index 4ec5746b..9c0abafd 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libobject.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -18,38 +18,38 @@ open Mod_subst
 
    * a caching function specifying how to add the object in the current
      scope;
-     If the object wishes to register its visibility in the Nametab, 
+     If the object wishes to register its visibility in the Nametab,
      it should do so for all possible sufixes.
 
-   * a loading function, specifying what to do when the module 
-     containing the object is loaded; 
-     If the object wishes to register its visibility in the Nametab, 
-     it should do so for all sufixes no shorter then the "int" argument
+   * a loading function, specifying what to do when the module
+     containing the object is loaded;
+     If the object wishes to register its visibility in the Nametab,
+     it should do so for all sufixes no shorter than the "int" argument
 
-   * an opening function, specifying what to do when the module 
+   * an opening function, specifying what to do when the module
      containing the object is opened (imported);
-     If the object wishes to register its visibility in the Nametab, 
-     it should do so for the sufix of the length the "int" argument
+     If the object wishes to register its visibility in the Nametab,
+     it should do so for the suffix of the length the "int" argument
 
-   * a classification function, specyfying what to do with the object,
+   * a classification function, specifying what to do with the object,
      when the current module (containing the object) is ended;
      The possibilities are:
-     Dispose   - the object dies at the end of the module
-     Substitue - meaning the object is substitutive and 
-                 the module name must be updated
-     Keep      - the object is not substitutive, but survives module 
-                 closing
-     Anticipate - this is for objects which have to be explicitely 
-                 managed by the [end_module] function (like Require 
-                 and Read markers)
+     Dispose    - the object dies at the end of the module
+     Substitute - meaning the object is substitutive and
+                  the module name must be updated
+     Keep       - the object is not substitutive, but survives module
+                  closing
+     Anticipate - this is for objects that have to be explicitely
+                  managed by the [end_module] function (like Require
+                  and Read markers)
 
      The classification function is also an occasion for a cleanup
-     (if this function returns Keep or Substitute of some object, the 
+     (if this function returns Keep or Substitute of some object, the
      cache method is never called for it)
 
-   * a substitution function, performing the substitution; 
-     this function should be declared for substitutive objects 
-     only (see obove)
+   * a substitution function, performing the substitution;
+     this function should be declared for substitutive objects
+     only (see above)
 
    * a discharge function, that is applied at section closing time to
      collect the data necessary to rebuild the discharged form of the
@@ -59,16 +59,9 @@ open Mod_subst
      rebuild the non volatile content of a section from the data
      collected by the discharge function
 
-   * an export function, to enable optional writing of its contents 
-     to disk (.vo). This function is also the oportunity to remove 
-     redundant information in order to keep .vo size small 
-
-     The export function is a little obsolete and will be removed 
-     in the near future... 
-
 *)
 
-type 'a substitutivity = 
+type 'a substitutivity =
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
 type 'a object_declaration = {
@@ -76,13 +69,12 @@ type 'a object_declaration = {
   cache_function : object_name * 'a -> unit;
   load_function : int -> object_name * 'a -> unit;
   open_function : int -> object_name * 'a -> unit;
-  classify_function : object_name * 'a -> 'a substitutivity;
-  subst_function : object_name * substitution * 'a -> 'a;
+  classify_function : 'a -> 'a substitutivity;
+  subst_function :  substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
-  rebuild_function : 'a -> 'a;
-  export_function : 'a -> 'a option }
+  rebuild_function : 'a -> 'a }
 
-(* The default object is a "Keep" object with empty methods. 
+(* The default object is a "Keep" object with empty methods.
    Object creators are advised to use the construction
    [{(default_object "MY_OBJECT") with
       cache_function = ...
@@ -94,7 +86,7 @@ type 'a object_declaration = {
 val default_object : string -> 'a object_declaration
 
 (* the identity substitution function *)
-val ident_subst_function : object_name * substitution * 'a -> 'a
+val ident_subst_function : substitution * 'a -> 'a
 
 (*s Given an object declaration, the function [declare_object]
    will hand back two functions, the "injection" and "projection"
@@ -102,7 +94,7 @@ val ident_subst_function : object_name * substitution * 'a -> 'a
 
 type obj
 
-val declare_object : 
+val declare_object :
   'a object_declaration -> ('a -> obj) * (obj -> 'a)
 
 val object_tag : obj -> string
@@ -110,9 +102,8 @@ val object_tag : obj -> string
 val cache_object : object_name * obj -> unit
 val load_object : int -> object_name * obj -> unit
 val open_object : int -> object_name * obj -> unit
-val subst_object : object_name * substitution * obj -> obj
-val classify_object : object_name * obj -> obj substitutivity
-val export_object : obj -> obj option
+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
diff --git a/library/library.ml b/library/library.ml
index 2c6d02ae..d066ff89 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 13175 2010-06-22 06:28:37Z herbelin $ *)
+(* $Id$ *)
 
 open Pp
 open Util
@@ -39,7 +39,7 @@ let is_in_load_paths phys_dir =
   let dir = System.canonical_path_name phys_dir in
   let lp = get_load_paths () in
   let check_p = fun p -> (String.compare dir p) == 0 in
-    List.exists check_p lp 
+    List.exists check_p lp
 
 let remove_load_path dir =
   load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths
@@ -48,7 +48,7 @@ let add_load_path isroot (phys_path,coq_path) =
   let phys_path = System.canonical_path_name phys_path in
     match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with
       | [_,dir,_] ->
-	  if coq_path <> dir 
+	  if coq_path <> dir
             (* If this is not the default -I . to coqtop *)
             && not
             (phys_path = System.canonical_path_name Filename.current_dir_name
@@ -71,7 +71,7 @@ let add_load_path isroot (phys_path,coq_path) =
 let physical_paths (dp,lp) = dp
 
 let extend_path_with_dirpath p dir =
-  List.fold_left Filename.concat p 
+  List.fold_left Filename.concat p
     (List.map string_of_id (List.rev (repr_dirpath dir)))
 
 let root_paths_matching_dir_path dir =
@@ -112,12 +112,12 @@ let loadpaths_matching_dir_path dir =
 let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths
 
 (************************************************************************)
-(*s Modules on disk contain the following informations (after the magic 
+(*s Modules on disk contain the following informations (after the magic
     number, and before the digest). *)
 
 type compilation_unit_name = dir_path
 
-type library_disk = { 
+type library_disk = {
   md_name : compilation_unit_name;
   md_compiled : compiled_library;
   md_objects : Declaremods.library_objects;
@@ -135,7 +135,7 @@ type library_t = {
   library_imports : compilation_unit_name list;
   library_digest : Digest.t }
 
-module LibraryOrdered = 
+module LibraryOrdered =
   struct
     type t = dir_path
     let compare d1 d2 =
@@ -164,7 +164,7 @@ let freeze () =
   !libraries_imports_list,
   !libraries_exports_list
 
-let unfreeze (mt,mo,mi,me) = 
+let unfreeze (mt,mo,mi,me) =
   libraries_table := mt;
   libraries_loaded_list := mo;
   libraries_imports_list := mi;
@@ -176,13 +176,11 @@ let init () =
   libraries_imports_list := [];
   libraries_exports_list := []
 
-let _ = 
+let _ =
   Summary.declare_summary "MODULES"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_module = false;
-      Summary.survive_section = false }
+      Summary.init_function = init }
 
 (* various requests to the tables *)
 
@@ -197,7 +195,7 @@ let try_find_library dir =
 let register_library_filename dir f =
   (* Not synchronized: overwrite the previous binding if one existed *)
   (* from a previous play of the session *)
-  libraries_filename_table := 
+  libraries_filename_table :=
     LibraryFilenameMap.add dir f !libraries_filename_table
 
 let library_full_filename dir =
@@ -214,13 +212,13 @@ let library_is_loaded dir =
   try let _ = find_library dir in true
   with Not_found -> false
 
-let library_is_opened dir = 
+let library_is_opened dir =
   List.exists (fun m -> m.library_name = dir) !libraries_imports_list
 
 let library_is_exported dir =
   List.exists (fun m -> m.library_name = dir) !libraries_exports_list
 
-let loaded_libraries () = 
+let loaded_libraries () =
   List.map (fun m -> m.library_name) !libraries_loaded_list
 
 let opened_libraries () =
@@ -251,7 +249,7 @@ let rec remember_last_of_each l m =
 
 let register_open_library export m =
   libraries_imports_list := remember_last_of_each !libraries_imports_list m;
-  if export then 
+  if export then
     libraries_exports_list := remember_last_of_each !libraries_exports_list m
 
 (************************************************************************)
@@ -273,14 +271,14 @@ let open_library export explicit_libs m =
     Declaremods.really_import_module (MPfile m.library_name)
   end
   else
-    if export then 
+    if export then
       libraries_exports_list := remember_last_of_each !libraries_exports_list m
 
-(* open_libraries recursively open a list of libraries but opens only once 
+(* open_libraries recursively open a list of libraries but opens only once
    a library that is re-exported many times *)
 
 let open_libraries export modl =
-  let to_open_list = 
+  let to_open_list =
     List.fold_left
       (fun l m ->
          let subimport =
@@ -301,19 +299,16 @@ let open_import i (_,(dir,export)) =
     (* if not (library_is_opened dir) then *)
       open_libraries export [try_find_library dir]
 
-let cache_import obj = 
+let cache_import obj =
   open_import 1 obj
 
-let subst_import (_,_,o) = o
+let subst_import (_,o) = o
 
-let export_import o = Some o
-
-let classify_import (_,(_,export as obj)) = 
+let classify_import (_,export as obj) =
   if export then Substitute obj else Dispose
 
-
 let (in_import, out_import) =
-  declare_object {(default_object "IMPORT LIBRARY") with 
+  declare_object {(default_object "IMPORT LIBRARY") with
        cache_function = cache_import;
        open_function = open_import;
        subst_function = subst_import;
@@ -359,7 +354,7 @@ let locate_qualified_library warn qid =
     if loadpath = [] then raise LibUnmappedDir;
     let name = string_of_id base ^ ".vo" in
     let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in
-    let dir = extend_dirpath (List.assoc lpath loadpath) base in
+    let dir = add_dirpath_suffix (List.assoc lpath loadpath) base in
     (* Look if loaded *)
     if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir)
     (* Otherwise, look for it in the file system *)
@@ -370,7 +365,7 @@ let explain_locate_library_error qid = function
   | LibUnmappedDir ->
       let prefix, _ = repr_qualid qid in
       errorlabstrm "load_absolute_library_from"
-      (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ 
+      (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++
       str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
   | LibNotFound ->
       errorlabstrm "load_absolute_library_from"
@@ -387,14 +382,14 @@ let try_locate_qualified_library (loc,qid) =
   try
     let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in
     dir,f
-  with e -> 
+  with e ->
     explain_locate_library_error qid e
 
 
 (************************************************************************)
 (* Internalise libraries *)
 
-let lighten_library m = 
+let lighten_library m =
   if !Flags.dont_load_proofs then lighten_library m else m
 
 let mk_library md digest = {
@@ -458,7 +453,7 @@ let rec_intern_by_filename_only id f =
   (* We check no other file containing same library is loaded *)
   if library_is_loaded m.library_name then
     begin
-      Flags.if_verbose warning 
+      Flags.if_verbose warning
 	((string_of_dirpath m.library_name)^" is already loaded from file "^
 	library_full_filename m.library_name);
       m.library_name, []
@@ -470,15 +465,15 @@ let rec_intern_by_filename_only id f =
 let rec_intern_library_from_file idopt f =
   (* A name is specified, we have to check it contains library id *)
   let paths = get_load_paths () in
-  let _, f = 
+  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 
+(*s [require_library] loads and possibly opens a library. This is a
     synchronized operation. It is performed as follows:
 
-  preparation phase: (functions require_library* ) the library and its 
+  preparation phase: (functions require_library* ) the library and its
     dependencies are read from to disk (using intern_* )
     [they are read from disk to ensure that at section/module
      discharging time, the physical library referred to outside the
@@ -486,8 +481,8 @@ let rec_intern_library_from_file idopt f =
      the section/module]
 
   execution phase: (through add_leaf and cache_require)
-    the library is loaded in the environment and Nametab, the objects are 
-    registered etc, using functions from Declaremods (via load_library, 
+    the library is loaded in the environment and Nametab, the objects are
+    registered etc, using functions from Declaremods (via load_library,
     which recursively loads its dependencies)
 *)
 
@@ -495,14 +490,14 @@ type library_reference = dir_path list * bool option
 
 let register_library (dir,m) =
   Declaremods.register_library
-    m.library_name 
-    m.library_compiled 
-    m.library_objects 
+    m.library_name
+    m.library_compiled
+    m.library_objects
     m.library_digest;
   register_loaded_library m
 
 (* Follow the semantics of Anticipate object:
-   - called at module or module type closing when a Require occurs in 
+   - called at module or module type closing when a Require occurs in
      the module or module type
    - not called from a library (i.e. a module identified with a file) *)
 let load_require _ (_,(needed,modl,_)) =
@@ -517,22 +512,17 @@ let cache_require o =
   load_require 1 o;
   open_require 1 o
 
-  (* keeps the require marker for closed section replay but removes
-     OS dependent fields from .vo files for cross-platform compatibility *)
-let export_require (_,l,e) = Some ([],l,e)
-
 let discharge_require (_,o) = Some o
 
-(* open_function is never called from here because an Anticipate object *) 
+(* open_function is never called from here because an Anticipate object *)
 
 let (in_require, out_require) =
   declare_object {(default_object "REQUIRE") with
        cache_function = cache_require;
        load_function = load_require;
        open_function = (fun _ _ -> assert false);
-       export_function = export_require;
        discharge_function = discharge_require;
-       classify_function = (fun (_,o) -> Anticipate o) }
+       classify_function = (fun o -> Anticipate o) }
 
 (* Require libraries, import them if [export <> None], mark them for export
    if [export = Some true] *)
@@ -540,11 +530,10 @@ let (in_require, out_require) =
 let xml_require = ref (fun d -> ())
 let set_xml_require f = xml_require := f
 
-let require_library qidl export =
-  let modrefl = List.map try_locate_qualified_library qidl in
+let require_library_from_dirpath modrefl export =
   let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in
   let modrefl = List.map fst modrefl in
-    if Lib.is_modtype () || Lib.is_module () then 
+    if Lib.is_modtype () || Lib.is_module () then
       begin
 	add_anonymous_leaf (in_require (needed,modrefl,None));
 	Option.iter (fun exp ->
@@ -556,6 +545,10 @@ let require_library qidl export =
     if !Flags.xml_export then List.iter !xml_require modrefl;
   add_frozen_state ()
 
+let require_library qidl export =
+  let modrefl = List.map try_locate_qualified_library qidl in
+    require_library_from_dirpath modrefl export
+
 let require_library_from_file idopt file export =
   let modref,needed = rec_intern_library_from_file idopt file in
   let needed = List.rev needed in
@@ -574,7 +567,7 @@ let require_library_from_file idopt file export =
 let import_module export (loc,qid) =
   try
     match Nametab.locate_module qid with
-      | MPfile dir -> 
+      | MPfile dir ->
 	  if Lib.is_modtype () || Lib.is_module () || not export then
 	    add_anonymous_leaf (in_import (dir, export))
 	  else
@@ -586,23 +579,25 @@ let import_module export (loc,qid) =
 	user_err_loc
           (loc,"import_library",
 	  str ((string_of_qualid qid)^" is not a module"))
-  
+
 (************************************************************************)
 (*s Initializing the compilation of a library. *)
 
-let check_coq_overwriting p =
+let check_coq_overwriting p id =
   let l = repr_dirpath p in
   if not !Flags.boot && l <> [] && string_of_id (list_last l) = "Coq" then
-    errorlabstrm "" (strbrk ("Name "^string_of_dirpath p^" starts with prefix \"Coq\" which is reserved for the Coq library."))
+    errorlabstrm ""
+      (strbrk ("Cannot build module "^string_of_dirpath p^"."^string_of_id id^
+      ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
 
-let start_library f = 
+let start_library f =
   let paths = get_load_paths () in
   let _,longf =
     System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
   let ldir0 = find_logical_path (Filename.dirname longf) in
-  check_coq_overwriting ldir0;
   let id = id_of_string (Filename.basename f) in
-  let ldir = extend_dirpath ldir0 id in
+  check_coq_overwriting ldir0 id;
+  let ldir = add_dirpath_suffix ldir0 id in
   Declaremods.start_library ldir;
   ldir,longf
 
@@ -617,15 +612,15 @@ let current_reexports () =
 
 let error_recursively_dependent_library dir =
   errorlabstrm ""
-    (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ 
+    (strbrk "Unable to use logical name " ++ pr_dirpath dir ++
      strbrk " to save current library because" ++
      strbrk " it already depends on a library of this name.")
 
 (* Security weakness: file might have been changed on disk between
-   writing the content and computing the checksum... *) 
+   writing the content and computing the checksum... *)
 let save_library_to dir f =
   let cenv, seg = Declaremods.end_library dir in
-  let md = { 
+  let md = {
     md_name = dir;
     md_compiled = cenv;
     md_objects = seg;
@@ -650,5 +645,5 @@ open Printf
 let mem s =
   let m = try_find_library s in
   h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)"
-		 (size_kb m) (size_kb m.library_compiled) 
+		 (size_kb m) (size_kb m.library_compiled)
 		 (size_kb m.library_objects)))
diff --git a/library/library.mli b/library/library.mli
index d61dc4b9..c6bd8fe0 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: library.mli 11750 2009-01-05 20:47:34Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Util
@@ -26,6 +26,7 @@ open Libobject
 (*s 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 : qualid located list -> bool option -> unit
+val require_library_from_dirpath : (dir_path * string) list -> bool option -> unit
 val require_library_from_file :
   identifier option -> System.physical_path -> bool option -> unit
 
@@ -78,8 +79,5 @@ val locate_qualified_library :
   bool -> qualid -> library_location * dir_path * System.physical_path
 val try_locate_qualified_library : qualid located -> dir_path * string
 
-(* Reserve Coq prefix for the standard library *)
-val check_coq_overwriting : dir_path -> unit
-
 (*s Statistics: display the memory use of a library. *)
 val mem : dir_path -> Pp.std_ppcmds
diff --git a/library/library.mllib b/library/library.mllib
new file mode 100644
index 00000000..4efb69a2
--- /dev/null
+++ b/library/library.mllib
@@ -0,0 +1,16 @@
+Nameops
+Libnames
+Libobject
+Summary
+Nametab
+Global
+Lib
+Declaremods
+Library
+States
+Decl_kinds
+Dischargedhypsmap
+Goptions
+Decls
+Heads
+
diff --git a/library/nameops.ml b/library/nameops.ml
index df9aa95d..28b799f5 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nameops.ml 9433 2006-12-12 09:38:53Z herbelin $ *)
+(* $Id$ *)
 
 open Pp
 open Util
@@ -30,14 +30,14 @@ let cut_ident skip_quote s =
   let slen = String.length s in
   (* [n'] is the position of the first non nullary digit *)
   let rec numpart n n' =
-    if n = 0 then 
+    if n = 0 then
       (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *)
       slen
-    else 
+    else
       let c = Char.code (String.get s (n-1)) in
-      if c = code_of_0 && n <> slen then 
-	numpart (n-1) n' 
-      else if code_of_0 <= c && c <= code_of_9 then 
+      if c = code_of_0 && n <> slen then
+	numpart (n-1) n'
+      else if code_of_0 <= c && c <= code_of_9 then
 	numpart (n-1) (n-1)
       else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then
 	numpart (n-1) (n-1)
@@ -50,14 +50,14 @@ let repr_ident s =
   let numstart = cut_ident false s in
   let s = string_of_id s in
   let slen = String.length s in
-  if numstart = slen then 
+  if numstart = slen then
     (s, None)
   else
     (String.sub s 0 numstart,
      Some (int_of_string (String.sub s numstart (slen - numstart))))
 
 let make_ident sa = function
-  | Some n -> 
+  | Some n ->
       let c = Char.code (String.get sa (String.length sa -1)) in
       let s =
         if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n)
@@ -112,26 +112,8 @@ let add_prefix s id = id_of_string (s ^ string_of_id id)
 
 let atompart_of_id id = fst (repr_ident id)
 
-(* Fresh names *)
-
 let lift_ident = lift_subscript
 
-let next_ident_away id avoid = 
-  if List.mem id avoid then
-    let id0 = if not (has_subscript id) then id else 
-    (* Ce serait sans doute mieux avec quelque chose inspiré de 
-       *** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
-    forget_subscript id in
-    let rec name_rec id =
-      if List.mem id avoid then name_rec (lift_ident id) else id in 
-    name_rec id0
-  else id
-
-let next_ident_away_from id avoid = 
-  let rec name_rec id =
-    if List.mem id avoid then name_rec (lift_ident id) else id in 
-  name_rec id 
-
 (* Names *)
 
 let out_name = function
@@ -143,9 +125,11 @@ let name_fold f na a =
   | Name id -> f id a
   | Anonymous -> a
 
+let name_iter f na = name_fold (fun x () -> f x) na ()
+
 let name_cons na l =
   match na with
-  | Anonymous -> l 
+  | Anonymous -> l
   | Name id -> id::l
 
 let name_app f = function
@@ -156,13 +140,6 @@ let name_fold_map f e = function
   | Name id -> let (e,id) = f e id in (e,Name id)
   | Anonymous -> e,Anonymous
 
-let next_name_away_with_default default name l = 
-  match name with
-    | Name str  -> next_ident_away str l
-    | Anonymous -> next_ident_away (id_of_string default) l
-
-let next_name_away = next_name_away_with_default "H"
-
 let pr_lab l = str (string_of_label l)
 
 let default_library = Names.initial_dir (* = ["Top"] *)
diff --git a/library/nameops.mli b/library/nameops.mli
index b6a39c20..f69bf3ff 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: nameops.mli 9433 2006-12-12 09:38:53Z herbelin $ i*)
+(*i $Id$ i*)
 
 open Names
 
@@ -23,17 +23,14 @@ val root_of_id : identifier -> identifier (* remove trailing digits, $'$ and $\_
 val add_suffix : identifier -> string -> identifier
 val add_prefix : string -> identifier -> identifier
 
-val lift_ident           : identifier -> identifier
-val next_ident_away      : identifier -> identifier list -> identifier
-val next_ident_away_from : identifier -> identifier list -> identifier
-
-val next_name_away : name -> identifier list -> identifier
-val next_name_away_with_default :
-  string -> name -> identifier list -> identifier
+val has_subscript    : identifier -> bool
+val lift_subscript   : identifier -> identifier
+val forget_subscript : identifier -> identifier
 
 val out_name : name -> identifier
 
 val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a
+val name_iter : (identifier -> unit) -> name -> unit
 val name_cons : name -> identifier list -> identifier list
 val name_app : (identifier -> identifier) -> name -> name
 val name_fold_map : ('a -> identifier -> 'a * identifier) -> 'a -> name -> 'a * name
diff --git a/library/nametab.ml b/library/nametab.ml
index 2c794fae..5eafa486 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nametab.ml 10664 2008-03-14 11:27:37Z soubiran $ *)
+(* $Id$ *)
 
 open Util
 open Pp
@@ -27,14 +27,16 @@ let error_global_constant_not_found_loc loc q =
 
 let error_global_not_found q = raise (GlobalizationError q)
 
+(* Kinds of global names *)
 
+type ltac_constant = kernel_name
 
-(* The visibility can be registered either 
+(* The visibility can be registered either
    - for all suffixes not shorter then a given int - when the object
      is loaded inside a module
    or
    - for a precise suffix, when the module containing (the module
-     containing ...) the object is open (imported) 
+     containing ...) the object is open (imported)
 *)
 type visibility = Until of int | Exactly of int
 
@@ -42,9 +44,9 @@ type visibility = Until of int | Exactly of int
 (* Data structure for nametabs *******************************************)
 
 
-(* This module type will be instantiated by [section_path] of [dir_path] *)
+(* This module type will be instantiated by [full_path] of [dir_path] *)
 (* The [repr] function is assumed to return the reversed list of idents. *)
-module type UserName = sig 
+module type UserName = sig
   type t
   val to_string : t -> string
   val repr : t -> identifier * module_ident list
@@ -55,15 +57,15 @@ end
    partially qualified names of type [qualid]. The mapping of
    partially qualified names to ['a] is determined by the [visibility]
    parameter of [push].
-   
+
    The [shortest_qualid] function given a user_name Coq.A.B.x, tries
    to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes
-   the same object. 
+   the same object.
 *)
 module type NAMETREE = sig
   type 'a t
   type user_name
-  
+
   val empty : 'a t
   val push : visibility -> user_name -> 'a -> 'a t -> 'a t
   val locate : qualid -> 'a t -> 'a
@@ -74,15 +76,15 @@ module type NAMETREE = sig
   val find_prefixes : qualid -> 'a t -> 'a list
 end
 
-module Make(U:UserName) : NAMETREE with type user_name = U.t 
-				     = 
+module Make(U:UserName) : NAMETREE with type user_name = U.t
+				     =
 struct
 
   type user_name = U.t
 
-  type 'a path_status = 
-      Nothing 
-    | Relative of user_name * 'a 
+  type 'a path_status =
+      Nothing
+    | Relative of user_name * 'a
     | Absolute of user_name * 'a
 
   (* Dictionaries of short names *)
@@ -91,38 +93,38 @@ struct
   type 'a t = 'a nametree Idmap.t
 
   let empty = Idmap.empty
-		
-  (* [push_until] is used to register [Until vis] visibility and 
+
+  (* [push_until] is used to register [Until vis] visibility and
      [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*)
 
   let rec push_until uname o level (current,dirmap) = function
     | modid :: path ->
-	let mc = 
+	let mc =
 	  try ModIdmap.find modid dirmap
 	  with Not_found -> (Nothing, ModIdmap.empty)
 	in
 	let this =
           if level <= 0 then
 	    match current with
-	      | Absolute (n,_) -> 
-		  (* This is an absolute name, we must keep it 
+	      | Absolute (n,_) ->
+		  (* This is an absolute name, we must keep it
 		     otherwise it may become unaccessible forever *)
 		  Flags.if_verbose
-		    warning ("Trying to mask the absolute name \"" 
-			     ^ U.to_string n ^ "\"!"); 
+		    warning ("Trying to mask the absolute name \""
+			     ^ U.to_string n ^ "\"!");
 		  current
 	      | Nothing
 	      | Relative _ -> Relative (uname,o)
-          else current 
+          else current
 	in
 	let ptab' = push_until uname o (level-1) mc path in
 	  (this, ModIdmap.add modid ptab' dirmap)
-    | [] -> 
+    | [] ->
 	match current with
-	  | Absolute (uname',o') -> 
+	  | Absolute (uname',o') ->
 	      if o'=o then begin
 		assert (uname=uname');
-		current, dirmap 
+		current, dirmap
 		  (* we are putting the same thing for the second time :) *)
 	      end
 	      else
@@ -137,15 +139,15 @@ struct
 
 let rec push_exactly uname o level (current,dirmap) = function
   | modid :: path ->
-      let mc = 
+      let mc =
 	try ModIdmap.find modid dirmap
 	with Not_found -> (Nothing, ModIdmap.empty)
       in
         if level = 0 then
 	  let this =
 	    match current with
-	      | Absolute (n,_) -> 
-		  (* This is an absolute name, we must keep it 
+	      | Absolute (n,_) ->
+		  (* This is an absolute name, we must keep it
 		     otherwise it may become unaccessible forever *)
 		  Flags.if_verbose
 		    warning ("Trying to mask the absolute name \""
@@ -158,7 +160,7 @@ let rec push_exactly uname o level (current,dirmap) = function
 	else (* not right level *)
 	  let ptab' = push_exactly uname o (level-1) mc path in
 	    (current, ModIdmap.add modid ptab' dirmap)
-  | [] -> 
+  | [] ->
       anomaly "Prefix longer than path! Impossible!"
 
 
@@ -166,7 +168,7 @@ let push visibility uname o tab =
   let id,dir = U.repr uname in
   let ptab =
     try Idmap.find id tab
-    with Not_found -> (Nothing, ModIdmap.empty) 
+    with Not_found -> (Nothing, ModIdmap.empty)
   in
   let ptab' = match visibility with
     | Until i -> push_until uname o (i-1) ptab dir
@@ -178,46 +180,46 @@ let push visibility uname o tab =
 let rec search (current,modidtab) = function
   | modid :: path -> search (ModIdmap.find modid modidtab) path
   | [] -> current
-      
+
 let find_node qid tab =
   let (dir,id) = repr_qualid qid in
     search (Idmap.find id tab) (repr_dirpath dir)
 
-let locate qid tab = 
+let locate qid tab =
   let o = match find_node qid tab with
     | Absolute (uname,o) | Relative (uname,o) -> o
-    | Nothing -> raise Not_found                                            
+    | Nothing -> raise Not_found
   in
     o
 
 let user_name qid tab =
   let uname = match find_node qid tab with
     | Absolute (uname,o) | Relative (uname,o) -> uname
-    | Nothing -> raise Not_found                                            
+    | Nothing -> raise Not_found
   in
     uname
-  
-let find uname tab = 
+
+let find uname tab =
   let id,l = U.repr uname in
     match search (Idmap.find id tab) l with
 	Absolute (_,o) -> o
       | _ -> raise Not_found
 
 let exists uname tab =
-  try 
+  try
     let _ = find uname tab in
       true
   with
       Not_found -> false
 
-let shortest_qualid ctx uname tab = 
+let shortest_qualid ctx uname tab =
   let id,dir = U.repr uname in
   let hidden = Idset.mem id ctx in
   let rec find_uname pos dir (path,tab) = match path with
     | Absolute (u,_) | Relative (u,_)
           when u=uname && not(pos=[] && hidden) -> List.rev pos
-    | _ -> 
-	match dir with 
+    | _ ->
+	match dir with
 	    [] -> raise Not_found
 	  | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tab)
   in
@@ -237,7 +239,7 @@ let rec flatten_idmap tab l =
 let rec search_prefixes (current,modidtab) = function
   | modid :: path -> search_prefixes (ModIdmap.find modid modidtab) path
   | [] -> List.rev (flatten_idmap  modidtab (push_node current []))
-      
+
 let find_prefixes qid tab =
   try
     let (dir,id) = repr_qualid qid in
@@ -250,10 +252,10 @@ end
 
 (* Global name tables *************************************************)
 
-module SpTab = Make (struct 
-		       type t = section_path
+module SpTab = Make (struct
+		       type t = full_path
 		       let to_string = string_of_path
-		       let repr sp = 
+		       let repr sp =
 			 let dir,id = repr_path sp in
 			   id, (repr_dirpath dir)
 		     end)
@@ -268,11 +270,8 @@ let the_tactictab = ref (SpTab.empty : kntab)
 type mptab = module_path SpTab.t
 let the_modtypetab = ref (SpTab.empty : mptab)
 
-type objtab = unit SpTab.t
-let the_objtab = ref (SpTab.empty : objtab)
-
 
-module DirTab = Make(struct 
+module DirTab = Make(struct
 		       type t = dir_path
 		       let to_string = string_of_dirpath
 		       let repr dir = match repr_dirpath dir with
@@ -289,22 +288,22 @@ let the_dirtab = ref (DirTab.empty : dirtab)
 (* Reversed name tables ***************************************************)
 
 (* This table translates extended_global_references back to section paths *)
-module Globrevtab = Map.Make(struct 
-			       type t=extended_global_reference 
-			       let compare = compare 
+module Globrevtab = Map.Make(struct
+			       type t=extended_global_reference
+			       let compare = compare
 			     end)
 
-type globrevtab = section_path Globrevtab.t
+type globrevtab = full_path Globrevtab.t
 let the_globrevtab = ref (Globrevtab.empty : globrevtab)
 
 
 type mprevtab = dir_path MPmap.t
 let the_modrevtab = ref (MPmap.empty : mprevtab)
 
-type mptrevtab = section_path MPmap.t
+type mptrevtab = full_path MPmap.t
 let the_modtyperevtab = ref (MPmap.empty : mptrevtab)
 
-type knrevtab = section_path KNmap.t
+type knrevtab = full_path KNmap.t
 let the_tacticrevtab = ref (KNmap.empty : knrevtab)
 
 
@@ -315,43 +314,45 @@ let the_tacticrevtab = ref (KNmap.empty : knrevtab)
    Parameter but also Remark and Fact) *)
 
 let push_xref visibility sp xref =
-  the_ccitab := SpTab.push visibility sp xref !the_ccitab;
   match visibility with
-    | Until _ -> 
-	if Globrevtab.mem xref !the_globrevtab then
-	  ()
-	else
-	  the_globrevtab := Globrevtab.add xref sp !the_globrevtab
-    | _ -> ()
+    | Until _ ->
+	the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+	the_globrevtab := Globrevtab.add xref sp !the_globrevtab
+    | _ ->
+	begin
+	  if SpTab.exists sp !the_ccitab then
+	    match SpTab.find sp !the_ccitab with
+	      | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) |
+		    TrueGlobal( ConstructRef _) as xref ->
+		  the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+	      | _ -> 
+		  the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+	    else
+	      the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+	end
 
 let push_cci visibility sp ref =
   push_xref visibility sp (TrueGlobal ref)
-
+    
 (* This is for Syntactic Definitions *)
-let push_syntactic_definition visibility sp kn =
-  push_xref visibility sp (SyntacticDef kn)
+let push_syndef visibility sp kn =
+  push_xref visibility sp (SynDef kn)
 
 let push = push_cci
 
-let push_modtype vis sp kn = 
+let push_modtype vis sp kn =
   the_modtypetab := SpTab.push vis sp kn !the_modtypetab;
   the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab
 
 (* This is for tactic definition names *)
 
-let push_tactic vis sp kn = 
+let push_tactic vis sp kn =
   the_tactictab := SpTab.push vis sp kn !the_tactictab;
   the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab
 
 
-(* This is for dischargeable non-cci objects (removed at the end of the
-   section -- i.e. Hints, Grammar ...) *) (* --> Unused *)
-
-let push_object visibility sp =
-  the_objtab := SpTab.push visibility sp () !the_objtab
-
 (* This is to remember absolute Section/Module names and to avoid redundancy *)
-let push_dir vis dir dir_ref = 
+let push_dir vis dir dir_ref =
   the_dirtab := DirTab.push vis dir dir_ref !the_dirtab;
   match dir_ref with
       DirModule (_,(mp,_)) -> the_modrevtab := MPmap.add mp dir !the_modrevtab
@@ -362,77 +363,75 @@ let push_dir vis dir dir_ref =
 
 
 (* This should be used when syntactic definitions are allowed *)
-let extended_locate qid = SpTab.locate qid !the_ccitab
+let locate_extended qid = SpTab.locate qid !the_ccitab
 
 (* This should be used when no syntactic definitions is expected *)
-let locate qid = match extended_locate qid with
+let locate qid = match locate_extended qid with
   | TrueGlobal ref -> ref
-  | SyntacticDef _ -> raise Not_found
+  | SynDef _ -> raise Not_found
 let full_name_cci qid = SpTab.user_name qid !the_ccitab
 
-let locate_syntactic_definition qid = match extended_locate qid with
+let locate_syndef qid = match locate_extended qid with
   | TrueGlobal _ -> raise Not_found
-  | SyntacticDef kn -> kn
+  | SynDef kn -> kn
 
 let locate_modtype qid = SpTab.locate qid !the_modtypetab
 let full_name_modtype qid = SpTab.user_name qid !the_modtypetab
 
-let locate_obj qid = SpTab.user_name qid !the_objtab
-
-type ltac_constant = kernel_name
 let locate_tactic qid = SpTab.locate qid !the_tactictab
 let full_name_tactic qid = SpTab.user_name qid !the_tactictab
 
 let locate_dir qid = DirTab.locate qid !the_dirtab
 
-let locate_module qid = 
+let locate_module qid =
   match locate_dir qid with
     | DirModule (_,(mp,_)) -> mp
     | _ -> raise Not_found
 
-let full_name_module qid = 
+let full_name_module qid =
   match locate_dir qid with
     | DirModule (dir,_) -> dir
     | _ -> raise Not_found
 
 let locate_section qid =
   match locate_dir qid with
-    | DirOpenSection (dir, _) 
+    | DirOpenSection (dir, _)
     | DirClosedSection dir -> dir
     | _ -> raise Not_found
 
-let locate_all qid = 
+let locate_all qid =
   List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l)
     (SpTab.find_prefixes qid !the_ccitab) []
 
-let extended_locate_all qid = SpTab.find_prefixes qid !the_ccitab
+let locate_extended_all qid = SpTab.find_prefixes qid !the_ccitab
 
 (* Derived functions *)
 
 let locate_constant qid =
-  match extended_locate qid with
+  match locate_extended qid with
     | TrueGlobal (ConstRef kn) -> kn
     | _ -> raise Not_found
 
-let locate_mind qid = 
-  match extended_locate qid with
+let locate_mind qid =
+  match locate_extended qid with
     | TrueGlobal (IndRef (kn,0)) -> kn
     | _ -> raise Not_found
 
-
-let absolute_reference sp =
+let global_of_path sp =
   match SpTab.find sp !the_ccitab with
     | TrueGlobal ref -> ref
     | _ -> raise Not_found
 
+let extended_global_of_path sp = SpTab.find sp !the_ccitab
+
 let locate_in_absolute_module dir id =
-  absolute_reference (make_path dir id)
+  global_of_path (make_path dir id)
 
 let global r =
   let (loc,qid) = qualid_of_reference r in
-  try match extended_locate qid with
+  try match locate_extended qid with
     | TrueGlobal ref -> ref
-    | SyntacticDef _ -> 
+    | SynDef _ ->
         user_err_loc (loc,"global",
           str "Unexpected reference to a notation: " ++
           pr_qualid qid)
@@ -442,7 +441,7 @@ let global r =
 (* Exists functions ********************************************************)
 
 let exists_cci sp = SpTab.exists sp !the_ccitab
-      
+
 let exists_dir dir = DirTab.exists dir !the_dirtab
 
 let exists_section = exists_dir
@@ -455,37 +454,40 @@ let exists_tactic sp = SpTab.exists sp !the_tactictab
 
 (* Reverse locate functions ***********************************************)
 
-let sp_of_global ref = 
+let path_of_global ref =
   match ref with
     | VarRef id -> make_path empty_dirpath id
     | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
 
+let dirpath_of_global ref =
+  fst (repr_path (path_of_global ref))
 
-let id_of_global ref = 
-  let (_,id) = repr_path (sp_of_global ref) in 
-  id
+let basename_of_global ref =
+  snd (repr_path (path_of_global ref))
 
-let sp_of_syntactic_definition kn = 
-  Globrevtab.find (SyntacticDef kn) !the_globrevtab
+let path_of_syndef kn =
+  Globrevtab.find (SynDef kn) !the_globrevtab
 
-let dir_of_mp mp =
+let dirpath_of_module mp =
   MPmap.find mp !the_modrevtab
 
+let path_of_tactic kn =
+  KNmap.find kn !the_tacticrevtab
 
 (* Shortest qualid functions **********************************************)
 
-let shortest_qualid_of_global ctx ref = 
+let shortest_qualid_of_global ctx ref =
   match ref with
     | VarRef id -> make_qualid empty_dirpath id
     | _ ->
         let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
         SpTab.shortest_qualid ctx sp !the_ccitab
 
-let shortest_qualid_of_syndef ctx kn = 
-  let sp = sp_of_syntactic_definition kn in
+let shortest_qualid_of_syndef ctx kn =
+  let sp = path_of_syndef kn in
     SpTab.shortest_qualid ctx sp !the_ccitab
 
-let shortest_qualid_of_module mp = 
+let shortest_qualid_of_module mp =
   let dir = MPmap.find mp !the_modrevtab in
     DirTab.shortest_qualid Idset.empty dir !the_dirtab
 
@@ -504,7 +506,7 @@ let pr_global_env env ref =
   let s = string_of_qualid (shortest_qualid_of_global env ref) in
   (str s)
 
-let inductive_of_reference r =
+let global_inductive r =
   match global r with
   | IndRef ind -> ind
   | ref ->
@@ -517,13 +519,12 @@ let inductive_of_reference r =
 (********************************************************************)
 (* Registration of tables as a global table and rollback            *)
 
-type frozen = ccitab * dirtab * objtab * kntab * kntab
+type frozen = ccitab * dirtab * kntab * kntab
     * globrevtab * mprevtab * knrevtab * knrevtab
 
-let init () = 
-  the_ccitab := SpTab.empty; 
+let init () =
+  the_ccitab := SpTab.empty;
   the_dirtab := DirTab.empty;
-  the_objtab := SpTab.empty;
   the_modtypetab := SpTab.empty;
   the_tactictab := SpTab.empty;
   the_globrevtab := Globrevtab.empty;
@@ -534,9 +535,8 @@ let init () =
 
 
 let freeze () =
-  !the_ccitab, 
+  !the_ccitab,
   !the_dirtab,
-  !the_objtab,
   !the_modtypetab,
   !the_tactictab,
   !the_globrevtab,
@@ -544,10 +544,9 @@ let freeze () =
   !the_modtyperevtab,
   !the_tacticrevtab
 
-let unfreeze (ccit,dirt,objt,mtyt,tact,globr,modr,mtyr,tacr) =
+let unfreeze (ccit,dirt,mtyt,tact,globr,modr,mtyr,tacr) =
   the_ccitab := ccit;
   the_dirtab := dirt;
-  the_objtab := objt;
   the_modtypetab := mtyt;
   the_tactictab := tact;
   the_globrevtab := globr;
@@ -555,10 +554,13 @@ let unfreeze (ccit,dirt,objt,mtyt,tact,globr,modr,mtyr,tacr) =
   the_modtyperevtab := mtyr;
   the_tacticrevtab := tacr
 
-let _ = 
+let _ =
   Summary.declare_summary "names"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_module = false;
-      Summary.survive_section = false }
+      Summary.init_function = init }
+
+(* Deprecated synonyms *)
+
+let extended_locate = locate_extended
+let absolute_reference = global_of_path
diff --git a/library/nametab.mli b/library/nametab.mli
index 71ea0aa5..b168d59c 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: nametab.mli 10497 2008-02-01 12:18:37Z soubiran $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Util
@@ -16,34 +16,52 @@ open Libnames
 (*i*)
 
 (*s This module contains the tables for globalization, which
-  associates internal object references to qualified names (qualid). *)
+    associates internal object references to qualified names (qualid).
+
+    There are three classes of names:
+
+    1a- internal kernel names: [kernel_name], [constant], [inductive],
+        [module_path], [dir_path]
+
+    1b- other internal names: [global_reference], [syndef_name],
+        [extended_global_reference], [global_dir_reference], ...
+
+    2- full, non ambiguous user names: [full_path]
+
+    3- non necessarily full, possibly ambiguous user names: [reference]
+       and [qualid]
+*)
 
 (* Most functions in this module fall into one of the following categories:
    \begin{itemize}
    \item [push : visibility -> full_user_name -> object_reference -> unit]
-   
+
    Registers the [object_reference] to be referred to by the
    [full_user_name] (and its suffixes according to [visibility]).
-   [full_user_name] can either be a [section_path] or a [dir_path].
+   [full_user_name] can either be a [full_path] or a [dir_path].
+
+   \item [exists : full_user_name -> bool]
 
-   \item [exists : full_user_name -> bool] 
-   
    Is the [full_user_name] already atributed as an absolute user name
-   of some object? 
+   of some object?
 
    \item [locate : qualid -> object_reference]
 
    Finds the object referred to by [qualid] or raises [Not_found]
-   
-   \item [name_of : object_reference -> user_name]
 
-   The [user_name] can be for example the shortest non ambiguous [qualid] or 
-   the [full_user_name] or [identifier]. Such a function can also have a 
-   local context argument. 
+   \item [full_name : qualid -> full_user_name]
+
+   Finds the full user name referred to by [qualid] or raises [Not_found]
+
+   \item [shortest_qualid_of : object_reference -> user_name]
+
+   The [user_name] can be for example the shortest non ambiguous [qualid] or
+   the [full_user_name] or [identifier]. Such a function can also have a
+   local context argument.
    \end{itemize}
 *)
-   
-  
+
+
 exception GlobalizationError of qualid
 exception GlobalizationConstantError of qualid
 
@@ -52,9 +70,6 @@ val error_global_not_found_loc : loc -> qualid -> 'a
 val error_global_not_found     : qualid -> 'a
 val error_global_constant_not_found_loc : loc -> qualid -> 'a
 
-
-
-
 (*s Register visibility of things *)
 
 (* The visibility can be registered either
@@ -64,93 +79,84 @@ val error_global_constant_not_found_loc : loc -> qualid -> 'a
    object is loaded inside a module -- or
 
    \item for a precise suffix, when the module containing (the module
-   containing ...) the object is opened (imported) 
+   containing ...) the object is opened (imported)
    \end{itemize}
 *)
 
 type visibility = Until of int | Exactly of int
 
-val push : visibility -> section_path -> global_reference -> unit
-val push_syntactic_definition : 
-  visibility -> section_path -> kernel_name -> unit
-val push_modtype : visibility -> section_path -> module_path -> unit
+val push : visibility -> full_path -> global_reference -> unit
+val push_modtype : visibility -> full_path -> module_path -> unit
 val push_dir : visibility -> dir_path -> global_dir_reference -> unit
-val push_object : visibility -> section_path -> unit
-val push_tactic : visibility -> section_path -> kernel_name -> unit
-
-
-(*s The following functions perform globalization of qualified names *)
+val push_syndef : visibility -> full_path -> syndef_name -> unit
 
-(* This returns the section path of a constant or fails with [Not_found] *)
-val locate : qualid -> global_reference
-
-(* This function is used to transform a qualified identifier into a
-   global reference, with a nice error message in case of failure *)
-val global : reference -> global_reference
-
-(* The same for inductive types *)
-val inductive_of_reference : reference -> inductive
-
-(* This locates also syntactic definitions; raise [Not_found] if not found *)
-val extended_locate : qualid -> extended_global_reference
+type ltac_constant = kernel_name
+val push_tactic : visibility -> full_path -> ltac_constant -> unit
 
-(* This locates all names with a given suffix, if qualid is valid as
-   such, it comes first in the list *)
-val extended_locate_all : qualid -> extended_global_reference list
 
-(* This locates all global references with a given suffixe *)
-val locate_all : qualid -> global_reference list
+(*s The following functions perform globalization of qualified names *)
 
-val locate_obj : qualid -> section_path
+(* These functions globalize a (partially) qualified name or fail with
+   [Not_found] *)
 
+val locate : qualid -> global_reference
+val locate_extended : qualid -> extended_global_reference
 val locate_constant : qualid -> constant
-val locate_mind : qualid -> mutual_inductive
-val locate_section : qualid -> dir_path
+val locate_syndef : qualid -> syndef_name
 val locate_modtype : qualid -> module_path
-val locate_syntactic_definition : qualid -> kernel_name
-
-type ltac_constant = kernel_name
-val locate_tactic : qualid -> ltac_constant
 val locate_dir : qualid -> global_dir_reference
 val locate_module : qualid -> module_path
+val locate_section : qualid -> dir_path
+val locate_tactic : qualid -> ltac_constant
 
-(* A variant looking up a [section_path] *)
-val absolute_reference : section_path -> global_reference
+(* These functions globalize user-level references into global
+   references, like [locate] and co, but raise a nice error message
+   in case of failure *)
 
+val global : reference -> global_reference
+val global_inductive : reference -> inductive
 
-(*s These function tell if the given absolute name is already taken *)
+(* These functions locate all global references with a given suffix;
+   if [qualid] is valid as such, it comes first in the list *)
 
-val exists_cci : section_path -> bool
-val exists_modtype : section_path -> bool
+val locate_all : qualid -> global_reference list
+val locate_extended_all : qualid -> extended_global_reference list
 
-(* Those three functions are the same *)
-val exists_dir : dir_path -> bool
-val exists_section : dir_path -> bool (* deprecated *)
-val exists_module : dir_path -> bool (* deprecated *)
+(* Mapping a full path to a global reference *)
 
+val global_of_path : full_path -> global_reference
+val extended_global_of_path : full_path -> extended_global_reference
 
-(*s These functions turn qualids into full user names: [section_path]s
-  or [dir_path]s *)
+(*s These functions tell if the given absolute name is already taken *)
 
-val full_name_modtype : qualid -> section_path
-val full_name_cci : qualid -> section_path
+val exists_cci : full_path -> bool
+val exists_modtype : full_path -> bool
+val exists_dir : dir_path -> bool
+val exists_section : dir_path -> bool (* deprecated synonym of [exists_dir] *)
+val exists_module : dir_path -> bool (* deprecated synonym of [exists_dir] *)
 
-(* As above but checks that the path found is indeed a module *)
-val full_name_module : qualid -> dir_path
+(*s These functions locate qualids into full user names *)
 
+val full_name_cci : qualid -> full_path
+val full_name_modtype : qualid -> full_path
+val full_name_module : qualid -> dir_path
 
 (*s Reverse lookup -- finding user names corresponding to the given
   internal name *)
 
-val sp_of_syntactic_definition : kernel_name -> section_path
-val shortest_qualid_of_global : Idset.t -> global_reference -> qualid
-val shortest_qualid_of_syndef : Idset.t -> kernel_name -> qualid
-val shortest_qualid_of_tactic : ltac_constant -> qualid
+(* Returns the full path bound to a global reference or syntactic
+   definition, and the (full) dirpath associated to a module path *)
+
+val path_of_syndef : syndef_name -> full_path
+val path_of_global : global_reference -> full_path
+val dirpath_of_module : module_path -> dir_path
+val path_of_tactic : ltac_constant -> full_path
 
-val dir_of_mp : module_path -> dir_path
+(* Returns in particular the dirpath or the basename of the full path
+   associated to global reference *)
 
-val sp_of_global : global_reference -> section_path
-val id_of_global : global_reference -> identifier
+val dirpath_of_global : global_reference -> dir_path
+val basename_of_global : global_reference -> identifier
 
 (* Printing of global references using names as short as possible *)
 val pr_global_env : Idset.t -> global_reference -> std_ppcmds
@@ -160,13 +166,13 @@ val pr_global_env : Idset.t -> global_reference -> std_ppcmds
    Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and
    Coq.A.B.x that denotes the same object. *)
 
-val shortest_qualid_of_module : module_path -> qualid
+val shortest_qualid_of_global : Idset.t -> global_reference -> qualid
+val shortest_qualid_of_syndef : Idset.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : module_path -> qualid
+val shortest_qualid_of_module : module_path -> qualid
+val shortest_qualid_of_tactic : ltac_constant -> qualid
 
+(* Deprecated synonyms *)
 
-(*
-type frozen
-
-val freeze : unit -> frozen
-val unfreeze : frozen -> unit
-*)
+val extended_locate : qualid -> extended_global_reference (*= locate_extended *)
+val absolute_reference : full_path -> global_reference (* = global_of_path *)
diff --git a/library/states.ml b/library/states.ml
index 3a4be1ca..b2ece049 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: states.ml 13175 2010-06-22 06:28:37Z herbelin $ *)
+(* $Id$ *)
 
 open System
 
@@ -32,14 +32,14 @@ let (extern_state,intern_state) =
 
 let with_heavy_rollback f x =
   let st = freeze () in
-  try 
+  try
     f x
   with reraise ->
     (unfreeze st; raise reraise)
 
 let with_state_protection f x =
   let st = freeze () in
-  try 
+  try
     let a = f x in unfreeze st; a
   with reraise ->
     (unfreeze st; raise reraise)
diff --git a/library/states.mli b/library/states.mli
index 210e06b2..782e41ca 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: states.mli 12080 2009-04-11 16:56:20Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*s States of the system. In that module, we provide functions to get
   and set the state of the whole system. Internally, it is done by
-  freezing the states of both [Lib] and [Summary]. We provide functions 
+  freezing the states of both [Lib] and [Summary]. We provide functions
   to write and restore state to and from a given file. *)
 
 val intern_state : string -> unit
@@ -21,7 +21,7 @@ val freeze : unit -> state
 val unfreeze : state -> unit
 
 (*s Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the
-  state of the whole system as it was before the evaluation if an exception 
+  state of the whole system as it was before the evaluation if an exception
   is raised. *)
 
 val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
diff --git a/library/summary.ml b/library/summary.ml
index 455ee264..e9b0bbd3 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: summary.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id$ *)
 
 open Pp
 open Util
@@ -14,11 +14,9 @@ open Util
 type 'a summary_declaration = {
   freeze_function : unit -> 'a;
   unfreeze_function : 'a -> unit;
-  init_function : unit -> unit;
-  survive_module : bool ;
-  survive_section : bool }
+  init_function : unit -> unit }
 
-let summaries = 
+let summaries =
   (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t)
 
 let internal_declare_summary sumname sdecl =
@@ -29,45 +27,32 @@ let internal_declare_summary sumname sdecl =
   let ddecl = {
     freeze_function = dyn_freeze;
     unfreeze_function = dyn_unfreeze;
-    init_function = dyn_init;
-    survive_module = sdecl.survive_module;
-    survive_section = sdecl.survive_section } 
+    init_function = dyn_init }
   in
   if Hashtbl.mem summaries sumname then
     anomalylabstrm "Summary.declare_summary"
       (str "Cannot declare a summary twice: " ++ str sumname);
   Hashtbl.add summaries sumname ddecl
 
-let declare_summary sumname decl = 
+let declare_summary sumname decl =
   internal_declare_summary (sumname^"-SUMMARY") decl
 
 type frozen = Dyn.t Stringmap.t
 
 let freeze_summaries () =
   let m = ref Stringmap.empty in
-  Hashtbl.iter 
+  Hashtbl.iter
     (fun id decl -> m := Stringmap.add id (decl.freeze_function()) !m)
     summaries;
   !m
 
 
-let unfreeze_some_summaries p fs = 
+let unfreeze_summaries fs =
   Hashtbl.iter
-    (fun id decl -> 
-       try 
-	 if p decl then
-	   decl.unfreeze_function (Stringmap.find id fs)
+    (fun id decl ->
+       try decl.unfreeze_function (Stringmap.find id fs)
        with Not_found -> decl.init_function())
     summaries
 
-let unfreeze_summaries = 
-  unfreeze_some_summaries (fun _ -> true)
-
-let section_unfreeze_summaries =
-  unfreeze_some_summaries (fun decl -> not decl.survive_section)
-
-let module_unfreeze_summaries =
-  unfreeze_some_summaries (fun decl -> not decl.survive_module)
-
 let init_summaries () =
   Hashtbl.iter (fun _ decl -> decl.init_function()) summaries
diff --git a/library/summary.mli b/library/summary.mli
index ba527bdf..e6e17ef8 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: summary.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id$ i*)
 
 (* This module registers the declaration of global tables, which will be kept
    in synchronization during the various backtracks of the system. *)
@@ -14,9 +14,7 @@
 type 'a summary_declaration = {
   freeze_function : unit -> 'a;
   unfreeze_function : 'a -> unit;
-  init_function : unit -> unit;
-  survive_module : bool;    (* should be false is most cases *)
-  survive_section : bool }
+  init_function : unit -> unit }
 
 val declare_summary : string -> 'a summary_declaration -> unit
 
@@ -24,9 +22,11 @@ type frozen
 
 val freeze_summaries : unit -> frozen
 val unfreeze_summaries : frozen -> unit
-val section_unfreeze_summaries : frozen -> unit
-val module_unfreeze_summaries : frozen -> unit
 val init_summaries : unit -> unit
 
-
+(** Beware: if some code is dynamically loaded via dynlink after the
+    initialization of Coq, the init functions of any summary declared
+    by this code may not be run. It is hence the responsability of
+    plugins to initialize themselves properly.
+*)