From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 library/decl_kinds.ml         |  70 ++++--
 library/declare.ml            | 262 ++++++++++-----------
 library/declare.mli           |  37 +--
 library/declaremods.ml        |  74 +++---
 library/declaremods.mli       |  19 +-
 library/dischargedhypsmap.ml  |   9 +-
 library/dischargedhypsmap.mli |   2 +-
 library/global.ml             |  19 +-
 library/global.mli            |  11 +-
 library/goptions.ml           |   3 +-
 library/goptions.mli          |   3 +-
 library/impargs.ml            | 190 +++++-----------
 library/impargs.mli           |   8 +-
 library/lib.ml                | 215 +++++++++++++-----
 library/lib.mli               |  43 +++-
 library/libnames.ml           |  61 ++---
 library/libnames.mli          |  23 +-
 library/libobject.ml          |  15 +-
 library/libobject.mli         |   5 +-
 library/library.ml            | 514 ++++++++++++++++++------------------------
 library/library.mli           |  94 ++++----
 library/nameops.ml            |   6 +-
 library/nameops.mli           |   4 +-
 library/nametab.ml            |   6 +-
 library/nametab.mli           |   2 +-
 library/states.ml             |   4 +-
 library/states.mli            |   2 +-
 library/summary.ml            |   2 +-
 library/summary.mli           |   2 +-
 29 files changed, 837 insertions(+), 868 deletions(-)
 mode change 100755 => 100644 library/nametab.ml

(limited to 'library')

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index a030284c..af54df2f 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -6,7 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_kinds.ml,v 1.6.2.1 2004/07/16 19:30:33 herbelin Exp $ *)
+(* $Id: decl_kinds.ml 7944 2006-01-29 16:01:32Z herbelin $ *)
+
+open Util
 
 (* Informal mathematical status of declarations *)
 
@@ -14,23 +16,32 @@ type locality_flag = (*bool (* local = true; global = false *)*)
   | Local
   | Global
 
-(* Kinds used at parsing time *)
+type boxed_flag = bool
 
 type theorem_kind =
   | Theorem
   | Lemma
   | Fact
   | Remark
+  | Property
+  | Proposition
+  | Corollary
 
 type definition_object_kind =
   | Definition
   | Coercion
   | SubClass
   | CanonicalStructure
+  | Example
+  | Fixpoint
+  | CoFixpoint
+  | Scheme
+  | StructureComponent
+  | IdentityCoercion
 
 type strength = locality_flag (* For compatibility *)
 
-type type_as_formula_kind = Definitional | Logical | Conjectural
+type assumption_object_kind = Definitional | Logical | Conjectural
 
 (* [assumption_kind] 
 
@@ -40,36 +51,51 @@ type type_as_formula_kind = Definitional | Logical | Conjectural
    Logical      |  Hypothesis | Axiom
 
 *)
-type assumption_kind = locality_flag * type_as_formula_kind
+type assumption_kind = locality_flag * assumption_object_kind
 
-type definition_kind = locality_flag * definition_object_kind
+type definition_kind = locality_flag * boxed_flag * definition_object_kind
 
 (* Kinds used in proofs *)
 
-type global_goal_kind =
-  | DefinitionBody
+type goal_object_kind =
+  | DefinitionBody of definition_object_kind
   | Proof of theorem_kind
 
-type goal_kind =
-  | IsGlobal of global_goal_kind
-  | IsLocal
+type goal_kind = locality_flag * goal_object_kind
 
 (* Kinds used in library *)
 
-type local_theorem_kind = LocalStatement
-
-type 'a mathematical_kind =
-  | IsAssumption of type_as_formula_kind
-  | IsDefinition
-  | IsConjecture
-  | IsProof of 'a
-
-type global_kind = theorem_kind mathematical_kind
-type local_kind = local_theorem_kind mathematical_kind
+type logical_kind =
+  | IsAssumption of assumption_object_kind
+  | IsDefinition of definition_object_kind
+  | IsProof of theorem_kind
 
 (* Utils *)
 
-let theorem_kind_of_goal_kind = function
-  | DefinitionBody -> IsDefinition
+let logical_kind_of_goal_kind = function
+  | DefinitionBody d -> IsDefinition d
   | Proof s -> IsProof s
 
+let string_of_theorem_kind = function
+  | Theorem -> "Theorem"
+  | Lemma -> "Lemma"
+  | Fact -> "Fact"
+  | Remark -> "Remark"
+  | Property -> "Property"
+  | Proposition -> "Proposition"
+  | Corollary -> "Corollary"
+
+let string_of_definition_kind (l,boxed,d) =
+  match (l,d) with
+  | Local, Coercion -> "Coercion Local"
+  | Global, Coercion -> "Coercion"
+  | Local, Definition -> "Let"
+  | Global, Definition -> if boxed then "Boxed Definition" else "Definition"
+  | Local, SubClass -> "Local SubClass"
+  | Global, SubClass -> "SubClass"
+  | Global, CanonicalStructure -> "Canonical Structure"
+  | Global, Example -> "Example"
+  | Local, (CanonicalStructure|Example) ->
+      anomaly "Unsupported local definition kind"
+  | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion)
+      -> anomaly "Internal definition kind"
diff --git a/library/declare.ml b/library/declare.ml
index cfa8890a..b1e55c20 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: declare.ml,v 1.128.2.2 2005/11/29 21:40:52 letouzey Exp $ *)
+(* $Id: declare.ml 7941 2006-01-28 23:07:59Z herbelin $ *)
 
 open Pp
 open Util
@@ -31,11 +31,7 @@ open Decl_kinds
 
 (**********************************************)
 
-(* For [DischargeAt (dir,n)], [dir] is the minimum prefix that a
-   construction keeps in its name (if persistent), or the section name
-   beyond which it is discharged (if volatile); the integer [n]
-   (useful only for persistent constructions), is the length of the section
-   part in [dir] *)
+(* Strength *)
 
 open Nametab
 
@@ -47,9 +43,9 @@ let string_of_strength = function
   | Global -> "(global)"
 
 (* XML output hooks *)
-let xml_declare_variable = ref (fun sp -> ())
-let xml_declare_constant = ref (fun sp -> ())
-let xml_declare_inductive = ref (fun sp -> ())
+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 if_xml f x = if !Options.xml_export then f x else ()
 
@@ -63,25 +59,28 @@ type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
   | SectionLocalAssum of types
 
-type variable_declaration = dir_path * section_variable_entry * local_kind
+type variable_declaration = dir_path * section_variable_entry * logical_kind
 
 type checked_section_variable =
   | CheckedSectionLocalDef of constr * types * Univ.constraints * bool
   | CheckedSectionLocalAssum of types * Univ.constraints
 
 type checked_variable_declaration = 
-    dir_path * checked_section_variable * local_kind
+    dir_path * checked_section_variable * logical_kind
 
 let vartab = ref (Idmap.empty : checked_variable_declaration 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 }
-
-let cache_variable ((sp,_),(id,(p,d,mk))) =
+  { 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 }
+
+let cache_variable ((sp,_),o) =
+  match o with
+  | Inl cst -> Global.add_constraints cst
+  | Inr (id,(p,d,mk)) ->
   (* Constr raisonne sur les noms courts *)
   if Idmap.mem id !vartab then
     errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
@@ -95,36 +94,38 @@ let cache_variable ((sp,_),(id,(p,d,mk))) =
         let (_,bd,ty) = Global.lookup_named id in
         CheckedSectionLocalDef (out_some bd,ty,cst,opaq) in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
+  add_section_variable id;
+  Dischargedhypsmap.set_discharged_hyps sp [];
   vartab := Idmap.add id (p,vd,mk) !vartab
 
+let get_variable_constraints id = 
+  match pi2 (Idmap.find id !vartab) with
+  | CheckedSectionLocalDef (c,ty,cst,opaq) -> cst
+  | CheckedSectionLocalAssum (ty,cst) -> cst
+
+let discharge_variable (_,o) = match o with
+  | Inr (id,_) -> Some (Inl (get_variable_constraints id))
+  | Inl _ -> Some o
+
 let (in_variable, out_variable) =
   declare_object { (default_object "VARIABLE") with
     cache_function = cache_variable;
+    discharge_function = discharge_variable;
     classify_function = (fun _ -> Dispose) }
 
-let declare_variable_common id obj =
-  let oname = add_leaf id (in_variable (id,obj)) in
-  declare_var_implicits id;
-  Symbols.declare_ref_arguments_scope (VarRef id);
-  oname
-
 (* for initial declaration *)
 let declare_variable id obj =
-  let (sp,kn as oname) = declare_variable_common id obj in
+  let oname = add_leaf id (in_variable (Inr (id,obj))) in
+  declare_var_implicits id;
+  Notation.declare_ref_arguments_scope (VarRef id);
   !xml_declare_variable oname;
-  Dischargedhypsmap.set_discharged_hyps sp [];
   oname
 
-(* when coming from discharge: no xml output *)
-let redeclare_variable id discharged_hyps obj =
-  let oname = declare_variable_common id obj in
-  Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps
-
 (* Globals: constants and parameters *)
 
-type constant_declaration = constant_entry * global_kind
+type constant_declaration = constant_entry * logical_kind
 
-let csttab = ref (Spmap.empty : global_kind Spmap.t)
+let csttab = ref (Spmap.empty : logical_kind Spmap.t)
 
 let _ = Summary.declare_summary "CONSTANT"
 	  { Summary.freeze_function = (fun () -> !csttab);
@@ -133,37 +134,56 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.survive_module = false;
 	    Summary.survive_section = false }
 
-let cache_constant ((sp,kn),(cdt,kind)) =
-  (if Idmap.mem (basename sp) !vartab then
-    errorlabstrm "cache_constant" 
-      (pr_id (basename sp) ++ str " already exists"));
-  (if Nametab.exists_cci sp then
-    let (_,id) = repr_path sp in
-    errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
-  let _,dir,_ = repr_kn kn in
-  let kn' = Global.add_constant dir (basename sp) cdt in
-    if kn' <> kn then
-      anomaly "Kernel and Library names do not match";
-  Nametab.push (Nametab.Until 1) sp (ConstRef kn);
-  csttab := Spmap.add sp kind !csttab
-
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
-let load_constant i ((sp,kn),(_,kind)) =
-  (if Nametab.exists_cci sp then
-    let (_,id) = repr_path sp in
-    errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
-  csttab := Spmap.add sp kind !csttab;
-  Nametab.push (Nametab.Until i) sp (ConstRef kn)
+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));
+  csttab := Spmap.add sp kind !csttab
 
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn),_) =
-  Nametab.push (Nametab.Exactly i) sp (ConstRef kn)
+  Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn))
+
+let cache_constant ((sp,kn),(cdt,dhyps,imps,kind)) =
+  let id = basename sp in
+  let _,dir,_ = repr_kn kn in
+  if Idmap.mem id !vartab then
+    errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+  if Nametab.exists_cci sp then
+    errorlabstrm "cache_constant" (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;
+  with_implicits imps declare_constant_implicits kn';
+  Notation.declare_ref_arguments_scope (ConstRef kn');
+  csttab := Spmap.add sp kind !csttab
+
+(*s Registration as global tables and rollback. *)
+
+open Cooking
+
+let discharged_hyps kn sechyps =
+  let (_,dir,_) = repr_kn kn in
+  let args = array_map_to_list destVar (instance_from_named_context sechyps) in
+  List.rev (List.map (Libnames.make_path dir) args)
+
+let discharge_constant ((sp,kn),(cdt,dhyps,imps,kind)) =
+  let con = constant_of_kn kn in
+  let cb = Global.lookup_constant con in
+  let (repl1,_ as repl) = replacement_context () in
+  let sechyps = section_segment (ConstRef con) in
+  let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in
+  Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,imps,kind)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp)
 
-let dummy_constant (ce,mk) = dummy_constant_entry,mk
+let dummy_constant (ce,_,imps,mk) = dummy_constant_entry,[],imps,mk
 
 let export_constant cst = Some (dummy_constant cst)
 
@@ -176,40 +196,43 @@ let (in_constant, out_constant) =
     open_function = open_constant;
     classify_function = classify_constant;
     subst_function = ident_subst_function;
+    discharge_function = discharge_constant;
     export_function = export_constant } 
 
 let hcons_constant_declaration = function
-  | DefinitionEntry ce ->
+  | DefinitionEntry ce when !Options.hash_cons_proofs ->
       let (hcons1_constr,_) = hcons_constr (hcons_names()) in
       DefinitionEntry
        { const_entry_body = hcons1_constr ce.const_entry_body;
 	 const_entry_type = option_app 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 discharged_hyps (cd,kind) =
-  let (sp,kn as oname) = add_leaf id (in_constant (cd,kind)) in
-  declare_constant_implicits kn;
-  Symbols.declare_ref_arguments_scope (ConstRef kn);
-  Dischargedhypsmap.set_discharged_hyps sp discharged_hyps;
-  oname
+let declare_constant_common id dhyps (cd,kind) =
+  let imps = implicits_flags () in
+  let (sp,kn) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in
+  let kn = constant_of_kn kn in
+  kn
 
 let declare_constant_gen internal id (cd,kind) =
   let cd = hcons_constant_declaration cd in
-  let oname = declare_constant_common id [] (ConstantEntry cd,kind) in
-  !xml_declare_constant (internal,oname);
-  oname
+  let kn = declare_constant_common id [] (ConstantEntry cd,kind) in
+  !xml_declare_constant (internal,kn);
+  kn
 
 let declare_internal_constant = declare_constant_gen true
 let declare_constant = declare_constant_gen false
 
-(* when coming from discharge *)
-let redeclare_constant id discharged_hyps (cd,kind) =
-  let _ = declare_constant_common id discharged_hyps (GlobalRecipe cd,kind) in
-  ()
-
 (* Inductives. *)
 
+let declare_inductive_argument_scopes kn mie =
+  list_iter_i (fun i {mind_entry_consnames=lc} ->
+    Notation.declare_ref_arguments_scope (IndRef (kn,i));
+    for j=1 to List.length lc do
+      Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j));
+    done) mie.mind_entry_inds
+
 let inductive_names sp kn mie =
   let (dp,_) = repr_path sp in
   let names, _ = 
@@ -230,39 +253,44 @@ let inductive_names sp kn mie =
       ([], 0) mie.mind_entry_inds
   in names
 
-
 let check_exists_inductive (sp,_) =
   (if Idmap.mem (basename sp) !vartab then
-    errorlabstrm "cache_inductive" 
+    errorlabstrm ""
       (pr_id (basename sp) ++ str " already exists"));
   if Nametab.exists_cci sp then
     let (_,id) = repr_path sp in
-    errorlabstrm "cache_inductive" (pr_id id ++ str " already exists")
+    errorlabstrm "" (pr_id id ++ str " already exists")
 
-let cache_inductive ((sp,kn),mie) =
-  let names = inductive_names sp kn mie in
-  List.iter check_exists_inductive names;
-  let _,dir,_ = repr_kn kn in
-  let kn' = Global.add_mind dir (basename sp) mie in
-    if kn' <> kn then
-      anomaly "Kernel and Library names do not match";
-
-  List.iter 
-    (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref)
-    names
-
-let load_inductive i ((sp,kn),mie) =
+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
 
-let open_inductive i ((sp,kn),mie) =
+let open_inductive i ((sp,kn),(_,_,mie)) =
   let names = inductive_names sp kn mie in
-(*  List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names*)
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
 
+let cache_inductive ((sp,kn),(dhyps,imps,mie)) =
+  let names = inductive_names sp kn mie in
+  List.iter check_exists_inductive names;
+  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;
+  Dischargedhypsmap.set_discharged_hyps sp dhyps;
+  with_implicits imps declare_mib_implicits kn;
+  declare_inductive_argument_scopes kn mie;
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
+
+let discharge_inductive ((sp,kn),(dhyps,imps,mie)) =
+  let mie = Global.lookup_mind kn in
+  let repl = replacement_context () in
+  let sechyps = section_segment (IndRef (kn,0)) in
+  Some (discharged_hyps kn sechyps,imps,
+        Discharge.process_inductive sechyps repl mie)
+
 let dummy_one_inductive_entry mie = {
-  mind_entry_params = [];
   mind_entry_typename = mie.mind_entry_typename;
   mind_entry_arity = mkProp;
   mind_entry_consnames = mie.mind_entry_consnames;
@@ -270,10 +298,11 @@ let dummy_one_inductive_entry mie = {
 }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_inductive_entry m = {
+let dummy_inductive_entry (_,imps,m) = ([],imps,{
+  mind_entry_params = [];
   mind_entry_record = false;
   mind_entry_finite = true;
-  mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }
+  mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
 
 let export_inductive x = Some (dummy_inductive_entry x)
 
@@ -284,38 +313,19 @@ let (in_inductive, out_inductive) =
     open_function = open_inductive;
     classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a));
     subst_function = ident_subst_function;
+    discharge_function = discharge_inductive;
     export_function = export_inductive } 
 
-let declare_inductive_argument_scopes kn mie =
-  list_iter_i (fun i {mind_entry_consnames=lc} ->
-    Symbols.declare_ref_arguments_scope (IndRef (kn,i));
-    for j=1 to List.length lc do
-      Symbols.declare_ref_arguments_scope (ConstructRef ((kn,i),j));
-    done) mie.mind_entry_inds
-
-let declare_inductive_common mie =
-  let id = match mie.mind_entry_inds with
-    | ind::_ -> ind.mind_entry_typename
-    | [] -> anomaly "cannot declare an empty list of inductives"
-  in
-  let oname = add_leaf id (in_inductive mie) in
-  declare_mib_implicits (snd oname);
-  declare_inductive_argument_scopes (snd oname) mie;
-  oname
-
 (* for initial declaration *)
 let declare_mind isrecord mie =
-  let (sp,kn as oname) = declare_inductive_common mie in
-  Dischargedhypsmap.set_discharged_hyps sp [] ;
+  let imps = implicits_flags () in
+  let id = match mie.mind_entry_inds with
+    | ind::_ -> ind.mind_entry_typename
+    | [] -> anomaly "cannot declare an empty list of inductives" in
+  let oname = add_leaf id (in_inductive ([],imps,mie)) in
   !xml_declare_inductive (isrecord,oname);
   oname
 
-(* when coming from discharge: no xml output *)
-let redeclare_inductive discharged_hyps mie =
- let oname = declare_inductive_common mie in
- Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps ;
- oname
-
 (*s Test and access functions. *)
 
 let is_constant sp = 
@@ -330,12 +340,6 @@ let get_variable id =
     | CheckedSectionLocalDef (c,ty,cst,opaq) -> (id,Some c,ty)
     | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty)
 
-let get_variable_with_constraints id = 
-  let (p,x,_) = Idmap.find id !vartab in
-  match x with
-    | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst)
-    | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst)
-
 let variable_strength _ = Local
 
 let find_section_variable id =
@@ -351,8 +355,10 @@ let variable_kind id =
   pi3 (Idmap.find id !vartab)
 
 let clear_proofs sign =
-  List.map
-    (fun (id,c,t as d) -> if variable_opacity id then (id,None,t) else d) sign
+  List.fold_right
+    (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
 
 (* Global references. *)
 
@@ -378,12 +384,6 @@ let mind_oper_of_id sp id mib =
 	   mip.mind_consnames)
     mib.mind_packets
 
-let context_of_global_reference = function
-  | VarRef id -> []
-  | ConstRef sp -> (Global.lookup_constant sp).const_hyps
-  | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps
-  | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps
-
 let last_section_hyps dir =
   fold_named_context
     (fun (id,_,_) sec_ids ->
diff --git a/library/declare.mli b/library/declare.mli
index 968be059..938bfd06 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,v 1.74.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: declare.mli 7941 2006-01-28 23:07:59Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -36,42 +36,29 @@ type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
   | SectionLocalAssum of types
 
-type variable_declaration = dir_path * section_variable_entry * local_kind
+type variable_declaration = dir_path * section_variable_entry * logical_kind
 
 val declare_variable : variable -> variable_declaration -> object_name
 
-(* Declaration from Discharge *)
-val redeclare_variable :
- variable -> Dischargedhypsmap.discharged_hyps -> variable_declaration -> unit
-
 (* Declaration of global constructions *)
 (* i.e. Definition/Theorem/Axiom/Parameter/... *)
 
-type constant_declaration = constant_entry * global_kind
+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 *)
-val declare_constant : identifier -> constant_declaration -> object_name
+val declare_constant :
+ identifier -> constant_declaration -> constant
 
 val declare_internal_constant :
-  identifier -> constant_declaration -> object_name
-
-val redeclare_constant :
- identifier -> Dischargedhypsmap.discharged_hyps -> 
-      Cooking.recipe * global_kind -> unit
+  identifier -> constant_declaration -> 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
 
-(* Declaration from Discharge *)
-val redeclare_inductive :
- Dischargedhypsmap.discharged_hyps -> mutual_inductive_entry -> object_name
-
-val out_inductive : Libobject.obj -> mutual_inductive_entry 
-
 val strength_min : strength * strength -> strength
 val string_of_strength : strength -> string
 
@@ -79,24 +66,20 @@ val string_of_strength : strength -> string
 
 val is_constant : section_path -> bool
 val constant_strength : section_path -> strength
-val constant_kind : section_path -> global_kind
+val constant_kind : section_path -> logical_kind
 
-val out_variable : Libobject.obj -> identifier * variable_declaration
 val get_variable : variable -> named_declaration
-val get_variable_with_constraints : 
-  variable -> named_declaration * Univ.constraints
 val variable_strength : variable -> strength 
-val variable_kind : variable -> local_kind
+val variable_kind : variable -> logical_kind
 val find_section_variable : variable -> section_path
 val last_section_hyps : dir_path -> identifier list
-val clear_proofs : named_context -> named_context
+val clear_proofs : named_context -> Environ.named_context_val
 
 (*s Global references *)
 
-val context_of_global_reference : global_reference -> section_context
 val strength_of_global : global_reference -> strength
 
 (* hooks for XML output *)
 val set_xml_declare_variable : (object_name -> unit) -> unit
-val set_xml_declare_constant : (bool * object_name -> unit) -> unit
+val set_xml_declare_constant : (bool * constant -> unit) -> unit
 val set_xml_declare_inductive : (bool * object_name -> unit) -> unit
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 2e8fb0a7..3b2196a5 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.ml,v 1.18.2.2 2005/12/30 11:08:56 herbelin Exp $ i*)
+(*i $Id: declaremods.ml 7720 2005-12-24 00:25:55Z herbelin $ i*)
 
 open Pp
 open Util
@@ -17,6 +17,7 @@ open Libnames
 open Libobject
 open Lib
 open Nametab
+open Mod_subst
 
 (* modules and components *)
 
@@ -372,19 +373,25 @@ let (in_modtype,out_modtype) =
 
 
 
-let replace_module_object id (subst, mbids, msid, lib_stack) modobjs =
+let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs =
   if mbids<>[] then 
     error "Unexpected functor objects"
   else
-    let rec replace_id = function 
-      | [] -> [] 
-      | (id',obj)::tail when id = id' ->
+    let rec replace_idl = function 
+      | _,[] -> [] 
+      | id::idl,(id',obj)::tail when id = id' ->
 	  if object_tag obj = "MODULE" then
-	    (id, in_module (None,modobjs,None))::tail
+           (match idl with
+               [] -> (id, in_module (None,modobjs,None))::tail
+             | _ ->
+               let (_,substobjs,_) = out_module obj in
+                let substobjs' = replace_module_object idl substobjs modobjs in
+                 (id, in_module (None,substobjs',None))::tail
+           )
 	  else error "MODULE expected!"
-      | lobj::tail -> lobj::replace_id tail
+      | idl,lobj::tail -> lobj::replace_idl (idl,tail)
     in
-      (subst, mbids, msid, replace_id lib_stack)
+      (subst, mbids, msid, replace_idl (idl,lib_stack))
 
 let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) =
   (subst, mbids1@mbids2, msid, lib_stack)
@@ -396,10 +403,10 @@ let rec get_modtype_substobjs = function
       let (subst, mbids, msid, objs) = get_modtype_substobjs mte in
 	(subst, mbid::mbids, msid, objs)
   | MTEwith (mty, With_Definition _) -> get_modtype_substobjs mty
-  | MTEwith (mty, With_Module (id,mp)) -> 
+  | MTEwith (mty, With_Module (idl,mp)) -> 
       let substobjs = get_modtype_substobjs mty in
       let modobjs = MPmap.find mp !modtab_substobjs in
-	replace_module_object id substobjs modobjs
+	replace_module_object idl substobjs modobjs
   | MTEsig (msid,_) -> 
       todo "Anonymous module types"; (empty_subst, [], msid, [])
 
@@ -449,7 +456,7 @@ let intern_args interp_modtype (env,oldargs) (idl,arg) =
     in
     env, List.map (fun mbid -> mbid,mty) mbids :: oldargs
       
-let start_module interp_modtype id args res_o =
+let start_module interp_modtype export id args res_o =
   let fs = Summary.freeze_summaries () in
   let env = Global.env () in
   let env,arg_entries_revlist = 
@@ -481,7 +488,7 @@ let start_module interp_modtype id args res_o =
 
   let mbids = List.map fst arg_entries in
   openmod_info:=(mbids,res_entry_o,sub_body_o);
-  let prefix = Lib.start_module id mp fs in
+  let prefix = Lib.start_module export id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
   Lib.add_frozen_state ()
 
@@ -565,7 +572,6 @@ let library_cache = Hashtbl.create 17
 
 let register_library dir cenv objs digest =
   let mp = MPfile dir in
-  let prefix = dir, (mp, empty_dirpath) in
   let substobjs, objects =
     try 
       ignore(Global.lookup_module mp);
@@ -697,21 +703,25 @@ let declare_modtype interp_modtype id args mty =
   ignore (add_leaf id (in_modtype (Some entry, substobjs)))
 			       
 
-
-let rec get_module_substobjs = function
+let rec get_module_substobjs env = function
   | MEident mp -> MPmap.find mp !modtab_substobjs 
   | MEfunctor (mbid,mty,mexpr) ->
-      let (subst, mbids, msid, objs) = 
-	get_module_substobjs mexpr 
-      in
+       let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
 	(subst, mbid::mbids, msid, objs)
   | MEstruct (msid,_) ->
       (empty_subst, [], msid, [])
   | MEapply (mexpr, MEident mp) ->
-      let (subst, mbids, msid, objs) = get_module_substobjs mexpr in
+      let feb,ftb = Mod_typing.translate_mexpr env mexpr in
+      let ftb = Modops.scrape_modtype env ftb in
+      let farg_id, farg_b, fbody_b = Modops.destr_functor ftb in
+      let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
 	(match mbids with
 	   | mbid::mbids ->
-	       (add_mbid mbid mp subst, mbids, msid, objs)
+              let resolve =
+               Modops.resolver_of_environment farg_id farg_b mp env in
+               (* application outside the kernel, only for substitutive
+                  objects (that are all non-logical objects) *)
+	       (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs)
 	   | [] -> match mexpr with
 	       | MEident _ | MEstruct _ -> error "Application of a non-functor"
 	       | _ -> error "Application of a functor with too few arguments")
@@ -757,7 +767,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
   let substobjs =
     match entry with
       | {mod_entry_type = Some mte} -> get_modtype_substobjs mte
-      | {mod_entry_expr = Some mexpr} -> get_module_substobjs mexpr
+      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr
       | _ -> anomaly "declare_module: No type, no body ..."
   in
     Summary.unfreeze_summaries fs;
@@ -772,23 +782,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
 
 (*s Iterators. *)
 
-let fold_all_segments insec f x =
-  let acc' = 
-    MPmap.fold 
-      (fun _ (prefix,objects) acc -> 
-	 let apply_obj acc (id,obj) = f acc (make_oname prefix id) obj in
-	   List.fold_left apply_obj acc objects)
-      !modtab_objects x
-  in
-  let rec apply_node acc = function
-    | sp, Leaf o -> f acc sp o
-    | _, ClosedSection (_,_,seg) -> 
-	if insec then List.fold_left apply_node acc seg else acc
-    | _ -> acc
-  in
-    List.fold_left apply_node acc' (Lib.contents_after None)
-
-let iter_all_segments insec f =
+let iter_all_segments f =
   let _ = 
     MPmap.iter 
       (fun _ (prefix,objects) -> 
@@ -798,13 +792,11 @@ let iter_all_segments insec f =
   in
   let rec apply_node = function
     | sp, Leaf o -> f sp o
-    | _, ClosedSection (_,_,seg) -> if insec then List.iter apply_node seg
     | _ -> ()
   in
     List.iter apply_node (Lib.contents_after None)
 
 
-
 let debug_print_modtab _ =
   let pr_seg = function
     | [] -> str "[]"
@@ -816,5 +808,3 @@ let debug_print_modtab _ =
   in
   let modules = MPmap.fold pr_modinfo !modtab_objects (mt ()) in
     hov 0 modules
-
-
diff --git a/library/declaremods.mli b/library/declaremods.mli
index f896310a..481809fc 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,v 1.8.2.2 2005/01/21 16:41:50 herbelin Exp $ i*)
+(*i $Id: declaremods.mli 6758 2005-02-20 18:13:28Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -43,9 +43,8 @@ val declare_module :
   'modexpr option -> unit
  
 val start_module : (env -> 'modtype -> module_type_entry) -> 
-  identifier -> 
-  (identifier located list * 'modtype) list -> ('modtype * bool) option -> 
-  unit
+  bool option -> identifier -> (identifier located list * 'modtype) list ->
+   ('modtype * bool) option -> unit
 
 val end_module : identifier -> unit
 
@@ -97,14 +96,12 @@ val really_import_module : module_path -> unit
 val import_module : bool -> module_path -> unit
 
 
-(*s [fold_all_segments] and [iter_all_segments] iterate over all
-    segments, the modules' segments first and then the current
-    segment. Modules are presented in an arbitrary order. The given
-    function is applied to all leaves (together with their section
-    path). The boolean indicates if we must enter closed sections. *)
+(*s [iter_all_segments] iterate over all segments, the modules'
+    segments first and then the current segment. Modules are presented
+    in an arbitrary order. The given function is applied to all leaves
+    (together with their section path). *)
 
-val fold_all_segments : bool -> ('a -> object_name -> obj -> 'a) -> 'a -> 'a
-val iter_all_segments : bool -> (object_name -> obj -> unit) -> unit
+val iter_all_segments : (object_name -> obj -> unit) -> unit
 
 
 val debug_print_modtab : unit -> Pp.std_ppcmds
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index 59a01d81..2a3abda8 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dischargedhypsmap.ml,v 1.3.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+(* $Id: dischargedhypsmap.ml 6748 2005-02-18 22:17:50Z herbelin $ *)
 
 open Util
 open Libnames
@@ -24,13 +24,16 @@ type discharged_hyps = section_path list
 
 let discharged_hyps_map = ref Spmap.empty
 
-let cache_discharged_hyps_map (_,(sp,hyps)) = 
+let load_discharged_hyps_map _ (_,(sp,hyps)) = 
   discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
 
+let cache_discharged_hyps_map o =
+  load_discharged_hyps_map 1 o
+
 let (in_discharged_hyps_map, _) =
   declare_object { (default_object "DISCHARGED-HYPS-MAP") with
     cache_function = cache_discharged_hyps_map;
-    load_function = (fun _ -> cache_discharged_hyps_map);
+    load_function = load_discharged_hyps_map;
     export_function = (fun x -> Some x) }
 
 let set_discharged_hyps sp hyps =
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
index 8851e5a3..9a3259ce 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,v 1.2.8.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: dischargedhypsmap.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (*i*)
 open Libnames
diff --git a/library/global.ml b/library/global.ml
index 8694d7af..b4d3a7ff 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: global.ml,v 1.43.2.2 2005/11/23 14:46:17 barras Exp $ *)
+(* $Id: global.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
 
 open Util
 open Names
@@ -39,6 +39,7 @@ let _ =
 
 let universes () = universes (env())
 let named_context () = named_context (env())
+let named_context_val () = named_context_val (env())
 
 let push_named_assum a =
   let (cst,env) = push_named_assum a !global_env in
@@ -134,14 +135,14 @@ let env_of_context hyps =
 open Libnames
 
 let type_of_reference env = function
-  | VarRef id -> let (_,_,t) = Environ.lookup_named id env in t
+  | VarRef id -> Environ.named_type id env 
   | ConstRef c -> Environ.constant_type env c
-  | IndRef ind -> Inductive.type_of_inductive env ind
-  | ConstructRef cstr -> Inductive.type_of_constructor env cstr
+  | IndRef ind ->
+     let specif = Inductive.lookup_mind_specif env ind in
+      Inductive.type_of_inductive specif
+  | ConstructRef cstr ->
+     let specif =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+       Inductive.type_of_constructor cstr specif
 
 let type_of_global t = type_of_reference (env ()) t
-
-
-(*let get_kn dp l = 
-  make_kn (current_modpath !global_env) dp l
-*)
diff --git a/library/global.mli b/library/global.mli
index 007986d1..278b9e65 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,v 1.40.2.2 2005/11/23 14:46:17 barras Exp $ i*)
+(*i $Id: global.mli 7899 2006-01-20 16:35:03Z barras $ i*)
 
 (*i*)
 open Names
@@ -29,7 +29,10 @@ open Safe_typing
 val safe_env : unit -> safe_environment
 val env : unit -> Environ.env
 
+val env_is_empty : unit -> bool
+
 val universes : unit -> universes
+val named_context_val : unit -> Environ.named_context_val
 val named_context : unit -> Sign.named_context
 
 val env_is_empty : unit -> bool
@@ -42,7 +45,7 @@ val push_named_def   : (identifier * constr * types option) -> Univ.constraints
   functions verify that given names match those generated by kernel *)
 
 val add_constant : 
-  dir_path -> identifier -> global_declaration -> kernel_name
+  dir_path -> identifier -> global_declaration -> constant
 val add_mind        : 
   dir_path -> identifier -> mutual_inductive_entry -> kernel_name
 
@@ -51,7 +54,7 @@ val add_modtype     : identifier -> module_type_entry -> kernel_name
 
 val add_constraints : constraints -> unit
 
-val set_engagement : Environ.engagement -> unit
+val set_engagement : engagement -> unit
 
 (*s Interactive modules and module types *)
 (* Both [start_*] functions take the [dir_path] argument to create a 
@@ -93,5 +96,5 @@ val import : compiled_library -> Digest.t -> module_path
  * environment and a given context. *)
   
 val type_of_global : Libnames.global_reference -> types
-val env_of_context : Sign.named_context -> Environ.env
+val env_of_context : Environ.named_context_val -> Environ.env
 
diff --git a/library/goptions.ml b/library/goptions.ml
index bcb4fb79..c220544c 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: goptions.ml,v 1.22.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+(* $Id: goptions.ml 6304 2004-11-16 15:49:08Z sacerdot $ *)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -17,6 +17,7 @@ open Names
 open Libnames
 open Term
 open Nametab
+open Mod_subst
 
 (****************************************************************************)
 (* 0- Common things                                                         *)
diff --git a/library/goptions.mli b/library/goptions.mli
index bbf5357a..16744ec4 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,v 1.10.6.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: goptions.mli 6304 2004-11-16 15:49:08Z sacerdot $ i*)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -59,6 +59,7 @@ open Names
 open Libnames
 open Term
 open Nametab
+open Mod_subst
 (*i*)
 
 (*s Things common to tables and options. *)
diff --git a/library/impargs.ml b/library/impargs.ml
index 8a9429a4..08ae2aa5 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: impargs.ml,v 1.59.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+(* $Id: impargs.ml 8672 2006-03-29 21:06:33Z herbelin $ *)
 
 open Util
 open Names
@@ -27,63 +27,44 @@ open Topconstr
 
 (* les implicites sont stricts par défaut en v8 *)
 let implicit_args = ref false
-let strict_implicit_args = ref (not !Options.v7)
+let strict_implicit_args = ref true
 let contextual_implicit_args = ref false
 
-let implicit_args_out = ref false
-let strict_implicit_args_out = ref true
-let contextual_implicit_args_out = ref false
-
 let make_implicit_args flag =
-  implicit_args := flag;
-  if not !Options.v7_only then implicit_args_out := flag;
-  if !Options.translate_strict_impargs then
-    strict_implicit_args_out := not flag
+  implicit_args := flag
 
 let make_strict_implicit_args flag =
-  strict_implicit_args := flag;
-  if not !Options.v7_only then strict_implicit_args_out := flag
+  strict_implicit_args := flag
 
 let make_contextual_implicit_args flag =
-  contextual_implicit_args := flag;
-  if not !Options.v7_only then contextual_implicit_args_out := flag
+  contextual_implicit_args := flag
 
 let is_implicit_args () = !implicit_args
-let is_implicit_args_out () = !implicit_args_out
 let is_strict_implicit_args () = !strict_implicit_args
 let is_contextual_implicit_args () = !contextual_implicit_args
 
-type implicits_flags = (bool * bool * bool) * (bool * bool * bool)
+type implicits_flags = bool * bool * bool
+
+let implicits_flags () = 
+  (!implicit_args, !strict_implicit_args, !contextual_implicit_args)
 
-let with_implicits ((a,b,c),(d,e,g)) f x =
+let with_implicits (a,b,c) f x =
   let oa = !implicit_args in
   let ob = !strict_implicit_args in
   let oc = !contextual_implicit_args in
-  let od = !implicit_args_out in
-  let oe = !strict_implicit_args_out in
-  let og = !contextual_implicit_args_out in
   try 
     implicit_args := a;
     strict_implicit_args := b;
     contextual_implicit_args := c;
-    implicit_args_out := d;
-    strict_implicit_args_out := e;
-    contextual_implicit_args_out := g;
     let rslt = f x in 
     implicit_args := oa;
     strict_implicit_args := ob;
     contextual_implicit_args := oc;
-    implicit_args_out := od;
-    strict_implicit_args_out := oe;
-    contextual_implicit_args_out := og;
     rslt
   with e -> begin
     implicit_args := oa;
     strict_implicit_args := ob;
     contextual_implicit_args := oc;
-    implicit_args_out := od;
-    strict_implicit_args_out := oe;
-    contextual_implicit_args_out := og;
     raise e
   end
 
@@ -135,7 +116,7 @@ let update pos rig (na,st) =
       | Some (DepFlexAndRigid (fpos,rpos) as x) ->
           if argument_less (pos,fpos) or pos=fpos then DepRigid pos else
           if argument_less (pos,rpos) then DepFlexAndRigid (fpos,pos) else x
-      | Some (DepFlex fpos as x) ->
+      | Some (DepFlex fpos) ->
           if argument_less (pos,fpos) or pos=fpos then DepRigid pos
           else DepFlexAndRigid (fpos,pos)
       | Some Manual -> assert false
@@ -213,13 +194,9 @@ let compute_implicits_gen strict contextual env t =
 	Array.to_list v
     | _ -> []
 
-let compute_implicits output env t =
-  let strict =
-    (not output & !strict_implicit_args) or
-    (output & !strict_implicit_args_out) in 
-  let contextual =
-    (not output & !contextual_implicit_args) or
-    (output & !contextual_implicit_args_out) in
+let compute_implicits env t =
+  let strict = !strict_implicit_args in
+  let contextual = !contextual_implicit_args in
   let l = compute_implicits_gen strict contextual env t in
   List.map (function
     | (Name id, Some imp) -> Some (id,imp)
@@ -267,20 +244,11 @@ type implicits =
   | No_impl
 
 let auto_implicits env ty =
-  let impl = 
-    if !implicit_args then
-      let l = compute_implicits false env ty in
-      Impl_auto (!strict_implicit_args,!contextual_implicit_args,l)
-    else
-      No_impl in
-  if Options.do_translate () then
-    impl, 
-    if !implicit_args_out then 
-      (let l = compute_implicits true env ty in
-      Impl_auto (!strict_implicit_args_out,!contextual_implicit_args_out,l))
-    else No_impl
-  else 
-    impl, impl
+  if !implicit_args then
+    let l = compute_implicits env ty in
+    Impl_auto (!strict_implicit_args,!contextual_implicit_args,l)
+  else
+    No_impl
 
 let list_of_implicits = function 
   | Impl_auto (_,_,l) -> l
@@ -289,7 +257,7 @@ let list_of_implicits = function
 
 (*s Constants. *)
 
-let constants_table = ref KNmap.empty
+let constants_table = ref Cmap.empty
 
 let compute_constant_implicits kn =
   let env = Global.env () in
@@ -297,7 +265,7 @@ let compute_constant_implicits kn =
   auto_implicits env (body_of_type cb.const_type)
 
 let constant_implicits sp =
-  try KNmap.find sp !constants_table with Not_found -> No_impl,No_impl
+  try Cmap.find sp !constants_table with Not_found -> No_impl
 
 (*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
@@ -326,10 +294,11 @@ let compute_mib_implicits kn =
   Array.mapi imps_one_inductive mib.mind_packets
 
 let inductive_implicits indp =
-  try Indmap.find indp !inductives_table with Not_found -> No_impl,No_impl
+  try Indmap.find indp !inductives_table with Not_found -> No_impl
 
 let constructor_implicits consp =
-  try Constrmap.find consp !constructors_table with Not_found -> No_impl,No_impl
+  try Constrmap.find consp !constructors_table with Not_found -> No_impl
+
 (*s Variables. *)
 
 let var_table = ref Idmap.empty
@@ -340,7 +309,17 @@ let compute_var_implicits id =
   auto_implicits env ty
 
 let var_implicits id = 
-  try Idmap.find id !var_table with Not_found -> No_impl,No_impl
+  try Idmap.find id !var_table with Not_found -> No_impl
+
+(* Implicits of a global reference. *)
+
+let compute_global_implicits = function
+  | VarRef id -> compute_var_implicits id
+  | ConstRef kn -> compute_constant_implicits kn
+  | IndRef (kn,i) -> 
+      let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps
+  | ConstructRef ((kn,i),j) -> 
+      let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1)
 
 (* Caching implicits *)
 
@@ -349,16 +328,19 @@ let cache_implicits_decl (r,imps) =
   | VarRef id -> 
       var_table := Idmap.add id imps !var_table
   | ConstRef kn ->
-      constants_table := KNmap.add kn imps !constants_table
+      constants_table := Cmap.add kn imps !constants_table
   | IndRef indp ->
       inductives_table := Indmap.add indp imps !inductives_table;
   | ConstructRef consp -> 
       constructors_table := Constrmap.add consp imps !constructors_table
 
-let cache_implicits (_,l) = List.iter cache_implicits_decl l
+let load_implicits _ (_,l) = List.iter cache_implicits_decl l
+
+let cache_implicits o =
+  load_implicits 1 o
 
 let subst_implicits_decl subst (r,imps as o) =
-  let r' = subst_global subst r in if r==r' then o else (r',imps)
+  let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
 
 let subst_implicits (_,subst,l) =
   list_smartmap (subst_implicits_decl subst) l
@@ -366,40 +348,27 @@ let subst_implicits (_,subst,l) =
 let (in_implicits, _) =
   declare_object {(default_object "IMPLICITS") with 
     cache_function = cache_implicits;
-    load_function = (fun _ -> cache_implicits);
+    load_function = load_implicits;
     subst_function = subst_implicits;
     classify_function = (fun (_,x) -> Substitute x);
     export_function = (fun x -> Some x) }
 
-(* Implicits of a global reference. *)
-
-let compute_global_implicits = function
-  | VarRef id -> compute_var_implicits id
-  | ConstRef kn -> compute_constant_implicits kn
-  | IndRef (kn,i) -> 
-      let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps
-  | ConstructRef ((kn,i),j) -> 
-      let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1)
-
 let declare_implicits_gen r = 
   add_anonymous_leaf (in_implicits [r,compute_global_implicits r])
 
 let declare_implicits r =
   with_implicits
-    ((true,!strict_implicit_args,!contextual_implicit_args),
-     (true,!strict_implicit_args_out,!contextual_implicit_args_out))
+    (true,!strict_implicit_args,!contextual_implicit_args)
     declare_implicits_gen r
 
 let declare_var_implicits id =
-  if !implicit_args or !implicit_args_out then
-    declare_implicits_gen (VarRef id)
+  if !implicit_args then declare_implicits_gen (VarRef id)
 
 let declare_constant_implicits kn =
-  if !implicit_args or !implicit_args_out then
-    declare_implicits_gen (ConstRef kn)
+  if !implicit_args then declare_implicits_gen (ConstRef kn)
 
 let declare_mib_implicits kn =
-  if !implicit_args or !implicit_args_out then
+  if !implicit_args then
   let imps = compute_mib_implicits kn in
   let imps = array_map_to_list
     (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) imps in
@@ -412,28 +381,10 @@ let implicits_of_global_gen = function
   | ConstructRef csp ->	constructor_implicits csp
 
 let implicits_of_global r =
-  let (imp_in,imp_out) = implicits_of_global_gen r in
-  list_of_implicits imp_in
-
-let implicits_of_global_out r =
-  let (imp_in,imp_out) = implicits_of_global_gen r in
-  list_of_implicits imp_out
+  list_of_implicits (implicits_of_global_gen r)
 
 (* Declare manual implicits *)
 
-(*
-let check_range n = function
-  | loc,ExplByPos i ->
-      if i<1 or i>n then error ("Bad argument number: "^(string_of_int i))
-  | loc,ExplByName id ->
-()
-*)
-
-let rec list_remove a = function
-  | b::l when a = b -> l
-  | b::l -> b::list_remove a l
-  | [] -> raise Not_found
-
 let set_implicit id imp =
   Some (id,match imp with None -> Manual | Some imp -> imp)
 
@@ -443,15 +394,13 @@ let declare_manual_implicits r l =
   let n = List.length autoimps in
   if not (list_distinct l) then 
     error ("Some parameters are referred more than once");
-(*  List.iter (check_range n) l;*)
-(*  let l = List.sort (-) l in*)
   (* Compare with automatic implicits to recover printing data and names *)
   let rec merge k l = function
     | (Name id,imp)::imps ->
 	let l',imp =
-	  try list_remove (ExplByPos k) l, set_implicit id imp
+	  try list_remove_first (ExplByPos k) l, set_implicit id imp
 	  with Not_found ->
-	  try list_remove (ExplByName id) l, set_implicit id imp
+	  try list_remove_first (ExplByName id) l, set_implicit id imp
 	  with Not_found ->
 	  l, None in
 	imp :: merge (k+1) l' imps
@@ -470,8 +419,6 @@ let declare_manual_implicits r l =
 		(str "Cannot set implicit argument number " ++ int i ++
 		 str ": it has no name") in
   let l = Impl_manual (merge 1 l autoimps) in
-  let (_,oimp_out) = implicits_of_global_gen r in
-  let l = l, if !Options.v7_only then oimp_out else l in
   add_anonymous_leaf (in_implicits [r,l])
 
 (* Tests if declared implicit *)
@@ -481,11 +428,11 @@ let test = function
   | Impl_auto (s,c,_) -> true,s,c
 
 let test_if_implicit find a =
-  try let b,c = find a in test b, test c
-  with Not_found -> (false,false,false),(false,false,false)
+  try let b = find a in test b
+  with Not_found -> (false,false,false)
     
 let is_implicit_constant sp =
-  test_if_implicit (KNmap.find sp) !constants_table
+  test_if_implicit (Cmap.find sp) !constants_table
 
 let is_implicit_inductive_definition indp =
   test_if_implicit (Indmap.find (indp,0)) !inductives_table
@@ -496,7 +443,7 @@ let is_implicit_var id =
 (*s Registration as global tables *)
 
 let init () =
-  constants_table := KNmap.empty;
+  constants_table := Cmap.empty;
   inductives_table := Indmap.empty;
   constructors_table := Constrmap.empty;
   var_table := Idmap.empty
@@ -518,34 +465,3 @@ let _ =
       Summary.init_function = init;
       Summary.survive_module = false;
       Summary.survive_section = false }
-
-(* Remark: flags implicit_args, contextual_implicit_args
-   are synchronized by the general options mechanism - see Vernacentries *)
-
-let init () =
-  (* strict_implicit_args_out must be not !Options.v7 
-     but init is done before parsing *)
-  strict_implicit_args:=not !Options.v7;
-  implicit_args_out:=false;
-  (* strict_implicit_args_out needs to be not !Options.v7 or
-     Options.do_translate() but init is done before parsing *)
-  strict_implicit_args_out:=true;
-  contextual_implicit_args_out:=false
-
-let freeze () =
-  (!strict_implicit_args,
-   !implicit_args_out,!strict_implicit_args_out,!contextual_implicit_args_out)
-
-let unfreeze (b,d,e,f) =
-  strict_implicit_args := b;
-  implicit_args_out := d;
-  strict_implicit_args_out := e;
-  contextual_implicit_args_out := f
-
-let _ = 
-  Summary.declare_summary "implicits-out-options"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_module = false;
-      Summary.survive_section = true }
diff --git a/library/impargs.mli b/library/impargs.mli
index 8db04ee7..671d195c 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,v 1.26.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: impargs.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -43,7 +43,7 @@ val positions_of_implicits : implicits_list -> int list
 
 (* Computation of the positions of arguments automatically inferable
    for an object of the given type in the given env *)
-val compute_implicits : bool -> env -> types -> implicits_list
+val compute_implicits : env -> types -> implicits_list
 
 (*s Computation of implicits (done using the global environment). *)
 
@@ -64,6 +64,4 @@ val is_implicit_var : variable -> implicits_flags
 
 val implicits_of_global : global_reference -> implicits_list
 
-(* For translator *)
-val implicits_of_global_out : global_reference -> implicits_list
-val is_implicit_args_out : unit -> bool
+val implicits_flags : unit -> implicits_flags
diff --git a/library/lib.ml b/library/lib.ml
index c46634f4..ee553cad 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: lib.ml,v 1.63.2.4 2005/11/04 09:02:38 herbelin Exp $ *)
+(* $Id: lib.ml 7710 2005-12-23 10:16:42Z herbelin $ *)
 
 open Pp
 open Util
@@ -21,11 +21,10 @@ open Summary
 type node = 
   | Leaf of obj
   | CompilingLibrary of object_prefix
-  | OpenedModule of object_prefix * Summary.frozen
+  | OpenedModule of bool option * object_prefix * Summary.frozen
   | OpenedModtype of object_prefix * Summary.frozen
   | OpenedSection of object_prefix * Summary.frozen
-  (* bool is to tell if the section must be opened automatically *)
-  | ClosedSection of bool * dir_path * library_segment
+  | ClosedSection
   | FrozenState of Summary.frozen
 
 and library_entry = object_name * node
@@ -51,7 +50,7 @@ let subst_objects prefix subst seg =
 let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
-    | ((sp,kn as oname),Leaf o) as node :: stk -> 
+    | ((sp,kn as oname),Leaf o) :: stk -> 
 	let id = id_of_label (label kn) in
 	  (match classify_object (oname,o) with 
 	     | Dispose -> clean acc stk
@@ -61,7 +60,7 @@ let classify_segment seg =
 		 clean ((id,o')::substl, keepl, anticipl) stk
 	     | Anticipate o' ->
 		 clean (substl, keepl, o'::anticipl) stk)
-    | (oname,ClosedSection _ as item) :: stk -> clean acc stk
+    | (oname,ClosedSection) :: stk -> clean acc stk
     | (_,OpenedSection _) :: _ -> error "there are still opened sections"
     | (_,OpenedModule _) :: _ -> error "there are still opened modules"
     | (_,OpenedModtype _) :: _ -> error "there are still opened module types"
@@ -105,6 +104,10 @@ let make_kn id =
   let mp,dir = current_prefix () in
     Names.make_kn mp dir (label_of_id id)
 
+let make_con id = 
+  let mp,dir = current_prefix () in
+    Names.make_con mp dir (label_of_id id)
+
 
 let make_oname id = make_path id, make_kn id
 
@@ -121,7 +124,7 @@ let sections_are_opened () =
 let recalc_path_prefix () =
   let rec recalc = function
     | (sp, OpenedSection (dir,_)) :: _ -> dir
-    | (sp, OpenedModule (dir,_)) :: _ -> dir
+    | (sp, OpenedModule (_,dir,_)) :: _ -> dir
     | (sp, OpenedModtype (dir,_)) :: _ -> dir
     | (sp, CompilingLibrary dir) :: _ -> dir
     | _::l -> recalc l
@@ -180,6 +183,8 @@ let add_absolutely_named_leaf sp obj =
   add_entry sp (Leaf obj)
 
 let add_leaf id obj =
+  if fst (current_prefix ()) = initial_path then 
+    error ("No session module started (use -top dir)");
   let oname = make_oname id in
   cache_object (oname,obj);
   add_entry oname (Leaf obj);
@@ -211,29 +216,13 @@ let is_something_opened = function
   | (_,OpenedModtype _) -> true
   | _ -> false
 
-let export_segment seg =
-  let rec clean acc = function
-    | (_,CompilingLibrary _) :: _ | [] -> acc
-    | (oname,Leaf o) as node :: stk ->
-	(match export_object o with
-	   | None -> clean acc stk
-	   | Some o' -> clean ((oname,Leaf o') :: acc) stk)
-    | (oname,ClosedSection _ as item) :: stk -> clean (item :: acc) stk
-    | (_,OpenedSection _) :: _ -> error "there are still opened sections"
-    | (_,OpenedModule _) :: _ -> error "there are still opened modules"
-    | (_,OpenedModtype _) :: _ -> error "there are still opened module types"
-    | (_,FrozenState _) :: stk -> clean acc stk
-  in
-    clean [] seg
-
-
-let start_module id mp nametab = 
+let start_module export id mp nametab = 
   let dir = extend_dirpath (fst !path_prefix) id in
   let prefix = dir,(mp,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 (prefix,nametab));
+  add_entry oname (OpenedModule (export,prefix,nametab));
   path_prefix := prefix;
   prefix
 (*  add_frozen_state () must be called in declaremods *)
@@ -241,7 +230,7 @@ let start_module id mp nametab =
 let end_module id = 
   let oname,nametab = 
     try match find_entry_p is_something_opened with
-      | oname,OpenedModule (_,nametab) -> 
+      | oname,OpenedModule (_,_,nametab) -> 
 	  let sp = fst oname in
 	  let id' = basename sp in
 	  if id<>id' then error "this is not the last opened module"; 
@@ -379,6 +368,70 @@ let is_module () =
 (* Returns the most recent OpenedThing node *)
 let what_is_opened () = find_entry_p is_something_opened
 
+(* Discharge tables *)
+
+let sectab =
+  ref ([] : (identifier list *
+             (identifier array Cmap.t * identifier array KNmap.t) *
+             (Sign.named_context Cmap.t * Sign.named_context KNmap.t)) list)
+
+let add_section () =
+  sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
+
+let add_section_variable id =
+  match !sectab with
+    | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
+    | (vars,repl,abs)::sl -> sectab := (id::vars,repl,abs)::sl
+
+let rec extract_hyps = function
+  | (id::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
+  | (id::idl,hyps) -> extract_hyps (idl,hyps)
+  | [], _ -> []
+
+let add_section_replacement f g hyps =
+  match !sectab with
+  | [] -> ()
+  | (vars,exps,abs)::sl ->
+    let sechyps = extract_hyps (vars,hyps) in
+    let args = Sign.instance_from_named_context (List.rev sechyps) in
+    sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl
+	
+let add_section_kn kn =
+  let f = (fun x (l1,l2) -> (l1,KNmap.add kn x l2)) in
+  add_section_replacement f f
+
+let add_section_constant kn =
+  let f = (fun x (l1,l2) -> (Cmap.add kn x l1,l2)) in
+  add_section_replacement f f
+
+let replacement_context () = pi2 (List.hd !sectab)
+
+let section_segment = function
+  | VarRef id ->
+      []
+  | ConstRef con -> 
+      Cmap.find con (fst (pi3 (List.hd !sectab)))
+  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+      KNmap.find kn (snd (pi3 (List.hd !sectab)))
+
+let section_instance r =
+  Sign.instance_from_named_context (List.rev (section_segment r))
+
+let init () = sectab := []
+let freeze () = !sectab
+let unfreeze s = sectab := s
+
+let _ = 
+  Summary.declare_summary "section-context"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_module = false;
+      Summary.survive_section = false }
+
+(*************)
+(* Sections. *)
+
 (* XML output hooks *)
 let xml_open_section = ref (fun id -> ())
 let xml_close_section = ref (fun id -> ())
@@ -386,8 +439,6 @@ let xml_close_section = ref (fun id -> ())
 let set_xml_open_section f = xml_open_section := f
 let set_xml_close_section f = xml_close_section := f
 
-(* Sections. *)
-
 let open_section id =
   let olddir,(mp,oldsec) = !path_prefix in
   let dir = extend_dirpath olddir id in
@@ -401,12 +452,19 @@ let open_section id =
   Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
   path_prefix := prefix;
   if !Options.xml_export then !xml_open_section id;
-  prefix
+  add_section ()
 
 
 (* Restore lib_stk and summaries as before the section opening, and
    add a ClosedSection object. *)
-let close_section ~export id =
+
+let discharge_item = function
+  | ((sp,_ as oname),Leaf lobj) ->
+      option_app (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
+  | _ ->
+      None
+
+let close_section id =
   let oname,fs = 
     try match find_entry_p is_something_opened with
       | oname,OpenedSection (_,fs) -> 
@@ -417,25 +475,26 @@ let close_section ~export id =
     with Not_found ->
       error "no opened section"
   in
-  let (after,_,before) = split_lib oname in
+  let (secdecls,_,before) = split_lib oname in
   lib_stk := before;
-  let prefix = !path_prefix in
+  let full_olddir = fst !path_prefix in
   pop_path_prefix ();
-  let closed_sec = 
-    ClosedSection (export, (fst prefix), export_segment after)
-  in
-  let name = make_path id, make_kn id in
-  add_entry name closed_sec;
+  add_entry (make_oname id) ClosedSection;
   if !Options.xml_export then !xml_close_section id;
-  (prefix, after, fs)
+  let newdecls = List.map discharge_item secdecls in
+  Summary.section_unfreeze_summaries fs;
+  List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls;
+  Cooking.clear_cooking_sharing ();
+  Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
 
+(*****************)
 (* Backtracking. *)
 
 let recache_decl = function
   | (sp, Leaf o) -> cache_object (sp,o)
+  | (_,OpenedSection _) -> add_section ()
   | _ -> ()
 
-
 let recache_context ctx =
   List.iter recache_decl ctx
 
@@ -463,7 +522,7 @@ let reset_name (loc,id) =
 
 let is_mod_node = function 
   | OpenedModule _ | OpenedModtype _ | OpenedSection _ 
-  | ClosedSection _ -> true 
+  | ClosedSection -> true 
   | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
   | _ -> false
 
@@ -471,7 +530,7 @@ let is_mod_node = function
    the same name *) 
 
 let reset_mod (loc,id) =
-  let (ent,before) = 
+  let (_,before) = 
     try
       find_split_p (fun (sp,node) -> 
                     let (_,spi) = repr_path (fst sp) in id = spi 
@@ -489,15 +548,29 @@ let reset_mod (loc,id) =
   recache_context after
 
 
-let point_obj =
-  let (f,_) = declare_object {(default_object "DOT") with
-				classify_function = (fun _ -> Dispose)} in
-    f()
+let (inLabel,outLabel) =
+  declare_object {(default_object "DOT") with
+				classify_function = (fun _ -> Dispose)}
 
-let mark_end_of_command () =
-  match !lib_stk with
-      (_,Leaf o)::_ when object_tag o = "DOT" -> ()
-    | _ -> add_anonymous_leaf point_obj
+let mark_end_of_command, current_command_label, set_command_label =
+  let n = ref 0 in
+  (fun () ->
+    match !lib_stk with
+        (_,Leaf o)::_ when object_tag o = "DOT" -> ()
+      | _ -> incr n;add_anonymous_leaf (inLabel !n)),
+  (fun () -> !n),
+  (fun x -> n:=x)
+
+let rec reset_label_stk n stk =
+  match stk with
+      (sp,Leaf o)::tail when object_tag o = "DOT" && n = outLabel o -> sp
+    | _::tail -> reset_label_stk n tail
+    | [] -> error "Unknown state number"
+
+let reset_label n = 
+  let res = reset_label_stk n !lib_stk in
+  set_command_label (n-1); (* forget state numbers after n only if reset succeeded *)
+  reset_to res
 
 let rec back_stk n stk =
   match stk with
@@ -543,6 +616,7 @@ let reset_initial () =
 	  | (_,[_,FrozenState fs as hd],before) ->
 	      lib_stk := hd::before;
 	      recalc_path_prefix ();
+			set_command_label 0;
 	      unfreeze_summaries fs
 	  | _ -> assert false
 	end
@@ -564,14 +638,39 @@ let library_part ref =
 	(* Theorem/Lemma outside its outer section of definition *)
 	dir
 
+(************************)
+(* Discharging names *)
+
+let pop_kn kn =
+  let (mp,dir,l) = Names.repr_kn kn in
+  Names.make_kn mp (dirpath_prefix dir) l
+
+let pop_con con = 
+  let (mp,dir,l) = Names.repr_con con in
+  Names.make_con mp (dirpath_prefix dir) l
+
+let con_defined_in_sec kn = 
+  let _,dir,_ = repr_con kn in
+  dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+
+let defined_in_sec kn = 
+  let _,dir,_ = repr_kn kn in
+  dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+
+let discharge_global = function
+  | ConstRef kn when con_defined_in_sec kn ->
+      ConstRef (pop_con kn)
+  | IndRef (kn,i) when defined_in_sec kn ->
+      IndRef (pop_kn kn,i)
+  | ConstructRef ((kn,i),j) when defined_in_sec kn ->
+      ConstructRef ((pop_kn kn,i),j)
+  | r -> r
+
+let discharge_kn kn = 
+  if defined_in_sec kn then pop_kn kn else kn
 
-let rec file_of_mp = function
-  | MPfile dir -> Some dir
-  | MPself _ -> Some (library_dp ())
-  | MPbound _ -> None
-  | MPdot (mp,_) -> file_of_mp mp
+let discharge_con cst = 
+  if con_defined_in_sec cst then pop_con cst else cst
 
-let file_part = function
-  | VarRef id -> anomaly "TODO";
-  | ConstRef kn | ConstructRef ((kn,_),_) | IndRef (kn,_) -> 
-      file_of_mp (modpath kn)
+let discharge_inductive (kn,i) =
+  (discharge_kn kn,i)
diff --git a/library/lib.mli b/library/lib.mli
index aa874470..22b6b6d8 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: lib.mli,v 1.41.2.3 2005/01/21 16:41:50 herbelin Exp $ i*)
+(*i $Id: lib.mli 6758 2005-02-20 18:13:28Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -14,6 +14,7 @@ open Names
 open Libnames
 open Libobject
 open Summary
+open Mod_subst
 (*i*)
 
 (*s This module provides a general mechanism to keep a trace of all operations
@@ -23,10 +24,10 @@ open Summary
 type node = 
   | Leaf of obj
   | CompilingLibrary of object_prefix
-  | OpenedModule of object_prefix * Summary.frozen
+  | OpenedModule of bool option * object_prefix * Summary.frozen
   | OpenedModtype of object_prefix * Summary.frozen
   | OpenedSection of object_prefix * Summary.frozen
-  | ClosedSection of bool * dir_path * library_segment
+  | ClosedSection
   | FrozenState of Summary.frozen
 
 and library_segment = (object_name * node) list
@@ -65,7 +66,8 @@ val add_leaves : identifier -> obj list -> object_name
 
 val add_frozen_state : unit -> unit
 val mark_end_of_command : unit -> unit
-
+val current_command_label : unit -> int
+val reset_label : int -> unit
 
 (*s The function [contents_after] returns the current library segment, 
   starting from a given section path. If not given, the entire segment
@@ -82,6 +84,7 @@ val make_path : identifier -> section_path
 (* Kernel-side names *)
 val current_prefix : unit -> module_path * dir_path
 val make_kn : identifier -> kernel_name
+val make_con : identifier -> constant
 
 (* Are we inside an opened section *)
 val sections_are_opened : unit -> bool
@@ -99,7 +102,7 @@ val what_is_opened : unit -> object_name * node
 (*s Modules and module types *)
 
 val start_module : 
-  module_ident -> module_path -> Summary.frozen -> object_prefix
+  bool option -> module_ident -> module_path -> Summary.frozen -> object_prefix
 val end_module : module_ident 
   -> object_name * object_prefix * Summary.frozen * library_segment
 
@@ -121,15 +124,10 @@ val library_dp : unit -> dir_path
 (* Extract the library part of a name even if in a section *)
 val library_part : global_reference -> dir_path
 
-(* Extract the library part of a name if not in a functor *)
-val file_part : global_reference -> dir_path option
-
 (*s Sections *)
 
-val open_section : identifier -> object_prefix
-
-val close_section : export:bool -> identifier -> 
-  object_prefix * library_segment * Summary.frozen
+val open_section : identifier -> unit
+val close_section : identifier -> unit
 
 (*s Backtracking (undo). *)
 
@@ -157,3 +155,24 @@ val reset_initial : unit -> unit
 (* XML output hooks *)
 val set_xml_open_section : (identifier -> unit) -> unit
 val set_xml_close_section : (identifier -> unit) -> unit
+
+
+(*s Section management for discharge *)
+
+val section_segment : global_reference -> Sign.named_context
+val section_instance : global_reference -> Term.constr array
+
+val add_section_variable : identifier -> unit
+val add_section_constant : constant -> Sign.named_context -> unit
+val add_section_kn : kernel_name -> Sign.named_context -> unit
+val replacement_context : unit ->
+  (identifier array Cmap.t * identifier array KNmap.t)
+
+(*s Discharge: decrease the section level if in the current section *)
+
+val discharge_kn :  kernel_name -> kernel_name
+val discharge_con : constant -> constant
+val discharge_global : global_reference -> global_reference
+val discharge_inductive : inductive -> inductive
+
+
diff --git a/library/libnames.ml b/library/libnames.ml
index 16f5a917..536a382d 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -6,13 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.ml,v 1.11.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+(*i $Id: libnames.ml 7052 2005-05-20 15:54:50Z herbelin $ i*)
 
 open Pp
 open Util
 open Names
 open Nameops
 open Term
+open Mod_subst
 
 type global_reference =
   | VarRef of variable
@@ -21,30 +22,34 @@ type global_reference =
   | ConstructRef of constructor
 
 let subst_global subst ref = match ref with
-  | VarRef _ -> ref
+  | VarRef var -> ref, mkVar var
   | ConstRef kn ->
-      let kn' = subst_kn subst kn in if kn==kn' then ref else
-          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 if kn==kn' then ref else
-          IndRef(kn',i)
+      let kn' = subst_kn subst kn in
+      if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
   | ConstructRef ((kn,i),j) ->
-      let kn' = subst_kn subst kn in if kn==kn' then ref else
-          ConstructRef ((kn',i),j)
+      let kn' = subst_kn subst kn in 
+      if kn==kn' then ref, mkConstruct ((kn,i),j)
+      else ConstructRef ((kn',i),j), mkConstruct ((kn',i),j)
 
-let reference_of_constr c = match kind_of_term c with
+let global_of_constr c = match kind_of_term c with
   | Const sp -> ConstRef sp
   | Ind ind_sp -> IndRef ind_sp
   | Construct cstr_cp -> ConstructRef cstr_cp
   | Var id -> VarRef id
   |  _ -> raise Not_found
 
-let constr_of_reference = function
+let constr_of_global = function
   | VarRef id -> mkVar id
   | ConstRef sp -> mkConst sp
   | ConstructRef sp -> mkConstruct sp
   | IndRef sp -> mkInd sp
 
+let constr_of_reference = constr_of_global
+let reference_of_constr = global_of_constr
+
 module RefOrdered =
   struct
     type t = global_reference
@@ -54,24 +59,8 @@ module RefOrdered =
 module Refset = Set.Make(RefOrdered)
 module Refmap = Map.Make(RefOrdered)
 
-module InductiveOrdered = struct
-  type t = inductive
-  let compare (spx,ix) (spy,iy) = 
-    let c = ix - iy in if c = 0 then compare spx spy else c
-end
-
-module Indmap = Map.Make(InductiveOrdered)
-
 let inductives_table = ref Indmap.empty
 
-module ConstructorOrdered = struct
-  type t = constructor
-  let compare (indx,ix) (indy,iy) = 
-    let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c
-end
-
-module Constrmap = Map.Make(ConstructorOrdered)
-
 (**********************************************)
 
 let pr_dirpath sl = (str (string_of_dirpath sl))
@@ -188,18 +177,10 @@ type extended_global_reference =
   | TrueGlobal of global_reference
   | SyntacticDef of kernel_name
 
-let subst_ext subst glref = match glref with
-  | TrueGlobal ref -> 
-      let ref' = subst_global subst ref in
-	if ref' == ref then glref else
-	  TrueGlobal ref'
-  | SyntacticDef kn ->
-      let kn' = subst_kn subst kn in
-	if kn' == kn then glref else
-	  SyntacticDef kn'
-
 let encode_kn dir id = make_kn (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 mp,sec_dir,l = repr_kn kn in
     match mp,(repr_dirpath sec_dir) with
@@ -207,6 +188,13 @@ let decode_kn kn =
       | _ , [] -> anomaly "MPfile expected!"
       | _ -> anomaly "Section part should be empty!"
 
+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)
+      | _ , [] -> anomaly "MPfile expected!"
+      | _ -> anomaly "Section part should be empty!"
+
 (*s qualified names *)
 type qualid = section_path
 
@@ -267,3 +255,4 @@ let pr_reference = function
 let loc_of_reference = function
   | Qualid (loc,qid) -> loc
   | Ident (loc,id) -> loc
+
diff --git a/library/libnames.mli b/library/libnames.mli
index a6055428..06595e81 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -6,13 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.mli,v 1.8.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
+(*i $Id: libnames.mli 7052 2005-05-20 15:54:50Z herbelin $ i*)
 
 (*i*)
 open Pp
 open Util
 open Names
 open Term
+open Mod_subst
 (*i*)
 
 (*s Global reference is a kernel side type for all references together *)
@@ -22,21 +23,22 @@ type global_reference =
   | IndRef of inductive
   | ConstructRef of constructor
 
-val subst_global : substitution -> global_reference -> global_reference
+val subst_global : substitution -> global_reference -> global_reference * constr
 
 (* Turn a global reference into a construction *)
-val constr_of_reference : global_reference -> constr
+val constr_of_global : global_reference -> constr
+
+(* Turn a construction denoting a global reference into a global reference;
+   raise [Not_found] if not a global reference *)
+val global_of_constr : constr -> global_reference
 
-(* Turn a construction denoting a global into a reference;
-   raise [Not_found] if not a global *)
+(* Obsolete synonyms for constr_of_global and global_of_constr *)
+val constr_of_reference : global_reference -> constr
 val reference_of_constr : constr -> global_reference
 
 module Refset : Set.S with type elt = global_reference 
 module Refmap : Map.S with type key = global_reference
 
-module Indmap : Map.S with type key = inductive
-module Constrmap : Map.S with type key = constructor
-
 (*s Dirpaths *)
 val pr_dirpath : dir_path -> Pp.std_ppcmds
 
@@ -82,13 +84,12 @@ type extended_global_reference =
   | TrueGlobal of global_reference
   | SyntacticDef of kernel_name
 
-val subst_ext : 
-  substitution -> extended_global_reference -> extended_global_reference
-
 (*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_con : dir_path -> identifier -> constant
+val decode_con : constant -> dir_path * identifier
 
 
 (*s A [qualid] is a partially qualified ident; it includes fully
diff --git a/library/libobject.ml b/library/libobject.ml
index 2e531e05..708c19b1 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,11 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: libobject.ml,v 1.8.8.1 2004/07/16 19:30:35 herbelin Exp $ *)
+(* $Id: libobject.ml 6748 2005-02-18 22:17:50Z herbelin $ *)
 
 open Util
 open Names
 open Libnames
+open Mod_subst
 
 (* The relax flag is used to make it possible to load files while ignoring
    failures to incorporate some objects.  This can be useful when one
@@ -35,6 +36,7 @@ type 'a object_declaration = {
   open_function : int -> object_name * 'a -> unit;
   classify_function : object_name * 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
+  discharge_function : object_name * 'a -> 'a option;
   export_function : 'a -> 'a option }
 
 let yell s = anomaly s
@@ -47,6 +49,7 @@ let default_object s = {
   subst_function = (fun _ -> 
     yell ("The object "^s^" does not know how to substitute!"));
   classify_function = (fun (_,obj) -> Keep obj);
+  discharge_function = (fun _ -> None);
   export_function = (fun _ -> None)} 
 
 
@@ -71,6 +74,7 @@ type dynamic_object_declaration = {
   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_discharge_function : object_name * obj -> obj option;
   dyn_export_function : obj -> obj option }
 
 let object_tag lobj = Dyn.tag lobj
@@ -103,6 +107,11 @@ let declare_object odecl =
 	| Anticipate (obj) -> Anticipate (infun obj)
     else 
       anomaly "somehow we got the wrong dynamic object in the classifyfun"
+  and discharge (oname,lobj) = 
+    if Dyn.tag lobj = na then 
+      option_app infun (odecl.discharge_function (oname,outfun lobj))
+    else 
+      anomaly "somehow we got the wrong dynamic object in the dischargefun"
   and exporter lobj = 
     if Dyn.tag lobj = na then 
       option_app infun (odecl.export_function (outfun lobj))
@@ -115,6 +124,7 @@ let declare_object odecl =
                              dyn_open_function = opener;
 			     dyn_subst_function = substituter;
 			     dyn_classify_function = classifier;
+			     dyn_discharge_function = discharge;
                              dyn_export_function = exporter };
   (infun,outfun)
 
@@ -153,5 +163,8 @@ let subst_object ((_,_,lobj) as node) =
 let classify_object ((_,lobj) as node) = 
   apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj
 
+let discharge_object ((_,lobj) as node) = 
+  apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
+
 let export_object lobj =
   apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index b9070f5d..88a12db9 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -6,11 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libobject.mli,v 1.9.8.2 2005/01/21 16:41:51 herbelin Exp $ i*)
+(*i $Id: libobject.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
 
 (*i*)
 open Names
 open Libnames
+open Mod_subst
 (*i*)
 
 (* [Libobject] declares persistent objects, given with methods:
@@ -69,6 +70,7 @@ type 'a object_declaration = {
   open_function : int -> object_name * 'a -> unit;
   classify_function : object_name * 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
+  discharge_function : object_name * 'a -> 'a option;
   export_function : 'a -> 'a option }
 
 (* The default object is a "Keep" object with empty methods. 
@@ -102,4 +104,5 @@ 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 discharge_object : object_name * obj -> obj option
 val relax : bool -> unit
diff --git a/library/library.ml b/library/library.ml
index aaed4545..760b6f07 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml,v 1.79.2.5 2006/01/10 17:06:23 barras Exp $ *)
+(* $Id: library.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
 
 open Pp
 open Util
@@ -25,30 +25,57 @@ open Declaremods
 
 type logical_path = dir_path
 
-let load_path = ref ([],[] : System.physical_path list * logical_path list)
+let load_paths = ref ([],[] : System.physical_path list * logical_path list)
 
-let get_load_path () = fst !load_path
+let get_load_paths () = fst !load_paths
+
+(* Hints to partially detects if two paths refer to the same repertory *)
+let rec remove_path_dot p = 
+  let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
+  let n = String.length curdir in
+  if String.length p > n && String.sub p 0 n = curdir then
+    remove_path_dot (String.sub p n (String.length p - n))
+  else
+    p
+
+let strip_path p =
+  let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
+  let n = String.length cwd in
+  if String.length p > n && String.sub p 0 n = cwd then
+    remove_path_dot (String.sub p n (String.length p - n))
+  else
+    remove_path_dot p
+
+let canonical_path_name p =
+  let current = Sys.getcwd () in
+  try 
+    Sys.chdir p;
+    let p' = Sys.getcwd () in
+    Sys.chdir current;
+    p'
+  with Sys_error _ ->
+    (* We give up to find a canonical name and just simplify it... *)
+    strip_path p
 
 
 let find_logical_path phys_dir = 
-  let phys_dir = System.canonical_path_name phys_dir in
-  match list_filter2 (fun p d -> p = phys_dir) !load_path with
+  let phys_dir = canonical_path_name phys_dir in
+  match list_filter2 (fun p d -> p = phys_dir) !load_paths with
   | _,[dir] -> dir
   | _,[] -> Nameops.default_root_prefix
   | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
 
-let remove_path dir =
-  let dir = System.canonical_path_name dir in
-  load_path := list_filter2 (fun p d -> p <> dir) !load_path
+let remove_load_path dir =
+  load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
 
-let add_load_path_entry (phys_path,coq_path) =
-  let phys_path = System.canonical_path_name phys_path in
-  match list_filter2 (fun p d -> p = phys_path) !load_path with
+let add_load_path (phys_path,coq_path) =
+  let phys_path = canonical_path_name phys_path in
+  match list_filter2 (fun p d -> p = phys_path) !load_paths with
   | _,[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
+        (phys_path = canonical_path_name Filename.current_dir_name
          && coq_path = Nameops.default_root_prefix)
       then
 	begin
@@ -58,19 +85,19 @@ let add_load_path_entry (phys_path,coq_path) =
 	    ^(string_of_dirpath dir)
 	    ^("\nIt is remapped to "^(string_of_dirpath coq_path)));
              flush_all ());
-	  remove_path phys_path;
-	  load_path := (phys_path::fst !load_path, coq_path::snd !load_path)
+	  remove_load_path phys_path;
+	  load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
 	end
   | _,[] ->
-      load_path := (phys_path :: fst !load_path, coq_path :: snd !load_path)
+      load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
   | _ -> anomaly ("Two logical paths are associated to "^phys_path)
 
 let physical_paths (dp,lp) = dp
 
-let load_path_of_logical_path dir =
-  fst (list_filter2 (fun p d -> d = dir) !load_path)
+let load_paths_of_dir_path dir =
+  fst (list_filter2 (fun p d -> d = dir) !load_paths)
 
-let get_full_load_path () = List.combine (fst !load_path) (snd !load_path)
+let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
 
 (************************************************************************)
 (*s Modules on disk contain the following informations (after the magic 
@@ -97,7 +124,7 @@ type library_t = {
   library_imports : compilation_unit_name list;
   library_digest : Digest.t }
 
-module CompilingLibraryOrdered = 
+module LibraryOrdered = 
   struct
     type t = dir_path
     let compare d1 d2 =
@@ -105,12 +132,12 @@ module CompilingLibraryOrdered =
         (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
   end
 
-module CompilingLibraryMap = Map.Make(CompilingLibraryOrdered)
+module LibraryMap = Map.Make(LibraryOrdered)
 
-(* This is a map from names to libraries *)
-let libraries_table = ref CompilingLibraryMap.empty
+(* This is a map from names to loaded libraries *)
+let libraries_table = ref LibraryMap.empty
 
-(* These are the _ordered_ lists of loaded, imported and exported libraries *)
+(* These are the _ordered_ sets of loaded, imported and exported libraries *)
 let libraries_loaded_list = ref []
 let libraries_imports_list = ref []
 let libraries_exports_list = ref []
@@ -128,7 +155,7 @@ let unfreeze (mt,mo,mi,me) =
   libraries_exports_list := me
 
 let init () =
-  libraries_table := CompilingLibraryMap.empty;
+  libraries_table := LibraryMap.empty;
   libraries_loaded_list := [];
   libraries_imports_list := [];
   libraries_exports_list := []
@@ -141,18 +168,20 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section = false }
 
-let find_library s =
-  CompilingLibraryMap.find s !libraries_table
+(* various requests to the tables *)
 
-let try_find_library s =
-  try find_library s
+let find_library dir =
+  LibraryMap.find dir !libraries_table
+
+let try_find_library dir =
+  try find_library dir
   with Not_found ->
-    error ("Unknown library " ^ (string_of_dirpath s))
+    error ("Unknown library " ^ (string_of_dirpath dir))
 
-let library_full_filename m = (find_library m).library_filename
+let library_full_filename dir = (find_library dir).library_filename
 
 let library_is_loaded dir =
-  try let _ = CompilingLibraryMap.find dir !libraries_table in true
+  try let _ = find_library dir in true
   with Not_found -> false
 
 let library_is_opened dir = 
@@ -176,7 +205,7 @@ let register_loaded_library m =
     | m'::_ as l when m'.library_name = m.library_name -> l
     | m'::l' -> m' :: aux l' in
   libraries_loaded_list := aux !libraries_loaded_list;
-  libraries_table := CompilingLibraryMap.add m.library_name m !libraries_table
+  libraries_table := LibraryMap.add m.library_name m !libraries_table
 
   (* ... while if a library is imported/exported several time, then
      only the last occurrence is really needed - though the imported
@@ -198,10 +227,8 @@ let register_open_library export m =
 (************************************************************************)
 (*s Opening libraries *)
 
-(*s [open_library s] opens a library. The library [s] and all
-  libraries needed by [s] are assumed to be already loaded. When
-  opening [s] we recursively open all the libraries needed by [s]
-  and tagged [exported]. *)
+(* [open_library export explicit m] opens library [m] if not already
+   opened _or_ if explicitly asked to be (re)opened *)
 
 let eq_lib_name m1 m2 = m1.library_name = m2.library_name
 
@@ -219,7 +246,10 @@ let open_library export explicit_libs m =
     if export then 
       libraries_exports_list := remember_last_of_each !libraries_exports_list m
 
-let open_libraries export modl = 
+(* 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 = 
     List.fold_left
       (fun l m ->
@@ -261,77 +291,94 @@ let (in_import, out_import) =
 
 
 (************************************************************************)
-(*s Loading from disk to cache (preparation phase) *)
-
-let vo_magic_number7 = 07993 (* V8.0pl3 final old syntax *)
-let vo_magic_number8 = 08003 (* V8.0pl3 final new syntax *)
+(*s Low-level interning/externing of libraries to files *)
 
-let (raw_extern_library7, raw_intern_library7) =
-  System.raw_extern_intern vo_magic_number7 ".vo"
-
-let (raw_extern_library8, raw_intern_library8) =
-  System.raw_extern_intern vo_magic_number8 ".vo"
+(*s Loading from disk to cache (preparation phase) *)
 
-let raw_intern_library a =
-  if !Options.v7 then
-    try raw_intern_library7 a
-    with System.Bad_magic_number fname ->
-      let _= raw_intern_library8 a in
-      error "Inconsistent compiled files: you probably want to use Coq in new syntax and remove the option -v7 or -translate"
-  else
-    try raw_intern_library8 a
-    with System.Bad_magic_number fname ->
-      let _= raw_intern_library7 a in
-      error "Inconsistent compiled files: you probably want to use Coq in old syntax by setting options -v7 or -translate"
+let vo_magic_number = 08003 (* V8.0 final new syntax + new params in ind *)
 
-let raw_extern_library =
-  if !Options.v7 then raw_extern_library7 else raw_extern_library8
+let (raw_extern_library, raw_intern_library) =
+  System.raw_extern_intern vo_magic_number ".vo"
 
-(* cache for loaded libraries *)
-let compunit_cache = ref CompilingLibraryMap.empty
+let with_magic_number_check f a =
+  try f a
+  with System.Bad_magic_number fname ->
+    errorlabstrm "with_magic_number_check"
+    (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++
+    spc () ++ str"It is corrupted" ++ spc () ++
+    str"or was compiled with another version of Coq.")
 
-let _ = 
-  Summary.declare_summary "MODULES-CACHE"
-    { Summary.freeze_function = (fun () -> !compunit_cache);
-      Summary.unfreeze_function = (fun cu -> compunit_cache := cu);
-      Summary.init_function = 
-	(fun () -> compunit_cache := CompilingLibraryMap.empty);
-      Summary.survive_module = true;
-      Summary.survive_section = true }
-
-(*s [load_library s] loads the library [s] from the disk, and [find_library s]
-   returns the library of name [s], loading it if necessary. 
-   The boolean [doexp] specifies if we open the libraries which are declared
-   exported in the dependencies (it is [true] at the highest level;
-   then same value as for caller is reused in recursive loadings). *)
+(************************************************************************)
+(*s Locate absolute or partially qualified library names in the path *)
 
 exception LibUnmappedDir
 exception LibNotFound
 type library_location = LibLoaded | LibInPath
 
 let locate_absolute_library dir =
-  (* Look if loaded in current environment *)
-  try
-    let m = CompilingLibraryMap.find dir !libraries_table in
-    (dir, m.library_filename)
-  with Not_found ->
-  (* Look if in loadpath *)
+  (* Search in loadpath *)
+  let pref, base = split_dirpath dir in
+  let loadpath = load_paths_of_dir_path pref in
+  if loadpath = [] then raise LibUnmappedDir;
   try
-    let pref, base = split_dirpath dir in
-    let loadpath = load_path_of_logical_path pref in
-    if loadpath = [] then raise LibUnmappedDir;
     let name = (string_of_id base)^".vo" in
     let _, file = System.where_in_path loadpath name in
     (dir, file)
-  with Not_found ->  raise LibNotFound
+  with Not_found ->
+  (* Last chance, removed from the file system but still in memory *)
+  try
+    (dir, library_full_filename dir)
+  with Not_found ->
+    raise LibNotFound
 
-let with_magic_number_check f a =
-  try f a
-  with System.Bad_magic_number fname ->
-    errorlabstrm "with_magic_number_check"
-    (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++
-    spc () ++ str"It is corrupted" ++ spc () ++
-    str"or was compiled with another version of Coq.")
+let locate_qualified_library qid =
+  try
+    (* Search library in loadpath *)
+    let dir, base = repr_qualid qid in 
+    let loadpath =
+      if repr_dirpath dir = [] then get_load_paths ()
+      else 
+        (* we assume dir is an absolute dirpath *)
+	load_paths_of_dir_path dir
+    in
+    if loadpath = [] then raise LibUnmappedDir;
+    let name =  (string_of_id base)^".vo" in
+    let path, file = System.where_in_path loadpath name in
+    let dir = extend_dirpath (find_logical_path path) base in
+    (* Look if loaded *)
+    try 
+      (LibLoaded, dir, library_full_filename dir)      
+    with Not_found ->
+      (LibInPath, dir, file)
+  with Not_found -> raise LibNotFound
+
+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 "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
+  | LibNotFound ->
+      errorlabstrm "load_absolute_library_from"
+      (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath")
+  | e -> raise e
+
+let try_locate_absolute_library dir =
+  try
+    locate_absolute_library dir
+  with e ->
+    explain_locate_library_error (qualid_of_dirpath dir) e
+
+let try_locate_qualified_library (loc,qid) =
+  try
+    let (_,dir,f) = locate_qualified_library qid in
+    dir,f
+  with e -> 
+    explain_locate_library_error qid e
+
+
+(************************************************************************)
+(* Internalise libraries *)
 
 let lighten_library m = 
   if !Options.dont_load_proofs then lighten_library m else m
@@ -352,55 +399,35 @@ let intern_from_file f =
   close_in ch;
   mk_library md f digest
 
-let rec intern_library (dir, f) =
-  try
-    (* Look if in the current logical environment *)
-    CompilingLibraryMap.find dir !libraries_table
+let rec intern_library needed (dir, f) =
+  (* Look if in the current logical environment *)
+  try find_library dir, needed
   with Not_found ->
-  try
-    (* Look if already loaded in cache and consequently its dependencies *)
-    CompilingLibraryMap.find dir !compunit_cache
+  (* Look if already listed and consequently its dependencies too *)
+  try List.assoc dir needed, needed
   with Not_found ->
-    (* [dir] is an absolute name which matches [f] which must be in loadpath *)
-    let m = intern_from_file f in
-    if dir <> m.library_name then
-      errorlabstrm "load_physical_library"
-	(str ("The file " ^ f ^ " contains library") ++ spc () ++
-	 pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
-         spc() ++ pr_dirpath dir);
-    intern_and_cache_library dir m
-
-and intern_and_cache_library dir m =
-  compunit_cache := CompilingLibraryMap.add dir m !compunit_cache;
-  try
-    List.iter (intern_mandatory_library dir) m.library_deps;
-    m
-  with e ->
-    compunit_cache := CompilingLibraryMap.remove dir !compunit_cache; 
-    raise e
+  (* [dir] is an absolute name which matches [f] which must be in loadpath *)
+  let m = intern_from_file f in
+  if dir <> m.library_name then
+    errorlabstrm "load_physical_library"
+      (str ("The file " ^ f ^ " contains library") ++ spc () ++
+       pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
+       spc() ++ pr_dirpath dir);
+  m, intern_library_deps needed dir m
 
-and intern_mandatory_library caller (dir,d) =
-  let m = intern_absolute_library_from dir in
+and intern_library_deps needed dir m =
+  (dir,m)::List.fold_left (intern_mandatory_library dir) needed m.library_deps
+
+and intern_mandatory_library caller needed (dir,d) =
+  let m,needed = intern_library needed (try_locate_absolute_library dir) in
   if d <> m.library_digest then
     error ("compiled library "^(string_of_dirpath caller)^
 	   " makes inconsistent assumptions over library "
-	   ^(string_of_dirpath dir))
-
-and intern_absolute_library_from dir =
-  try
-    intern_library (locate_absolute_library dir)
-  with
-  | LibUnmappedDir ->
-      let prefix, dir = fst (split_dirpath dir), string_of_dirpath dir in
-      errorlabstrm "load_absolute_library_from"
-      (str ("Cannot load "^dir^":") ++ spc () ++ 
-      str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
-  | LibNotFound ->
-      errorlabstrm "load_absolute_library_from"
-      (str"Cannot find library " ++ pr_dirpath dir ++ str" in loadpath")
-  | e -> raise e
+	   ^(string_of_dirpath dir));
+  needed
 
-let rec_intern_library mref = let _ = intern_library mref in ()
+let rec_intern_library needed mref =
+  let _,needed = intern_library needed mref in needed
 
 let check_library_short_name f dir = function
   | Some id when id <> snd (split_dirpath dir) ->
@@ -416,55 +443,18 @@ let rec_intern_by_filename_only id f =
   check_library_short_name f m.library_name id;
   (* We check no other file containing same library is loaded *)
   try
-    let m' = CompilingLibraryMap.find m.library_name !libraries_table in
+    let m' = find_library m.library_name in
     Options.if_verbose warning 
       ((string_of_dirpath m.library_name)^" is already loaded from file "^
        m'.library_filename);
-    m.library_name
+    m.library_name, []
   with Not_found ->
-    let m = intern_and_cache_library m.library_name m in
-    m.library_name
-
-let locate_qualified_library qid =
-  try
-    (* Search library in loadpath *)
-    let dir, base = repr_qualid qid in 
-    let loadpath =
-      if repr_dirpath dir = [] then get_load_path ()
-      else 
-        (* we assume dir is an absolute dirpath *)
-	load_path_of_logical_path dir
-    in
-    if loadpath = [] then raise LibUnmappedDir;
-    let name =  (string_of_id base)^".vo" in
-    let path, file = System.where_in_path loadpath name in
-    let dir = extend_dirpath (find_logical_path path) base in
-    (* Look if loaded *)
-    try 
-      (LibLoaded, dir, library_full_filename dir)      
-    with Not_found ->
-      (LibInPath, dir, file)
-  with Not_found -> raise LibNotFound
-
-let rec_intern_qualified_library (loc,qid) =
-  try
-    let (_,dir,f) = locate_qualified_library qid in
-    rec_intern_library (dir,f);
-    dir
-  with
-  | LibUnmappedDir ->
-      let prefix, id = repr_qualid qid in
-      user_err_loc (loc, "rec_intern_qualified_library",
-        str ("Cannot load "^(string_of_id id)^":") ++ spc () ++ 
-        str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++
-        fnl ())
-  | LibNotFound ->
-      user_err_loc (loc, "rec_intern_qualified_library",
-        str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath")
+    let needed = intern_library_deps [] m.library_name m in
+    m.library_name, needed
 
 let rec_intern_library_from_file idopt f =
   (* A name is specified, we have to check it contains library id *)
-  let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
+  let _, f = System.find_file_in_path (get_load_paths ()) (f^".vo") in
   rec_intern_by_filename_only idopt f
 
 (**********************************************************************)
@@ -472,8 +462,11 @@ let rec_intern_library_from_file idopt f =
     operation. It is performed as follows:
 
   preparation phase: (functions require_library* ) the library and its 
-    dependencies are read from to disk to the compunit_cache 
-    (using intern_* )
+    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
+     section/module is the one that was used at type-checking time in
+     the section/module]
 
   execution phase: (through add_leaf and cache_require)
     the library is loaded in the environment and Nametab, the objects are 
@@ -487,117 +480,83 @@ let rec_intern_library_from_file idopt f =
 
 type library_reference = dir_path list * bool option
 
-let string_of_library (_,dir,_) = string_of_id (List.hd (repr_dirpath dir))
+let register_library (dir,m) =
+  Declaremods.register_library
+    m.library_name 
+    m.library_compiled 
+    m.library_objects 
+    m.library_digest;
+  register_loaded_library m
 
-let rec load_library dir =
-  try
-    (* Look if loaded in current env (and consequently its dependencies) *)
-    CompilingLibraryMap.find dir !libraries_table
-  with Not_found ->
-    (* [dir] is an absolute name matching [f] which must be in loadpath *)
-    let m =
-      try CompilingLibraryMap.find dir !compunit_cache
-      with Not_found ->
-        anomaly ((string_of_dirpath dir)^" should be in cache")
-    in
-    List.iter (fun (dir,_) -> ignore (load_library dir)) m.library_deps;
-    Declaremods.register_library
-      m.library_name 
-      m.library_compiled 
-      m.library_objects 
-      m.library_digest;
-    register_loaded_library m;
-    m
-
-let cache_require (_,(modl,export)) =
-  let ml = list_map_left load_library modl in
-  match export with
-    | None -> ()
-    | Some export -> open_libraries export ml
-
-let load_require  _ (_,(modl,_)) =
-  ignore(list_map_left load_library modl)
+  (* [needed] is the ordered list of libraries not already loaded *)
+let cache_require (_,(needed,modl,export)) =
+  List.iter register_library needed;
+  option_iter (fun exp -> open_libraries exp (List.map find_library modl))
+    export
+
+let load_require  _ (_,(needed,modl,_)) =
+  List.iter register_library needed
 
   (* 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 export_require (_,l,e) = Some ([],l,e)
+
+let discharge_require (_,o) = Some o
 
 let (in_require, out_require) =
   declare_object {(default_object "REQUIRE") with
        cache_function = cache_require;
        load_function = load_require;
        export_function = export_require;
+       discharge_function = discharge_require;
        classify_function = (fun (_,o) -> Anticipate o) }
 
+(* Require libraries, import them if [export <> None], mark them for export
+   if [export = Some true] *)
+
+(* read = require without opening *)
+
 let xml_require = ref (fun d -> ())
 let set_xml_require f = xml_require := f
 
-let require_library spec qidl export =
-(*
-  if sections_are_opened () && Options.verbose () then
-    warning ("Objets of "^(string_of_library modref)^
-             " not surviving sections (e.g. Grammar \nand Hints)\n"^
-             "will be removed at the end of the section");
-*)
-  let modrefl = List.map rec_intern_qualified_library qidl in
+let require_library qidl export =
+  let modrefl = List.map try_locate_qualified_library qidl in
+  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 begin
-      add_anonymous_leaf (in_require (modrefl,None));
-      List.iter
-	(fun dir ->
-	   add_anonymous_leaf (in_import (dir, export)))
-	modrefl
+      add_anonymous_leaf (in_require (needed,modrefl,None));
+      option_iter (fun exp ->
+	List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
+	export
     end
     else
-      add_anonymous_leaf (in_require (modrefl,Some export));
+      add_anonymous_leaf (in_require (needed,modrefl,export));
   if !Options.xml_export then List.iter !xml_require modrefl;
   add_frozen_state ()
 
-let require_library_from_file spec idopt file export =
-  let modref = rec_intern_library_from_file idopt file in
-    if Lib.is_modtype () || Lib.is_module () then begin
-      add_anonymous_leaf (in_require ([modref],None));
-      add_anonymous_leaf (in_import (modref, export))
-    end
-    else
-      add_anonymous_leaf (in_require ([modref],Some export));
-    if !Options.xml_export then !xml_require modref;
-    add_frozen_state ()
-
-
-(* read = require without opening *)
-
-let read_library qid =
-  let modref = rec_intern_qualified_library qid in
-  add_anonymous_leaf (in_require ([modref],None));
-  if !Options.xml_export then !xml_require modref;
-  add_frozen_state ()
-
-let read_library_from_file f =
-  let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in
-  let modref = rec_intern_by_filename_only None f in
-  add_anonymous_leaf (in_require ([modref],None));
+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
+  if Lib.is_modtype () || Lib.is_module () then begin
+    add_anonymous_leaf (in_require (needed,[modref],None));
+    option_iter (fun exp -> add_anonymous_leaf (in_import (modref,exp)))
+      export
+  end
+  else
+    add_anonymous_leaf (in_require (needed,[modref],export));
   if !Options.xml_export then !xml_require modref;
   add_frozen_state ()
 
-
-(* called at end of section *)
-
-let reload_library modrefl =
-  add_anonymous_leaf (in_require modrefl);
-  add_frozen_state ()
-
-
-
 (* the function called by Vernacentries.vernac_import *)
 
-let import_library export (loc,qid) =
+let import_module export (loc,qid) =
   try
     match Nametab.locate_module qid with
 	MPfile dir -> 
 	  if Lib.is_modtype () || Lib.is_module () || not export then
 	    add_anonymous_leaf (in_import (dir, export))
 	  else
-	    add_anonymous_leaf (in_require ([dir], Some export))
+	    add_anonymous_leaf (in_require ([],[dir], Some export))
       | mp ->
 	  import_module export mp
   with
@@ -607,27 +566,30 @@ let import_library export (loc,qid) =
 	 str ((string_of_qualid qid)^" is not a module"))
   
 (************************************************************************)
-(*s [save_library s] saves the library [m] to the disk. *)
+(*s Initializing the compilation of a library. *)
 
 let start_library f = 
   let _,longf = 
-    System.find_file_in_path (get_load_path ()) (f^".v") in
+    System.find_file_in_path (get_load_paths ()) (f^".v") in
   let ldir0 = find_logical_path (Filename.dirname longf) in
   let id = id_of_string (Filename.basename f) in
   let ldir = extend_dirpath ldir0 id in
   Declaremods.start_library ldir;
   ldir,longf
 
+(************************************************************************)
+(*s [save_library dir] ends library [dir] and save it to the disk. *)
+
 let current_deps () =
   List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list
 
 let current_reexports () =
   List.map (fun m -> m.library_name) !libraries_exports_list
 
-let save_library_to s f =
-  let cenv, seg = Declaremods.end_library s in
+let save_library_to dir f =
+  let cenv, seg = Declaremods.end_library dir in
   let md = { 
-    md_name = s;
+    md_name = dir;
     md_compiled = cenv;
     md_objects = seg;
     md_deps = current_deps ();
@@ -641,33 +603,7 @@ let save_library_to s f =
     close_out ch
   with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e)
 
-(*s Pretty-printing of libraries state. *)
- 
-(* this function is not used... *)
-let fmt_libraries_state () =
-  let opened = opened_libraries ()
-  and loaded = loaded_libraries () in
-  (str "Imported (open) Modules: " ++
-     prlist_with_sep pr_spc pr_dirpath opened ++ fnl () ++
-     str "Loaded Modules: " ++
-     prlist_with_sep pr_spc pr_dirpath loaded ++ fnl ())
-
-
-(*s For tactics/commands requiring vernacular libraries *)
-
-let check_required_library d =
-  let d' = List.map id_of_string d in
-  let dir = make_dirpath (List.rev d') in
-  if not (library_is_loaded dir) then
-(* Loading silently ...
-    let m, prefix = list_sep_last d' in
-    read_library 
-     (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
-*)
-(* or failing ...*)
-    error ("Library "^(list_last d)^" has to be required first")
-
-
+(************************************************************************)
 (*s Display the memory use of a library. *)
 
 open Printf
diff --git a/library/library.mli b/library/library.mli
index 18be1671..f7620682 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,v 1.23.2.1 2004/07/16 19:30:36 herbelin Exp $ i*)
+(*i $Id: library.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -15,65 +15,58 @@ open Libnames
 open Libobject
 (*i*)
 
-(*s This module is the heart of the library. It provides low level
-  functions to load, open and save libraries. Libraries are saved
-  onto the disk with checksums (obtained with the [Digest] module),
-  which are checked at loading time to prevent inconsistencies
-  between files written at various dates. It also provides a high
-  level function [require] which corresponds to the vernacular
-  command [Require]. *)
+(*s This module provides functions to load, open and save
+  libraries. Libraries correspond to the subclass of modules that
+  coincide with a file on disk (the ".vo" files). Libraries on the
+  disk comes with checksums (obtained with the [Digest] module), which
+  are checked at loading time to prevent inconsistencies between files
+  written at various dates.
+*)
+
+(*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_file :
+  identifier option -> System.physical_path -> bool option -> unit
+
+(*s Open a module (or a library); if the boolean is true then it's also
+   an export otherwise just a simple import *)
+val import_module : bool -> qualid located -> unit
 
-val read_library : qualid located -> unit
+(*s Start the compilation of a library *)
+val start_library : string -> dir_path * string
 
-val read_library_from_file : System.physical_path -> unit
+(*s End the compilation of a library and save it to a ".vo" file *)
+val save_library_to : dir_path -> string -> unit
 
-(* [import_library true qid] = [export qid] *)
- 
-val import_library : bool -> qualid located -> unit
+(*s Interrogate the status of libraries *)
 
+  (* - Tell if a library is loaded or opened *)
 val library_is_loaded : dir_path -> bool
 val library_is_opened : dir_path -> bool
 
+  (* - Tell which libraries are loaded or imported *)
 val loaded_libraries : unit -> dir_path list
 val opened_libraries : unit -> dir_path list
 
-val fmt_libraries_state : unit -> Pp.std_ppcmds
-
-(*s Require. The command [require_library spec m file export] loads and opens
-  a library [m]. [file] specifies the filename, if not [None]. [spec]
-  specifies to look for a specification ([true]) or for an implementation
-  ([false]), if not [None]. And [export] specifies if the library must be 
-  exported. *)
-
-val require_library :
-  bool option -> qualid located list -> bool -> unit
-
-val require_library_from_file :
-  bool option -> identifier option -> System.physical_path -> bool -> unit
-
-val set_xml_require : (dir_path -> unit) -> unit
-
-(*s [save_library_to s f] saves the current environment as a library [s]
-  in the file [f]. *)
-
-val start_library : string -> dir_path * string
-val save_library_to : dir_path -> string -> unit
-
-(* [library_full_filename] returns the full filename of a loaded library. *)
-
+  (* - Return the full filename of a loaded library. *)
 val library_full_filename : dir_path -> string
 
+(*s Hook for the xml exportation of libraries *)
+val set_xml_require : (dir_path -> unit) -> unit
 
-(*s Global load path *)
-type logical_path = dir_path
+(*s Global load paths: a load path is a physical path in the file
+    system; to each load path is associated a Coq [dir_path] (the "logical"
+    path of the physical path) *)
 
-val get_load_path : unit -> System.physical_path list
-val get_full_load_path : unit -> (System.physical_path * logical_path) list
-val add_load_path_entry : System.physical_path * logical_path -> unit
-val remove_path : System.physical_path -> unit
-val find_logical_path : System.physical_path -> logical_path
-val load_path_of_logical_path : dir_path -> System.physical_path list
+val get_load_paths : unit -> System.physical_path list
+val get_full_load_paths : unit -> (System.physical_path * dir_path) list
+val add_load_path : System.physical_path * dir_path -> unit
+val remove_load_path : System.physical_path -> unit
+val find_logical_path : System.physical_path -> dir_path
+val load_paths_of_dir_path : dir_path -> System.physical_path list
 
+(*s Locate a library in the load paths *)
 exception LibUnmappedDir
 exception LibNotFound
 type library_location = LibLoaded | LibInPath
@@ -81,14 +74,5 @@ type library_location = LibLoaded | LibInPath
 val locate_qualified_library :
   qualid -> library_location * dir_path * System.physical_path
 
-
-val check_required_library : string list -> unit
-
-(*s Displays the memory use of a library. *)
+(*s Statistics: display the memory use of a library. *)
 val mem : dir_path -> Pp.std_ppcmds
-
-(* For discharge *)
-type library_reference
-
-val out_require : Libobject.obj -> library_reference
-val reload_library : library_reference -> unit
diff --git a/library/nameops.ml b/library/nameops.ml
index 35b707a7..6db5f75d 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nameops.ml,v 1.21.2.2 2004/10/12 10:12:31 herbelin Exp $ *)
+(* $Id: nameops.ml 6205 2004-10-12 10:13:15Z herbelin $ *)
 
 open Pp
 open Util
@@ -16,6 +16,10 @@ open Names
 
 let pr_id id = str (string_of_id id)
 
+let pr_name = function
+  | Anonymous -> str "_"
+  | Name id -> pr_id id
+
 let wildcard = id_of_string "_"
 
 (* Utilities *)
diff --git a/library/nameops.mli b/library/nameops.mli
index 71dbf040..9d1722d4 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -6,12 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: nameops.mli,v 1.12.2.3 2005/01/21 17:14:10 herbelin Exp $ i*)
+(*i $Id: nameops.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
 
 open Names
 
 (* Identifiers and names *)
 val pr_id : identifier -> Pp.std_ppcmds
+val pr_name : name -> Pp.std_ppcmds
+
 val wildcard : identifier
 
 val make_ident : string -> int option -> identifier
diff --git a/library/nametab.ml b/library/nametab.ml
old mode 100755
new mode 100644
index 4bd0cb3f..96280e8b
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nametab.ml,v 1.48.2.2 2005/11/21 09:16:27 herbelin Exp $ *)
+(* $Id: nametab.ml 8642 2006-03-17 10:09:02Z notin $ *)
 
 open Util
 open Pp
@@ -96,7 +96,7 @@ struct
      [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*)
 
   let rec push_until uname o level (current,dirmap) = function
-    | modid :: path as dir ->
+    | modid :: path ->
 	let mc = 
 	  try ModIdmap.find modid dirmap
 	  with Not_found -> (Nothing, ModIdmap.empty)
@@ -135,7 +135,7 @@ struct
 
 
 let rec push_exactly uname o level (current,dirmap) = function
-  | modid :: path as dir ->
+  | modid :: path ->
       let mc = 
 	try ModIdmap.find modid dirmap
 	with Not_found -> (Nothing, ModIdmap.empty)
diff --git a/library/nametab.mli b/library/nametab.mli
index 4cea1d40..a05b7415 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,v 1.43.2.3 2005/11/21 09:16:27 herbelin Exp $ i*)
+(*i $Id: nametab.mli 7596 2005-11-21 09:17:07Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/library/states.ml b/library/states.ml
index 7a7f1e06..3bb37a4d 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: states.ml,v 1.8.14.1 2004/07/16 19:30:36 herbelin Exp $ *)
+(* $Id: states.ml 6692 2005-02-06 13:03:51Z herbelin $ *)
 
 open System
 
@@ -24,7 +24,7 @@ let state_magic_number = 19764
 let (extern_state,intern_state) =
   let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in
   (fun s -> raw_extern s (get_state())),
-  (fun s -> set_state (raw_intern (Library.get_load_path ()) s))
+  (fun s -> set_state (raw_intern (Library.get_load_paths ()) s))
 
 (* Rollback. *)
 
diff --git a/library/states.mli b/library/states.mli
index 70018180..eff046ef 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: states.mli,v 1.6.16.1 2004/07/16 19:30:36 herbelin Exp $ i*)
+(*i $Id: states.mli 5920 2004-07-16 20:01:26Z herbelin $ 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
diff --git a/library/summary.ml b/library/summary.ml
index fc88350a..455ee264 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: summary.ml,v 1.7.2.1 2004/07/16 19:30:36 herbelin Exp $ *)
+(* $Id: summary.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/library/summary.mli b/library/summary.mli
index 7e691f0b..ba527bdf 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,v 1.8.2.1 2004/07/16 19:30:36 herbelin Exp $ i*)
+(*i $Id: summary.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* This module registers the declaration of global tables, which will be kept
    in synchronization during the various backtracks of the system. *)
-- 
cgit v1.2.3