Imported Upstream version 8.0pl1upstream/8.0pl1

30 files changed, 6321 insertions, 0 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
new file mode 100644
index 00000000..a030284c
--- /dev/null
+++ b/library/decl_kinds.ml
@@ -0,0 +1,75 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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 $ *)
+
+(* Informal mathematical status of declarations *)
+
+type locality_flag = (*bool (* local = true; global = false *)*)
+  | Local
+  | Global
+
+(* Kinds used at parsing time *)
+
+type theorem_kind =
+  | Theorem
+  | Lemma
+  | Fact
+  | Remark
+
+type definition_object_kind =
+  | Definition
+  | Coercion
+  | SubClass
+  | CanonicalStructure
+
+type strength = locality_flag (* For compatibility *)
+
+type type_as_formula_kind = Definitional | Logical | Conjectural
+
+(* [assumption_kind] 
+
+                |  Local      | Global
+   ------------------------------------
+   Definitional |  Variable   | Parameter
+   Logical      |  Hypothesis | Axiom
+
+*)
+type assumption_kind = locality_flag * type_as_formula_kind
+
+type definition_kind = locality_flag * definition_object_kind
+
+(* Kinds used in proofs *)
+
+type global_goal_kind =
+  | DefinitionBody
+  | Proof of theorem_kind
+
+type goal_kind =
+  | IsGlobal of global_goal_kind
+  | IsLocal
+
+(* 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
+
+(* Utils *)
+
+let theorem_kind_of_goal_kind = function
+  | DefinitionBody -> IsDefinition
+  | Proof s -> IsProof s
+
diff --git a/library/declare.ml b/library/declare.ml
new file mode 100644
index 00000000..8b9dfeda
--- /dev/null
+++ b/library/declare.ml
@@ -0,0 +1,402 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: declare.ml,v 1.128.2.1 2004/07/16 19:30:34 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Libnames
+open Nameops
+open Term
+open Sign
+open Declarations
+open Entries
+open Inductive
+open Indtypes
+open Reduction
+open Type_errors
+open Typeops
+open Libobject
+open Lib
+open Impargs
+open Nametab
+open Safe_typing
+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] *)
+
+open Nametab
+
+let strength_min (stre1,stre2) =
+  if stre1 = Local or stre2 = Local then Local else Global
+
+let string_of_strength = function
+  | Local -> "(local)"
+  | 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 if_xml f x = if !Options.xml_export then f x else ()
+
+let set_xml_declare_variable f = xml_declare_variable := if_xml f
+let set_xml_declare_constant f = xml_declare_constant := if_xml f
+let set_xml_declare_inductive f = xml_declare_inductive := if_xml f
+
+(* Section variables. *)
+
+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 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
+
+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))) =
+  (* Constr raisonne sur les noms courts *)
+  if Idmap.mem id !vartab then
+    errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
+  let vd = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum ty ->
+        let cst = Global.push_named_assum (id,ty) in
+        let (_,bd,ty) = Global.lookup_named id in
+        CheckedSectionLocalAssum (ty,cst)
+    | SectionLocalDef (c,t,opaq) -> 
+        let cst = Global.push_named_def (id,c,t) in
+        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);
+  vartab := Idmap.add id (p,vd,mk) !vartab
+
+let (in_variable, out_variable) =
+  declare_object { (default_object "VARIABLE") with
+    cache_function = cache_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
+  !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
+
+let csttab = ref (Spmap.empty : global_kind Spmap.t)
+
+let _ = Summary.declare_summary "CONSTANT"
+	  { Summary.freeze_function = (fun () -> !csttab);
+	    Summary.unfreeze_function = (fun ft -> csttab := ft);
+	    Summary.init_function = (fun () -> csttab := Spmap.empty);
+	    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)
+
+(* Opening means making the name without its module qualification available *)
+let open_constant i ((sp,kn),_) =
+  Nametab.push (Nametab.Exactly i) sp (ConstRef kn)
+
+(* 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 export_constant cst = Some (dummy_constant cst)
+
+let classify_constant (_,cst) = Substitute (dummy_constant cst)
+
+let (in_constant, out_constant) =
+  declare_object { (default_object "CONSTANT") with
+    cache_function = cache_constant;
+    load_function = load_constant;
+    open_function = open_constant;
+    classify_function = classify_constant;
+    subst_function = ident_subst_function;
+    export_function = export_constant } 
+
+let hcons_constant_declaration = function
+  | DefinitionEntry ce ->
+      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 }
+  | 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_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 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 inductive_names sp kn mie =
+  let (dp,_) = repr_path sp in
+  let names, _ = 
+    List.fold_left
+      (fun (names, n) ind ->
+	 let ind_p = (kn,n) in
+	 let names, _ =
+	   List.fold_left
+	     (fun (names, p) l ->
+		let sp = 
+		  Libnames.make_path dp l
+		in
+		  ((sp, ConstructRef (ind_p,p)) :: names, p+1))
+	     (names, 1) ind.mind_entry_consnames in
+	 let sp = Libnames.make_path dp ind.mind_entry_typename
+	 in
+	   ((sp, IndRef ind_p) :: names, n+1))
+      ([], 0) mie.mind_entry_inds
+  in names
+
+
+let check_exists_inductive (sp,_) =
+  (if Idmap.mem (basename sp) !vartab then
+    errorlabstrm "cache_inductive" 
+      (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")
+
+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 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 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 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;
+  mind_entry_lc = []
+}
+
+(* Hack to reduce the size of .vo: we keep only what load/open needs *)
+let dummy_inductive_entry m = {
+  mind_entry_finite = true;
+  mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }
+
+let export_inductive x = Some (dummy_inductive_entry x)
+
+let (in_inductive, out_inductive) =
+  declare_object {(default_object "INDUCTIVE") with 
+    cache_function = cache_inductive;
+    load_function = load_inductive;
+    open_function = open_inductive;
+    classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a));
+    subst_function = ident_subst_function;
+    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 [] ;
+  !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 = 
+  try let _ = Spmap.find sp !csttab in true with Not_found -> false
+
+let constant_strength sp = Global
+let constant_kind sp = Spmap.find sp !csttab
+
+let get_variable id = 
+  let (p,x,_) = Idmap.find id !vartab in
+  match x with
+    | 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 =
+  let (p,_,_) = Idmap.find id !vartab in Libnames.make_path p id
+
+let variable_opacity id =
+  let (_,x,_) = Idmap.find id !vartab in
+  match x with
+    | CheckedSectionLocalDef (c,ty,cst,opaq) -> opaq
+    | CheckedSectionLocalAssum (ty,cst) -> false (* any.. *)
+
+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
+
+(* Global references. *)
+
+let first f v =
+  let n = Array.length v in
+  let rec look_for i =
+    if i = n then raise Not_found;
+    try f i v.(i) with Not_found -> look_for (succ i)
+  in
+  look_for 0
+
+let mind_oper_of_id sp id mib =
+  first
+    (fun tyi mip ->
+       if id = mip.mind_typename then 
+	 IndRef (sp,tyi)
+       else
+	 first 
+	   (fun cj cid -> 
+	      if id = cid then 
+		ConstructRef ((sp,tyi),succ cj) 
+	      else raise Not_found) 
+	   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 ->
+      try
+        let (p,_,_) = Idmap.find id !vartab in
+        if dir=p then id::sec_ids else sec_ids
+      with Not_found -> sec_ids)
+    (Environ.named_context (Global.env()))
+    ~init:[]
+
+let is_section_variable = function
+  | VarRef _ -> true
+  | _ -> false
+
+let strength_of_global = function
+  | VarRef _ -> Local
+  | IndRef _ | ConstructRef _ | ConstRef _ -> Global
diff --git a/library/declare.mli b/library/declare.mli
new file mode 100644
index 00000000..968be059
--- /dev/null
+++ b/library/declare.mli
@@ -0,0 +1,102 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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*)
+open Names
+open Libnames
+open Term
+open Sign
+open Declarations
+open Entries
+open Indtypes
+open Safe_typing
+open Nametab
+open Decl_kinds
+(*i*)
+
+(* This module provides the official functions to declare new variables, 
+   parameters, constants and inductive types. Using the following functions
+   will add the entries in the global environment (module [Global]), will
+   register the declarations in the library (module [Lib]) --- so that the
+   reset works properly --- and will fill some global tables such as 
+   [Nametab] and [Impargs]. *)
+
+open Nametab
+
+(* Declaration of local constructions (Variable/Hypothesis/Local) *)
+
+type section_variable_entry =
+  | SectionLocalDef of constr * types option * bool (* opacity *)
+  | SectionLocalAssum of types
+
+type variable_declaration = dir_path * section_variable_entry * local_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
+
+(* [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_internal_constant :
+  identifier -> constant_declaration -> object_name
+
+val redeclare_constant :
+ identifier -> Dischargedhypsmap.discharged_hyps -> 
+      Cooking.recipe * global_kind -> unit
+
+(* [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
+
+(*s Corresponding test and access functions. *)
+
+val is_constant : section_path -> bool
+val constant_strength : section_path -> strength
+val constant_kind : section_path -> global_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 find_section_variable : variable -> section_path
+val last_section_hyps : dir_path -> identifier list
+val clear_proofs : named_context -> named_context
+
+(*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_inductive : (bool * object_name -> unit) -> unit
diff --git a/library/declaremods.ml b/library/declaremods.ml
new file mode 100644
index 00000000..b968a432
--- /dev/null
+++ b/library/declaremods.ml
@@ -0,0 +1,820 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: declaremods.ml,v 1.18.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+
+open Pp
+open Util
+open Names
+open Declarations
+open Entries
+open Libnames
+open Libobject
+open Lib
+open Nametab
+
+(* modules and components *)
+
+
+(* This type is a functional closure of substitutive lib_objects.
+
+   The first part is a partial substitution (which will be later
+   applied to lib_objects when completed).
+
+   The second one is a list of bound identifiers which is nonempty
+   only if the objects are owned by a fuctor
+
+   The third one is the "self" ident of the signature (or structure),
+   which should be substituted in lib_objects with the real name of
+   the module.
+
+   The fourth one is the segment itself which can contain references
+   to identifiers in the domain of the substitution or in other two
+   parts. These references are invalid in the current scope and
+   therefore must be substitued with valid names before use.
+
+*)
+type substitutive_objects = 
+    substitution * mod_bound_id list * mod_self_id * lib_objects
+
+
+(* For each module, we store the following things:
+
+   In modtab_substobjs: substitutive_objects 
+     when we will do Module M:=N, the objects of N will be reloaded 
+     with M after substitution
+
+   In modtab_objects: "substituted objects" @ "keep objects"
+
+   substituted objects - 
+     roughly the objects above after the substitution - we need to 
+     keep them to call open_object when the module is opened (imported)
+ 
+   keep objects -
+     The list of non-substitutive objects - as above, for each of 
+     them we will call open_object when the module is opened 
+     
+   (Some) Invariants:
+   * If the module is a functor, the two latter lists are empty.
+
+   * Module objects in substitutive_objects part have empty substituted 
+     objects.
+
+   * Modules which where created with Module M:=mexpr or with 
+     Module M:SIG. ... End M. have the keep list empty.
+*)
+let modtab_substobjs = 
+  ref (MPmap.empty : substitutive_objects MPmap.t)
+let modtab_objects = 
+  ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t)
+
+
+(* currently started interactive module (if any) - its arguments (if it
+   is a functor) and declared output type *)
+let openmod_info = 
+  ref (([],None,None) : mod_bound_id list * module_type_entry option 
+                                          * module_type_body option) 
+
+let _ = Summary.declare_summary "MODULE-INFO"
+	  { Summary.freeze_function = (fun () -> 
+					 !modtab_substobjs,
+					 !modtab_objects,
+					 !openmod_info);
+	    Summary.unfreeze_function = (fun (sobjs,objs,info) -> 
+					   modtab_substobjs := sobjs;
+					   modtab_objects := objs;
+					   openmod_info := info);
+	    Summary.init_function = (fun () -> 
+				       modtab_substobjs := MPmap.empty;
+				       modtab_objects := MPmap.empty;
+				       openmod_info := ([],None,None));
+	    Summary.survive_module = false;
+	    Summary.survive_section = false }
+
+(* auxiliary functions to transform section_path and kernel_name given
+   by Lib into module_path and dir_path needed for modules *)
+
+let mp_of_kn kn = 
+  let mp,sec,l = repr_kn kn in 
+    if sec=empty_dirpath then 
+      MPdot (mp,l) 
+    else
+      anomaly ("Non-empty section in module name!" ^ string_of_kn kn)
+
+let dir_of_sp sp = 
+  let dir,id = repr_path sp in
+    extend_dirpath dir id
+
+let msid_of_mp = function
+    MPself msid -> msid
+  | _ -> anomaly "'Self' module path expected!"
+
+let msid_of_prefix (_,(mp,sec)) = 
+  if sec=empty_dirpath then 
+    msid_of_mp mp
+  else
+    anomaly ("Non-empty section in module name!" ^ 
+	     string_of_mp mp ^ "." ^ string_of_dirpath sec)
+
+
+(* This function checks if the type calculated for the module [mp] is
+   a subtype of [sub_mtb]. Uses only the global environment. *)
+let check_subtypes mp sub_mtb =
+  let env = Global.env () in
+  let mtb = (Environ.lookup_module mp env).mod_type in
+  let _ = Environ.add_constraints 
+	    (Subtyping.check_subtypes env mtb sub_mtb) 
+  in
+    ()  (* The constraints are checked and forgot immediately! *) 
+
+
+(* This function registers the visibility of the module and iterates
+   through its components. It is called by plenty module functions *)
+
+let do_module exists what iter_objects i dir mp substobjs objects =
+  let prefix = (dir,(mp,empty_dirpath)) in
+  let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
+  let vis = 
+    if exists then 
+      if 
+	try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo 
+	with Not_found -> false 
+      then
+	Nametab.Exactly i
+      else
+	errorlabstrm (what^"_module") 
+	  (pr_dirpath dir ++ str " should already exist!") 
+    else
+      if Nametab.exists_dir dir then
+	errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
+      else
+	Nametab.Until i
+  in
+    Nametab.push_dir vis dir dirinfo;
+    modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
+    match objects with
+	Some seg -> 
+	  modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects;
+	  iter_objects (i+1) prefix seg	  
+      | None ->  ()
+
+    
+let conv_names_do_module exists what iter_objects i 
+      (sp,kn) substobjs substituted =
+  let dir,mp = dir_of_sp sp, mp_of_kn kn in
+  do_module exists what iter_objects i dir mp substobjs substituted
+
+(* Interactive modules and module types cannot be recached! cache_mod*
+   functions can be called only once (and "end_mod*" set the flag to
+   false then)
+*)
+
+let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) =
+  let _ = match entry with
+    | None ->
+	anomaly "You must not recache interactive modules!"
+    | Some (me,sub_mte_o) ->
+	let sub_mtb_o = match sub_mte_o with 
+	    None -> None
+	  | Some mte -> Some (Mod_typing.translate_modtype (Global.env()) mte)
+	in
+
+	let mp = Global.add_module (basename sp) me in
+	if mp <> mp_of_kn kn then
+	  anomaly "Kernel and Library names do not match";
+	  
+	match sub_mtb_o with
+	    None -> ()
+	  | Some sub_mtb -> check_subtypes mp sub_mtb
+
+  in
+  conv_names_do_module false "cache" load_objects 1 oname substobjs substituted
+
+
+(* TODO: This check is not essential *)
+let check_empty s = function
+     | None -> ()
+     | Some _ -> 
+	 anomaly ("We should never have full info in " ^ s^"!")
+
+
+(* When this function is called the module itself is already in the
+   environment. This function loads its objects only *)
+
+let load_module i (oname,(entry,substobjs,substituted)) =
+  (* TODO: This check is not essential *)
+  check_empty "load_module" entry;
+  conv_names_do_module false "load" load_objects i oname substobjs substituted
+
+
+let open_module i (oname,(entry,substobjs,substituted)) =
+  (* TODO: This check is not essential *)
+  check_empty "open_module" entry;
+  conv_names_do_module true "open" open_objects i oname substobjs substituted
+
+
+let subst_substobjs dir mp (subst,mbids,msid,objs) =
+  match mbids with
+    | [] -> 
+	let prefix = dir,(mp,empty_dirpath) in
+	  Some (subst_objects prefix (add_msid msid mp subst) objs)
+    | _ -> None
+
+
+let subst_module ((sp,kn),subst,(entry,substobjs,_)) =
+  check_empty "subst_module" entry;
+  let dir,mp = dir_of_sp sp, mp_of_kn kn in
+  let (sub,mbids,msid,objs) = substobjs in
+  let subst' = join sub subst in
+  (* substitutive_objects get the new substitution *)
+  let substobjs = (subst',mbids,msid,objs) in
+  (* if we are not a functor - calculate substitued.
+     We add "msid |-> mp" to the substitution *)
+  let substituted = subst_substobjs dir mp substobjs
+  in
+    (None,substobjs,substituted)
+
+
+let classify_module (_,(_,substobjs,_)) =
+  Substitute (None,substobjs,None)
+
+let (in_module,out_module) =
+  declare_object {(default_object "MODULE") with
+    cache_function = cache_module;
+    load_function = load_module;
+    open_function = open_module;
+    subst_function = subst_module;
+    classify_function = classify_module;
+    export_function = (fun _ -> anomaly "No modules in sections!") }
+
+
+let cache_keep _ = anomaly "This module should not be cached!"
+
+let load_keep i ((sp,kn),seg) = 
+  let mp = mp_of_kn kn in
+  let prefix = dir_of_sp sp, (mp,empty_dirpath) in
+    begin 
+      try
+	let prefix',objects = MPmap.find mp !modtab_objects in
+	  if prefix' <> prefix then 
+	    anomaly "Two different modules with the same path!";
+	  modtab_objects := MPmap.add mp (prefix,objects@seg) !modtab_objects;
+      with
+	  Not_found -> anomaly "Keep objects before substitutive"
+    end;
+    load_objects i prefix seg
+
+let open_keep i ((sp,kn),seg) = 
+  let dirpath,mp = dir_of_sp sp, mp_of_kn kn in
+    open_objects i (dirpath,(mp,empty_dirpath)) seg
+
+let (in_modkeep,out_modkeep) = 
+  declare_object {(default_object "MODULE KEEP OBJECTS") with
+    cache_function = cache_keep;
+    load_function = load_keep;
+    open_function = open_keep;
+    export_function = (fun _ -> anomaly "No modules in sections!") }
+
+(* we remember objects for a module type. In case of a declaration:
+   Module M:SIG:=...
+   The module M gets its objects from SIG
+*)
+let modtypetab =
+  ref (KNmap.empty : substitutive_objects KNmap.t)
+
+(* currently started interactive module type. We remember its arguments
+   if it is a functor type *)
+let openmodtype_info =
+  ref ([] : mod_bound_id list)
+
+let _ = Summary.declare_summary "MODTYPE-INFO"
+	  { Summary.freeze_function = (fun () ->
+					 !modtypetab,!openmodtype_info);
+	    Summary.unfreeze_function = (fun ft ->
+					   modtypetab := fst ft;
+					   openmodtype_info := snd ft);
+	    Summary.init_function = (fun () ->
+				       modtypetab := KNmap.empty;
+				       openmodtype_info := []);
+	    Summary.survive_module = false;
+	    Summary.survive_section = true }
+
+
+
+
+let cache_modtype ((sp,kn),(entry,modtypeobjs)) =
+  let _ = 
+    match entry with
+      | None ->
+	  anomaly "You must not recache interactive module types!"
+      | Some mte ->
+	  let kn' = Global.add_modtype (basename sp) mte in
+	  if kn' <> kn then
+	    anomaly "Kernel and Library names do not match"
+  in
+
+  if Nametab.exists_modtype sp then
+    errorlabstrm "cache_modtype"
+      (pr_sp sp ++ str " already exists") ;
+
+  Nametab.push_modtype (Nametab.Until 1) sp kn;
+
+  modtypetab := KNmap.add kn modtypeobjs !modtypetab
+
+
+let load_modtype i ((sp,kn),(entry,modtypeobjs)) =
+  check_empty "load_modtype" entry;
+
+  if Nametab.exists_modtype sp then
+    errorlabstrm "cache_modtype"
+      (pr_sp sp ++ str " already exists") ;
+
+  Nametab.push_modtype (Nametab.Until i) sp kn;
+    
+  modtypetab := KNmap.add kn modtypeobjs !modtypetab
+
+
+let open_modtype i ((sp,kn),(entry,_)) =
+  check_empty "open_modtype" entry;
+
+  if 
+    try Nametab.locate_modtype (qualid_of_sp sp) <> kn 
+    with Not_found -> true
+  then
+    errorlabstrm ("open_modtype") 
+      (pr_sp sp ++ str " should already exist!");
+
+  Nametab.push_modtype (Nametab.Exactly i) sp kn
+
+
+let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) =
+  check_empty "subst_modtype" entry;
+  (entry,(join subs subst,mbids,msid,objs))
+
+
+let classify_modtype (_,(_,substobjs)) =
+  Substitute (None,substobjs)
+
+
+let (in_modtype,out_modtype) =
+    declare_object {(default_object "MODULE TYPE") with
+      cache_function = cache_modtype;
+      open_function = open_modtype;
+      load_function = load_modtype;
+      subst_function = subst_modtype;
+      classify_function = classify_modtype;
+      export_function = in_some }
+
+
+
+let replace_module_object id (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' ->
+	  if object_tag obj = "MODULE" then
+	    (id, in_module (None,modobjs,None))::tail
+	  else error "MODULE expected!"
+      | lobj::tail -> lobj::replace_id tail
+    in
+      (subst, mbids, msid, replace_id lib_stack)
+
+let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) =
+  (subst, mbids1@mbids2, msid, lib_stack)
+
+
+let rec get_modtype_substobjs = function
+    MTEident ln -> KNmap.find ln !modtypetab
+  | MTEfunsig (mbid,_,mte) ->
+      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)) -> 
+      let substobjs = get_modtype_substobjs mty in
+      let modobjs = MPmap.find mp !modtab_substobjs in
+	replace_module_object id substobjs modobjs
+  | MTEsig (msid,_) -> 
+      todo "Anonymous module types"; (empty_subst, [], msid, [])
+
+(* push names of bound modules (and their components) to Nametab *)
+(* add objects associated to them *)
+let process_module_bindings argids args =
+  let process_arg id (mbid,mty) =
+    let dir = make_dirpath [id] in
+    let mp = MPbound mbid in
+    let substobjs = get_modtype_substobjs mty in
+    let substituted = subst_substobjs dir mp substobjs in
+      do_module false "start" load_objects 1 dir mp substobjs substituted
+  in
+    List.iter2 process_arg argids args
+
+
+let replace_module mtb id mb = todo "replace module after with"; mtb 
+
+let rec get_some_body mty env = match mty with
+    MTEident kn -> Environ.lookup_modtype kn env 
+  | MTEfunsig _ 
+  | MTEsig _ -> anomaly "anonymous module types not supported"
+  | MTEwith (mty,With_Definition _) -> get_some_body mty env 
+  | MTEwith (mty,With_Module (id,mp)) -> 
+      replace_module (get_some_body mty env) id (Environ.lookup_module mp env)
+
+
+let intern_args interp_modtype (env,oldargs) (idl,arg) = 
+  let lib_dir = Lib.library_dp() in
+  let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
+  let mty = interp_modtype env arg in
+  let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
+  let mps = List.map (fun mbid -> MPbound mbid) mbids in
+  let substobjs = get_modtype_substobjs mty in
+  let substituted's = 
+    List.map2 
+      (fun dir mp -> dir, mp, subst_substobjs dir mp substobjs) 
+      dirs mps  
+  in
+    List.iter 
+      (fun (dir, mp, substituted) -> 
+	 do_module false "interp" load_objects 1 dir mp substobjs substituted)
+      substituted's;
+    let body = Modops.module_body_of_type (get_some_body mty env) in
+    let env = 
+      List.fold_left (fun env mp -> Modops.add_module mp body env) env mps
+    in
+    env, List.map (fun mbid -> mbid,mty) mbids :: oldargs
+      
+let start_module interp_modtype id args res_o =
+  let fs = Summary.freeze_summaries () in
+  let env = Global.env () in
+  let env,arg_entries_revlist = 
+    List.fold_left (intern_args interp_modtype) (env,[]) args 
+  in
+  let arg_entries = List.concat (List.rev arg_entries_revlist) in
+
+  let res_entry_o, sub_body_o = match res_o with
+      None -> None, None
+    | Some (res, true) ->
+	Some (interp_modtype env res), None
+    | Some (res, false) ->
+	(* If the module type is non-restricting, we must translate it
+	   here to catch errors as early as possible. If it is
+	   estricting, the kernel takes care of it.  *)
+	let sub_mte = 
+	  List.fold_right 
+	    (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+	    arg_entries 
+	    (interp_modtype env res)
+	in
+	let sub_mtb = 
+	  Mod_typing.translate_modtype (Global.env()) sub_mte
+	in
+	  None, Some sub_mtb
+  in
+
+  let mp = Global.start_module id arg_entries res_entry_o in
+
+  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
+  Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
+  Lib.add_frozen_state ()
+
+
+let end_module id =
+
+  let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in
+  let mp = Global.end_module id in
+  let mbids, res_o, sub_o = !openmod_info in
+    
+  begin match sub_o with
+      None -> ()
+    | Some sub_mtb -> check_subtypes mp sub_mtb
+  end;
+    
+  let substitute, keep, special = Lib.classify_segment lib_stack in
+
+  let dir = fst oldprefix in
+  let msid = msid_of_prefix oldprefix in
+
+  let substobjs = try
+    match res_o with
+      | None -> 
+	  empty_subst, mbids, msid, substitute
+      | Some (MTEident ln) ->
+	  abstract_substobjs mbids (KNmap.find ln (!modtypetab))
+      | Some (MTEsig (msid,_)) ->
+	  todo "Anonymous signatures not supported";
+	  empty_subst, mbids, msid, []
+      | Some (MTEwith _ as mty) ->
+	  abstract_substobjs mbids (get_modtype_substobjs mty)
+      | Some (MTEfunsig _) -> 
+	  anomaly "Funsig cannot be here..."
+    with
+	Not_found -> anomaly "Module objects not found..."
+  in
+
+  (* must be called after get_modtype_substobjs, because of possible
+     dependencies on functor arguments *)
+  Summary.module_unfreeze_summaries fs;
+
+  let substituted = subst_substobjs dir mp substobjs in
+  let node = in_module (None,substobjs,substituted) in
+  let objects = 
+    if keep = [] || mbids <> [] then 
+      special@[node]   (* no keep objects or we are defining a functor *)
+    else
+      special@[node;in_modkeep keep]   (* otherwise *)
+  in
+  let newoname = Lib.add_leaves id objects in
+
+    if (fst newoname) <> (fst oldoname) then
+      anomaly "Names generated on start_ and end_module do not match";
+    if mp_of_kn (snd newoname) <> mp then 
+      anomaly "Kernel and Library names do not match";
+
+    Lib.add_frozen_state () (* to prevent recaching *)
+
+
+
+let module_objects mp = 
+  let prefix,objects = MPmap.find mp !modtab_objects in
+    segment_of_objects prefix objects
+
+
+
+(************************************************************************)
+(* libraries *)
+
+type library_name = dir_path
+
+(* The first two will form substitutive_objects, the last one is keep *)
+type library_objects = 
+    mod_self_id * lib_objects * lib_objects
+
+
+(* The library_cache here is needed to avoid recalculations of
+   substituted modules object during "reloading" of libraries *)
+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);
+      (* if it's in the environment, the cached objects should be correct *)
+      Hashtbl.find library_cache dir
+    with
+	Not_found ->
+	  if mp <> Global.import cenv digest then
+	    anomaly "Unexpected disk module name";
+	  let msid,substitute,keep = objs in
+	  let substobjs = empty_subst, [], msid, substitute in
+	  let substituted = subst_substobjs dir mp substobjs in
+	  let objects = option_app (fun seg -> seg@keep) substituted in
+	  let modobjs = substobjs, objects in
+	    Hashtbl.add library_cache dir modobjs;
+	    modobjs
+  in
+    do_module false "register_library" load_objects 1 dir mp substobjs objects
+
+
+let start_library dir = 
+  let mp = Global.start_library dir in
+  openmod_info:=[],None,None;
+  Lib.start_compilation dir mp;
+  Lib.add_frozen_state ()
+
+
+let end_library dir = 
+  let prefix, lib_stack = Lib.end_compilation dir in
+  let cenv = Global.export dir in
+  let msid = msid_of_prefix prefix in
+  let substitute, keep, _ = Lib.classify_segment lib_stack in
+    cenv,(msid,substitute,keep)
+
+
+(* implementation of Export M and Import M *)
+
+
+let really_import_module mp = 
+  let prefix,objects = MPmap.find mp !modtab_objects in
+    open_objects 1 prefix objects
+
+
+let cache_import (_,(_,mp)) = 
+(* for non-substitutive exports: 
+  let mp = Nametab.locate_module (qualid_of_dirpath dir) in  *)
+  really_import_module mp
+
+let classify_import (_,(export,_ as obj)) = 
+  if export then Substitute obj else Dispose
+
+let subst_import (_,subst,(export,mp as obj)) =
+  let mp' = subst_mp subst mp in
+    if mp'==mp then obj else
+      (export,mp')
+
+let (in_import,out_import) = 
+  declare_object {(default_object "IMPORT MODULE") with
+    cache_function = cache_import;
+    open_function = (fun i o -> if i=1 then cache_import o);
+    subst_function = subst_import;
+    classify_function = classify_import }
+
+
+let import_module export mp = 
+  Lib.add_anonymous_leaf (in_import (export,mp))
+
+(************************************************************************)
+(* module types *)
+
+let start_modtype interp_modtype id args =
+  let fs = Summary.freeze_summaries () in
+  let env = Global.env () in
+  let env,arg_entries_revlist = 
+    List.fold_left (intern_args interp_modtype) (env,[]) args 
+  in
+  let arg_entries = List.concat (List.rev arg_entries_revlist) in
+
+  let mp = Global.start_modtype id arg_entries in
+
+  let mbids = List.map fst arg_entries in
+  openmodtype_info := mbids;
+  let prefix = Lib.start_modtype id mp fs in
+  Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
+  Lib.add_frozen_state ()
+
+
+let end_modtype id =
+
+  let oldoname,prefix,fs,lib_stack = Lib.end_modtype id in
+  let ln = Global.end_modtype id in
+  let substitute, _, special = Lib.classify_segment lib_stack in
+
+  let msid = msid_of_prefix prefix in
+  let mbids = !openmodtype_info in
+
+  Summary.module_unfreeze_summaries fs;
+
+  let modtypeobjs = empty_subst, mbids, msid, substitute in
+
+  let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs)]) in
+  if fst oname <> fst oldoname then
+    anomaly
+      "Section paths generated on start_ and end_modtype do not match";
+  if snd oname <> ln then
+    anomaly
+      "Kernel and Library names do not match";
+
+  Lib.add_frozen_state ()(* to prevent recaching *)
+
+
+let declare_modtype interp_modtype id args mty = 
+  let fs = Summary.freeze_summaries () in
+  let env = Global.env () in
+  let env,arg_entries_revlist = 
+    List.fold_left (intern_args interp_modtype) (env,[]) args 
+  in
+  let arg_entries = List.concat (List.rev arg_entries_revlist) in
+  let base_mty = interp_modtype env mty in
+  let entry = 
+    List.fold_right 
+      (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+      arg_entries
+      base_mty
+  in
+  let substobjs = get_modtype_substobjs entry in
+  Summary.unfreeze_summaries fs;
+    
+  ignore (add_leaf id (in_modtype (Some entry, substobjs)))
+			       
+
+
+let rec get_module_substobjs = function
+  | MEident mp -> MPmap.find mp !modtab_substobjs 
+  | MEfunctor (mbid,mty,mexpr) ->
+      let (subst, mbids, msid, objs) = 
+	get_module_substobjs 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
+	(match mbids with
+	   | mbid::mbids ->
+	       (add_mbid mbid mp subst, mbids, msid, objs)
+	   | [] -> match mexpr with
+	       | MEident _ | MEstruct _ -> error "Application of a non-functor"
+	       | _ -> error "Application of a functor with too few arguments")
+  | MEapply (_,mexpr) ->
+      Modops.error_application_to_not_path mexpr
+
+
+let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
+
+  let fs = Summary.freeze_summaries () in
+  let env = Global.env () in
+  let env,arg_entries_revlist = 
+    List.fold_left (intern_args interp_modtype) (env,[]) args 
+  in
+  let arg_entries = List.concat (List.rev arg_entries_revlist) in
+  let mty_entry_o, mty_sub_o = match mty_o with
+      None -> None, None
+    | (Some (mty, true)) -> 
+	Some (List.fold_right 
+		(fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+		arg_entries 
+		(interp_modtype env mty)), 
+	None
+    | (Some (mty, false)) -> 
+	None, 
+	Some (List.fold_right 
+		(fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+		arg_entries 
+		(interp_modtype env mty))
+  in
+  let mexpr_entry_o = match mexpr_o with
+      None -> None
+    | Some mexpr -> 
+	Some (List.fold_right 
+		(fun (mbid,mte) me -> MEfunctor(mbid,mte,me))
+		arg_entries
+		(interp_modexpr env mexpr))
+  in
+  let entry = 
+    {mod_entry_type = mty_entry_o;	    
+     mod_entry_expr = mexpr_entry_o }
+  in
+  let substobjs =
+    match entry with
+      | {mod_entry_type = Some mte} -> get_modtype_substobjs mte
+      | {mod_entry_expr = Some mexpr} -> get_module_substobjs mexpr
+      | _ -> anomaly "declare_module: No type, no body ..."
+  in
+    Summary.unfreeze_summaries fs;
+
+    let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
+    let substituted = subst_substobjs dir mp substobjs in
+
+      ignore (add_leaf
+		id
+		(in_module (Some (entry, mty_sub_o), substobjs, substituted)))
+
+
+(*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 _ = 
+    MPmap.iter 
+      (fun _ (prefix,objects) -> 
+	 let apply_obj (id,obj) = f (make_oname prefix id) obj in
+	   List.iter apply_obj objects)
+      !modtab_objects
+  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 "[]"
+    | l -> str ("[." ^ string_of_int (List.length l) ^ ".]")
+  in
+  let pr_modinfo mp (prefix,objects) s =
+    s ++ str (string_of_mp mp) ++ (spc ())
+    ++ (pr_seg (segment_of_objects prefix objects))
+  in
+  let modules = MPmap.fold pr_modinfo !modtab_objects (mt ()) in
+    hov 0 modules
+
+
diff --git a/library/declaremods.mli b/library/declaremods.mli
new file mode 100644
index 00000000..f229da1e
--- /dev/null
+++ b/library/declaremods.mli
@@ -0,0 +1,116 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: declaremods.mli,v 1.8.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+
+(*i*)
+open Util
+open Names
+open Entries
+open Environ
+open Libnames
+open Libobject
+open Lib
+   (*i*)
+
+(*s This modules provides official functions to declare modules and
+  module types *)
+
+
+(*s Modules *)
+
+(* [declare_module interp_modtype interp_modexpr id fargs typ expr]
+   declares module [id], with type constructed by [interp_modtype]
+   from functor arguments [fargs] and [typ] and with module body
+   constructed by [interp_modtype] from functor arguments [fargs] and
+   by [interp_modexpr] from [expr]. At least one of [typ], [expr] must
+   be non-empty.
+   
+   The [bool] in [typ] tells if the module must be abstracted [true]
+   with respect to the module type or merely matched without any
+   restriction [false].
+*)
+
+val declare_module : 
+  (env -> 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) ->
+  identifier -> 
+  (identifier located list * 'modtype) list -> ('modtype * bool) option -> 
+  'modexpr option -> unit
+ 
+val start_module : (env -> 'modtype -> module_type_entry) -> 
+  identifier -> 
+  (identifier located list * 'modtype) list -> ('modtype * bool) option -> 
+  unit
+
+val end_module : identifier -> unit
+
+
+
+(*s Module types *)
+
+val declare_modtype : (env -> 'modtype -> module_type_entry) -> 
+  identifier -> (identifier located list * 'modtype) list -> 'modtype -> unit
+
+val start_modtype : (env -> 'modtype -> module_type_entry) -> 
+  identifier -> (identifier located list * 'modtype) list -> unit
+
+val end_modtype : identifier -> unit
+
+
+(*s Objects of a module. They come in two lists: the substitutive ones
+  and the other *)
+
+val module_objects : module_path -> library_segment
+
+
+(*s Libraries i.e. modules on disk *)
+
+type library_name = dir_path
+
+type library_objects
+
+val register_library : 
+  library_name -> 
+    Safe_typing.compiled_library -> library_objects -> Digest.t -> unit
+
+val start_library : library_name -> unit
+
+val end_library :
+  library_name -> Safe_typing.compiled_library * library_objects
+
+
+(* [really_import_module mp] opens the module [mp] (in a Caml sense).
+   It modifies Nametab and performs the "open_object" function for
+   every object of the module. *)
+
+val really_import_module : module_path -> unit
+
+(* [import_module export mp] is a synchronous version of
+   [really_import_module]. If [export] is [true], the module is also
+   opened every time the module containing it is. *)
+
+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. *)
+
+val fold_all_segments : bool -> ('a -> object_name -> obj -> 'a) -> 'a -> 'a
+val iter_all_segments : bool -> (object_name -> obj -> unit) -> unit
+
+
+val debug_print_modtab : unit -> Pp.std_ppcmds
+
+(*val debug_print_modtypetab : unit -> Pp.std_ppcmds*)
+
+(* For translator *)
+val process_module_bindings : module_ident list ->
+  (mod_bound_id * module_type_entry) list -> unit
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
new file mode 100644
index 00000000..59a01d81
--- /dev/null
+++ b/library/dischargedhypsmap.ml
@@ -0,0 +1,60 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: dischargedhypsmap.ml,v 1.3.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+
+open Util
+open Libnames
+open Names
+open Term
+open Reduction
+open Declarations
+open Environ
+open Inductive
+open Libobject
+open Lib
+open Nametab
+
+type discharged_hyps = section_path list
+
+let discharged_hyps_map = ref Spmap.empty
+
+let cache_discharged_hyps_map (_,(sp,hyps)) = 
+  discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
+
+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);
+    export_function = (fun x -> Some x) }
+
+let set_discharged_hyps sp hyps =
+ add_anonymous_leaf (in_discharged_hyps_map (sp,hyps))
+
+let get_discharged_hyps sp =
+  try
+   Spmap.find sp !discharged_hyps_map
+  with Not_found ->
+   anomaly ("No discharged hypothesis for object " ^ string_of_path sp)
+
+(*s Registration as global tables and rollback. *)
+
+let init () =
+  discharged_hyps_map := Spmap.empty
+
+let freeze () = !discharged_hyps_map
+
+let unfreeze dhm = discharged_hyps_map := dhm
+
+let _ = 
+  Summary.declare_summary "discharged_hypothesis"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_module = false;
+      Summary.survive_section = true }
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
new file mode 100644
index 00000000..8851e5a3
--- /dev/null
+++ b/library/dischargedhypsmap.mli
@@ -0,0 +1,24 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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*)
+open Libnames
+open Term
+open Environ
+open Nametab
+(*i*)
+
+type discharged_hyps = section_path list
+
+(*s Discharged hypothesis. Here we store the discharged hypothesis of each *)
+(*  constant or inductive type declaration.                                *)
+
+val set_discharged_hyps : section_path -> discharged_hyps -> unit
+val get_discharged_hyps : section_path -> discharged_hyps
diff --git a/library/doc.tex b/library/doc.tex
new file mode 100644
index 00000000..33af5933
--- /dev/null
+++ b/library/doc.tex
@@ -0,0 +1,16 @@
+
+\newpage
+\section*{The Coq library}
+
+\ocwsection \label{library}
+This chapter describes the \Coq\ library, which is made of two parts:
+\begin{itemize}
+  \item a general mechanism to keep a trace of all operations and of
+    the state of the system, with backtrack capabilities;
+  \item a global environment for the CCI, with functions to export and 
+    import compiled modules.
+\end{itemize}
+The modules of the library are organized as follows.
+
+\bigskip
+\begin{center}\epsfig{file=library.dep.ps}\end{center}
diff --git a/library/global.ml b/library/global.ml
new file mode 100644
index 00000000..bfa9335c
--- /dev/null
+++ b/library/global.ml
@@ -0,0 +1,145 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: global.ml,v 1.43.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+
+open Util
+open Names
+open Term
+open Sign
+open Environ
+open Safe_typing
+open Summary
+
+(* We introduce here the global environment of the system, and we declare it
+   as a synchronized table. *)
+
+let global_env = ref empty_environment
+
+let safe_env () = !global_env
+
+let env () = env_of_safe_env !global_env
+
+let _ = 
+  declare_summary "Global environment"
+    { freeze_function = (fun () -> !global_env);
+      unfreeze_function = (fun fr -> global_env := fr);
+      init_function = (fun () -> global_env := empty_environment);
+      survive_module = true;
+      survive_section = false }
+
+(* Then we export the functions of [Typing] on that environment. *)
+
+let universes () = universes (env())
+let named_context () = named_context (env())
+
+let push_named_assum a =
+  let (cst,env) = push_named_assum a !global_env in
+  global_env := env;
+  cst
+let push_named_def d =
+  let (cst,env) = push_named_def d !global_env in
+  global_env := env;
+  cst
+
+(*let add_thing add kn thing =
+  let _,dir,l = repr_kn kn in
+  let kn',newenv = add dir l thing !global_env in
+    if kn = kn' then
+      global_env := newenv
+    else
+      anomaly "Kernel names do not match."
+*)
+
+let add_thing add dir id thing = 
+  let kn, newenv = add dir (label_of_id id) thing !global_env in
+    global_env := newenv;
+    kn
+
+let add_constant = add_thing add_constant 
+let add_mind = add_thing add_mind
+let add_modtype = add_thing (fun _ -> add_modtype) ()
+let add_module = add_thing (fun _ -> add_module) ()
+
+let add_constraints c = global_env := add_constraints c !global_env
+
+let set_engagement c = global_env := set_engagement c !global_env
+
+let start_module id params mtyo =
+  let l = label_of_id id in
+  let mp,newenv = start_module l params mtyo !global_env in
+    global_env := newenv;
+    mp
+  
+let end_module id =
+  let l = label_of_id id in
+  let mp,newenv = end_module l !global_env in
+    global_env := newenv;
+    mp
+
+
+let start_modtype id params = 
+  let l = label_of_id id in
+  let mp,newenv = start_modtype l params !global_env in
+    global_env := newenv;
+    mp
+
+let end_modtype id =
+  let l = label_of_id id in
+  let kn,newenv = end_modtype l !global_env in
+    global_env := newenv;
+    kn
+
+
+
+
+let lookup_named id = lookup_named id (env())
+let lookup_constant kn = lookup_constant kn (env())
+let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind
+let lookup_mind kn = lookup_mind kn (env())
+
+let lookup_module mp = lookup_module mp (env())
+let lookup_modtype kn = lookup_modtype kn (env())
+
+
+
+
+let start_library dir = 
+  let mp,newenv = start_library dir !global_env in
+    global_env := newenv; 
+    mp
+
+let export s = snd (export !global_env s)
+
+let import cenv digest = 
+  let mp,newenv = import cenv digest !global_env in 
+    global_env := newenv; 
+    mp
+
+
+
+(*s Function to get an environment from the constants part of the global
+    environment and a given context. *)
+
+let env_of_context hyps = 
+  reset_with_named_context hyps (env())
+
+open Libnames
+
+let type_of_reference env = function
+  | VarRef id -> let (_,_,t) = Environ.lookup_named id env in t
+  | ConstRef c -> Environ.constant_type env c
+  | IndRef ind -> Inductive.type_of_inductive env ind
+  | ConstructRef cstr -> Inductive.type_of_constructor env cstr
+
+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
new file mode 100644
index 00000000..1da5965c
--- /dev/null
+++ b/library/global.mli
@@ -0,0 +1,95 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: global.mli,v 1.40.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+
+(*i*)
+open Names
+open Univ
+open Term
+open Declarations
+open Entries
+open Indtypes
+open Safe_typing
+   (*i*)
+
+(* This module defines the global environment of Coq.  The functions
+   below are exactly the same as the ones in [Safe_typing], operating on
+   that global environment. [add_*] functions perform name verification,
+   i.e. check that the name given as argument match those provided by
+   [Safe_typing]. *)
+
+
+
+val safe_env : unit -> safe_environment
+val env : unit -> Environ.env
+
+val universes : unit -> universes
+val named_context : unit -> Sign.named_context
+
+(*s Extending env with variables and local definitions *)
+val push_named_assum : (identifier * types) -> Univ.constraints
+val push_named_def   : (identifier * constr * types option) -> Univ.constraints
+
+(*s Adding constants, inductives, modules and module types.  All these
+  functions verify that given names match those generated by kernel *)
+
+val add_constant : 
+  dir_path -> identifier -> global_declaration -> kernel_name
+val add_mind        : 
+  dir_path -> identifier -> mutual_inductive_entry -> kernel_name
+
+val add_module      : identifier -> module_entry -> module_path
+val add_modtype     : identifier -> module_type_entry -> kernel_name
+
+val add_constraints : constraints -> unit
+
+val set_engagement : Environ.engagement -> unit
+
+(*s Interactive modules and module types *)
+(* Both [start_*] functions take the [dir_path] argument to create a 
+   [mod_self_id]. This should be the name of the compilation unit. *)
+
+(* [start_*] functions return the [module_path] valid for components
+   of the started module / module type *)
+
+val start_module : 
+  identifier -> (mod_bound_id * module_type_entry) list 
+    -> module_type_entry option 
+      -> module_path
+
+val end_module :
+  identifier -> module_path
+
+val start_modtype :
+  identifier -> (mod_bound_id * module_type_entry) list
+    -> module_path
+
+val end_modtype :
+  identifier -> kernel_name
+
+
+(* Queries *)
+val lookup_named     : variable -> named_declaration
+val lookup_constant  : constant -> constant_body
+val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body
+val lookup_mind      : mutual_inductive -> mutual_inductive_body
+val lookup_module    : module_path -> module_body
+val lookup_modtype   : kernel_name -> module_type_body
+
+(* Compiled modules *)
+val start_library : dir_path -> module_path
+val export : dir_path -> compiled_library
+val import : compiled_library -> Digest.t -> module_path
+
+(*s Function to get an environment from the constants part of the global
+ * environment and a given context. *)
+  
+val type_of_global : Libnames.global_reference -> types
+val env_of_context : Sign.named_context -> Environ.env
+
diff --git a/library/goptions.ml b/library/goptions.ml
new file mode 100644
index 00000000..bcb4fb79
--- /dev/null
+++ b/library/goptions.ml
@@ -0,0 +1,359 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: goptions.ml,v 1.22.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+
+(* This module manages customization parameters at the vernacular level     *)
+
+open Pp
+open Util
+open Libobject
+open Names
+open Libnames
+open Term
+open Nametab
+
+(****************************************************************************)
+(* 0- Common things                                                         *)
+
+type option_name =
+  | PrimaryTable of string
+  | SecondaryTable of string * string
+
+let nickname = function
+  | PrimaryTable s         -> s
+  | SecondaryTable (s1,s2) -> s1^" "^s2
+
+let error_undeclared_key key =
+  error ((nickname key)^": no table or option of this type")
+
+type value =
+  | BoolValue   of bool
+  | IntValue    of int option
+  | StringValue of string
+  | IdentValue  of global_reference
+
+(****************************************************************************)
+(* 1- Tables                                                                *)
+
+class type ['a] table_of_A =
+object
+  method add : 'a -> unit
+  method remove : 'a -> unit
+  method mem : 'a -> unit
+  method print : unit
+end
+
+module MakeTable =
+  functor
+   (A : sig
+	  type t
+	  type key
+	  val table : (string * key table_of_A) list ref
+	  val encode : key -> t
+	  val subst : substitution -> t -> t
+          val printer : t -> std_ppcmds
+          val key : option_name
+          val title : string
+          val member_message : t -> bool -> std_ppcmds
+          val synchronous : bool
+        end) ->
+  struct
+    type option_mark =
+      | GOadd
+      | GOrmv
+
+    let nick = nickname A.key
+
+    let _ =
+      if List.mem_assoc nick !A.table then
+	error "Sorry, this table name is already used"
+
+    module MyType = struct type t = A.t let compare = Pervasives.compare end
+    module MySet = Set.Make(MyType)
+
+    let t = ref (MySet.empty : MySet.t)
+
+    let _ = 
+      if A.synchronous then
+	let freeze () = !t in
+	let unfreeze c = t := c in
+	let init () = t := MySet.empty in
+	Summary.declare_summary nick
+          { Summary.freeze_function = freeze;
+            Summary.unfreeze_function = unfreeze;
+            Summary.init_function = init;
+	    Summary.survive_module = false;
+	    Summary.survive_section = true }
+
+    let (add_option,remove_option) =
+      if A.synchronous then
+        let cache_options (_,(f,p)) = match f with
+          | GOadd -> t := MySet.add p !t
+          | GOrmv -> t := MySet.remove p !t in
+        let load_options i o = if i=1 then cache_options o in
+	let subst_options (_,subst,(f,p as obj)) = 
+	  let p' = A.subst subst p in
+	    if p' == p then obj else
+	      (f,p')
+	in
+	let export_options fp = Some fp in
+        let (inGo,outGo) =
+          Libobject.declare_object {(Libobject.default_object nick) with
+                Libobject.load_function = load_options;
+		Libobject.open_function = load_options;
+		Libobject.cache_function = cache_options;
+		Libobject.subst_function = subst_options;
+		Libobject.classify_function = (fun (_,x) -> Substitute x);
+		Libobject.export_function = export_options} 
+	in
+        ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
+         (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c))))
+      else
+        ((fun c -> t := MySet.add c !t),
+         (fun c -> t := MySet.remove c !t))
+
+    let print_table table_name printer table =
+      msg (str table_name ++ 
+	   (hov 0 
+	      (if MySet.is_empty table then str "None" ++ fnl ()
+               else MySet.fold
+		 (fun a b -> printer a ++ spc () ++ b)
+		 table (mt ()) ++ fnl ())))
+
+    class table_of_A () =
+    object
+      method add x = add_option (A.encode x)
+      method remove x = remove_option (A.encode x)
+      method mem x = 
+	let y = A.encode x in
+        let answer = MySet.mem y !t in
+        msg (A.member_message y answer ++ fnl ())
+      method print = print_table A.title A.printer !t 
+    end
+
+    let _ = A.table := (nick,new table_of_A ())::!A.table
+    let active c = MySet.mem c !t
+    let elements () = MySet.elements !t
+  end
+
+let string_table = ref []
+
+let get_string_table k = List.assoc (nickname k) !string_table
+
+module type StringConvertArg =
+sig
+  val key : option_name
+  val title : string
+  val member_message : string -> bool -> std_ppcmds
+  val synchronous : bool
+end
+
+module StringConvert = functor (A : StringConvertArg) ->
+struct
+  type t = string
+  type key = string
+  let table = string_table
+  let encode x = x
+  let subst _ x = x
+  let printer = str
+  let key = A.key
+  let title = A.title
+  let member_message = A.member_message
+  let synchronous = A.synchronous
+end
+
+module MakeStringTable =
+  functor (A : StringConvertArg) -> MakeTable (StringConvert(A))
+
+let ref_table = ref []
+
+let get_ref_table k = List.assoc (nickname k) !ref_table
+
+module type RefConvertArg =
+sig
+  type t
+  val encode : reference -> t
+  val subst : substitution -> t -> t
+  val printer : t -> std_ppcmds
+  val key : option_name
+  val title : string
+  val member_message : t -> bool -> std_ppcmds
+  val synchronous : bool
+end
+
+module RefConvert = functor (A : RefConvertArg) -> 
+struct
+  type t = A.t
+  type key = reference
+  let table = ref_table
+  let encode = A.encode
+  let subst = A.subst
+  let printer = A.printer
+  let key = A.key
+  let title = A.title
+  let member_message = A.member_message
+  let synchronous = A.synchronous
+end
+
+module MakeRefTable =
+  functor (A : RefConvertArg) -> MakeTable (RefConvert(A))
+
+(****************************************************************************)
+(* 2- Options                                                               *)
+
+type 'a option_sig = {
+  optsync  : bool;
+  optname  : string;
+  optkey   : option_name;
+  optread  : unit -> 'a;
+  optwrite : 'a -> unit }
+
+type option_type = bool * (unit -> value) -> (value -> unit) 
+
+module Key = struct type t = option_name let compare = Pervasives.compare end
+module OptionMap = Map.Make(Key)
+
+let value_tab = ref OptionMap.empty
+
+(* This raises Not_found if option of key [key] is unknown *)
+
+let get_option key = OptionMap.find key !value_tab
+
+let check_key key = try 
+  let _ = get_option key in
+  error "Sorry, this option name is already used"
+with Not_found ->
+  if List.mem_assoc (nickname key) !string_table
+    or List.mem_assoc (nickname key) !ref_table
+  then error "Sorry, this option name is already used"
+
+open Summary
+open Libobject
+open Lib
+
+let declare_option cast uncast 
+  { optsync=sync; optname=name; optkey=key; optread=read; optwrite=write } =
+  check_key key;
+  let default = read() in
+  let write = if sync then 
+    let (decl_obj,_) = 
+      declare_object {(default_object (nickname key)) with
+		       cache_function = (fun (_,v) -> write v);
+		       classify_function = (fun _ -> Dispose)}
+    in 
+    let _ = declare_summary (nickname key) 
+	      {freeze_function = read;
+	       unfreeze_function = write;
+	       init_function = (fun () -> write default);
+	       survive_module = false;
+	       survive_section = true}
+    in 
+    fun v -> add_anonymous_leaf (decl_obj v)
+  else write
+  in 
+  let cread () = cast (read ()) in
+  let cwrite v = write (uncast v) in 
+  value_tab := OptionMap.add key (name,(sync,cread,cwrite)) !value_tab; 
+  write
+
+type 'a write_function = 'a -> unit
+
+let declare_int_option =
+  declare_option 
+    (fun v -> IntValue v)
+    (function IntValue v -> v | _ -> anomaly "async_option")
+let declare_bool_option =
+  declare_option
+    (fun v -> BoolValue v)
+    (function BoolValue v -> v | _ -> anomaly "async_option")
+let declare_string_option =
+  declare_option
+    (fun v -> StringValue v)
+    (function StringValue v -> v | _ -> anomaly "async_option")
+
+(* 3- User accessible commands *)
+
+(* Setting values of options *)
+
+let set_option_value check_and_cast key v =
+  let (name,(_,read,write)) =
+    try get_option key
+    with Not_found -> error ("There is no option "^(nickname key)^".")
+  in
+  write (check_and_cast v (read ()))
+
+let bad_type_error () = error "Bad type of value for this option"
+
+let set_int_option_value = set_option_value
+  (fun v -> function 
+     | (IntValue _) -> IntValue v
+     | _ -> bad_type_error ())
+let set_bool_option_value = set_option_value
+  (fun v -> function 
+     | (BoolValue _) -> BoolValue v
+     | _ -> bad_type_error ())
+let set_string_option_value = set_option_value
+ (fun v -> function 
+    | (StringValue _) -> StringValue v
+    | _ -> bad_type_error ())
+
+(* Printing options/tables *)
+
+let msg_option_value (name,v) =
+  match v with
+    | BoolValue true  -> str "true"
+    | BoolValue false -> str "false"
+    | IntValue (Some n) -> int n
+    | IntValue None   -> str "undefined"
+    | StringValue s   -> str s
+    | IdentValue r    -> pr_global_env Idset.empty r
+
+let print_option_value key =
+  let (name,(_,read,_)) = get_option key in
+  let s = read () in 
+  match s with
+    | BoolValue b -> 
+	msg (str ("The "^name^" mode is "^(if b then "on" else "off")) ++ 
+	     fnl ())
+    | _ ->
+	msg (str ("Current value of "^name^" is ") ++
+	     msg_option_value (name,s) ++ fnl ())
+
+
+let print_tables () =
+  msg
+    (str "Synchronous options:" ++ fnl () ++
+     OptionMap.fold 
+       (fun key (name,(sync,read,write)) p -> 
+	  if sync then 
+	    p ++ str ("  "^(nickname key)^": ") ++
+	    msg_option_value (name,read()) ++ fnl ()
+	  else 
+	    p)
+       !value_tab (mt ()) ++
+     str "Asynchronous options:" ++ fnl () ++
+     OptionMap.fold 
+       (fun key (name,(sync,read,write)) p -> 
+	  if sync then 
+	    p
+	  else 
+	    p ++ str ("  "^(nickname key)^": ") ++
+            msg_option_value (name,read()) ++ fnl ())
+       !value_tab (mt ()) ++
+     str "Tables:" ++ fnl () ++
+     List.fold_right
+       (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+       !string_table (mt ()) ++
+     List.fold_right
+       (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+       !ref_table (mt ()) ++
+     fnl ()
+    )
+
+
diff --git a/library/goptions.mli b/library/goptions.mli
new file mode 100644
index 00000000..bbf5357a
--- /dev/null
+++ b/library/goptions.mli
@@ -0,0 +1,171 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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*)
+
+(* This module manages customization parameters at the vernacular level     *)
+
+(* Two kinds of things are managed : tables and options value
+   - Tables are created by applying the [MakeTable] functor.
+   - Variables storing options value are created by applying one of the
+   [declare_int_option], [declare_bool_option], ... functions.
+
+   Each table/option is uniquely identified by a key of type [option_name].
+   There are two kinds of table/option idenfiers: the primary ones
+   (supposed to be more global) and the secondary ones
+
+   The declaration of a table, say of name [SecondaryTable("Toto","Titi")] 
+   automatically makes available the following vernacular commands:
+
+      Add Toto Titi foo.
+      Remove Toto Titi foo.
+      Print Toto Titi.
+      Test Toto Titi.
+
+   The declaration of a non boolean option value, say of name
+   [SecondaryTable("Tata","Tutu")], automatically makes available the
+   following vernacular commands:
+
+       Set Tata Tutu val.
+       Print Table Tata Tutu.
+
+   If it is the declaration of a boolean value, the following
+   vernacular commands are made available:
+
+       Set Tata Tutu.
+       Unset Tata Tutu.
+       Print Table Tata Tutu. (* synonym: Test Table Tata Tutu. *)
+
+   For a primary table, say of name [PrimaryTable("Bidule")], the
+   vernacular commands look like
+
+      Add Bidule foo.
+      Print Table Bidule foo.
+      Set Bidule foo.
+      ...
+
+   The created table/option may be declared synchronous or not
+   (synchronous = consistent with the resetting commands)                   *)
+
+(*i*)
+open Pp
+open Util
+open Names
+open Libnames
+open Term
+open Nametab
+(*i*)
+
+(*s Things common to tables and options. *)
+
+(* The type of primary or secondary table/option keys *)
+type option_name =
+  | PrimaryTable of string
+  | SecondaryTable of string * string
+
+val error_undeclared_key : option_name -> 'a
+
+(*s Tables. *)
+
+(* The functor [MakeStringTable] declares a table containing objects
+   of type [string]; the function [member_message] say what to print
+   when invoking the "Test Toto Titi foo." command; at the end [title]
+   is the table name printed when invoking the "Print Toto Titi."
+   command; [active] is roughly the internal version of the vernacular
+   "Test ...": it tells if a given object is in the table; [elements]
+   returns the list of elements of the table *)
+
+module MakeStringTable :
+  functor
+    (A : sig
+       val key : option_name
+       val title : string
+       val member_message : string -> bool -> std_ppcmds
+       val synchronous : bool
+     end) ->
+sig
+  val active : string -> bool
+  val elements : unit -> string list
+end
+
+(* The functor [MakeRefTable] declares a new table of objects of type
+   [A.t] practically denoted by [reference]; the encoding function
+   [encode : reference -> A.t] is typically a globalization function,
+   possibly with some restriction checks; the function
+   [member_message] say what to print when invoking the "Test Toto
+   Titi foo." command; at the end [title] is the table name printed
+   when invoking the "Print Toto Titi." command; [active] is roughly
+   the internal version of the vernacular "Test ...": it tells if a
+   given object is in the table.  *)
+
+module MakeRefTable :
+  functor
+    (A : sig
+           type t
+           val encode : reference -> t
+	   val subst : substitution -> t -> t
+           val printer : t -> std_ppcmds
+           val key : option_name
+           val title : string
+           val member_message : t -> bool -> std_ppcmds
+           val synchronous : bool
+         end) ->
+    sig
+      val active : A.t -> bool
+      val elements : unit -> A.t list
+    end
+
+
+(*s Options. *)
+
+(* These types and function are for declaring a new option of name [key]
+   and access functions [read] and [write]; the parameter [name] is the option name 
+   used when printing the option value (command "Print Toto Titi." *)
+
+type 'a option_sig = {
+  optsync    : bool; 
+  optname    : string;
+  optkey     : option_name;
+  optread    : unit -> 'a;
+  optwrite   : 'a -> unit
+}
+
+(* When an option is declared synchronous ([optsync] is [true]), the output is 
+   a synchronous write function. Otherwise it is [optwrite] *)
+
+type 'a write_function = 'a -> unit
+
+val declare_int_option   : int option option_sig -> int option write_function
+val declare_bool_option  : bool option_sig   -> bool write_function
+val declare_string_option: string option_sig -> string write_function
+
+
+(*s Special functions supposed to be used only in vernacentries.ml *)
+
+val get_string_table :
+  option_name ->
+    < add : string -> unit;
+      remove : string -> unit;
+      mem : string -> unit;
+      print : unit >
+
+val get_ref_table :
+  option_name ->
+    < add : reference -> unit;
+      remove : reference -> unit;
+      mem : reference -> unit;
+      print : unit >
+
+val set_int_option_value    : option_name -> int option -> unit
+val set_bool_option_value   : option_name -> bool   -> unit
+val set_string_option_value : option_name -> string -> unit
+
+val print_option_value : option_name -> unit
+
+val print_tables : unit -> unit
+
diff --git a/library/impargs.ml b/library/impargs.ml
new file mode 100644
index 00000000..8a9429a4
--- /dev/null
+++ b/library/impargs.ml
@@ -0,0 +1,551 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: impargs.ml,v 1.59.2.1 2004/07/16 19:30:35 herbelin Exp $ *)
+
+open Util
+open Names
+open Libnames
+open Term
+open Reduction
+open Declarations
+open Environ
+open Inductive
+open Libobject
+open Lib
+open Nametab
+open Pp
+open Termops
+open Topconstr
+
+(*s Flags governing the computation of implicit arguments *)
+
+(* les implicites sont stricts par défaut en v8 *)
+let implicit_args = ref false
+let strict_implicit_args = ref (not !Options.v7)
+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
+
+let make_strict_implicit_args flag =
+  strict_implicit_args := flag;
+  if not !Options.v7_only then strict_implicit_args_out := flag
+
+let make_contextual_implicit_args flag =
+  contextual_implicit_args := flag;
+  if not !Options.v7_only then contextual_implicit_args_out := 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)
+
+let with_implicits ((a,b,c),(d,e,g)) 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
+
+(*s Computation of implicit arguments *)
+
+(* We remember various information about why an argument is (automatically)
+   inferable as implicit
+
+- [DepRigid] means that the implicit argument can be found by
+  unification along a rigid path (we do not print the arguments of
+  this kind if there is enough arguments to infer them)
+
+- [DepFlex] means that the implicit argument can be found by unification
+  along a collapsable path only (e.g. as x in (P x) where P is another
+  argument) (we do (defensively) print the arguments of this kind)
+
+- [DepFlexAndRigid] means that the least argument from which the
+  implicit argument can be inferred is following a collapsable path
+  but there is a greater argument from where the implicit argument is
+  inferable following a rigid path (useful to know how to print a
+  partial application)
+
+  We also consider arguments inferable from the conclusion but it is
+  operational only if [conclusion_matters] is true.
+*)
+
+type argument_position =
+  | Conclusion
+  | Hyp of int
+
+type implicit_explanation =
+  | DepRigid of argument_position
+  | DepFlex of argument_position
+  | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
+  | Manual
+
+let argument_less = function
+  | Hyp n, Hyp n' -> n<n'
+  | Hyp _, Conclusion -> true
+  | Conclusion, _ -> false
+
+let update pos rig (na,st) =
+  let e =
+  if rig then
+    match st with
+      | None -> DepRigid pos
+      | Some (DepRigid n as x) ->
+          if argument_less (pos,n) then DepRigid pos else x
+      | 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) ->
+          if argument_less (pos,fpos) or pos=fpos then DepRigid pos
+          else DepFlexAndRigid (fpos,pos)
+      | Some Manual -> assert false
+  else
+    match st with
+      | None -> DepFlex pos
+      | Some (DepRigid rpos as x) ->
+          if argument_less (pos,rpos) then DepFlexAndRigid (pos,rpos) else x
+      | Some (DepFlexAndRigid (fpos,rpos) as x) ->
+          if argument_less (pos,fpos) then DepFlexAndRigid (pos,rpos) else x
+      | Some (DepFlex fpos as x) ->
+          if argument_less (pos,fpos) then DepFlex pos else x
+      | Some Manual -> assert false
+  in na, Some e
+
+(* modified is_rigid_reference with a truncated env *)
+let is_flexible_reference env bound depth f =
+  match kind_of_term f with
+    | Rel n when n >= bound+depth -> (* inductive type *) false
+    | Rel n when n >= depth -> (* previous argument *) true
+    | Rel n -> (* since local definitions have been expanded *) false
+    | Const kn ->
+        let cb = Environ.lookup_constant kn env in
+        cb.const_body <> None & not cb.const_opaque
+    | Var id ->
+        let (_,value,_) = Environ.lookup_named id env in value <> None
+    | Ind _ | Construct _ -> false
+    |  _ -> true
+
+let push_lift d (e,n) = (push_rel d e,n+1)
+
+(* Precondition: rels in env are for inductive types only *)
+let add_free_rels_until strict bound env m pos acc =
+  let rec frec rig (env,depth as ed) c =
+    match kind_of_term (whd_betadeltaiota env c) with
+    | Rel n when (n < bound+depth) & (n >= depth) ->
+        acc.(bound+depth-n-1) <- update pos rig (acc.(bound+depth-n-1))
+    | App (f,_) when rig & is_flexible_reference env bound depth f ->
+	if strict then () else
+          iter_constr_with_full_binders push_lift (frec false) ed c
+    | Case _ when rig ->
+	if strict then () else
+          iter_constr_with_full_binders push_lift (frec false) ed c
+    | _ ->
+        iter_constr_with_full_binders push_lift (frec rig) ed c
+  in 
+  frec true (env,1) m; acc
+
+(* calcule la liste des arguments implicites *)
+
+let my_concrete_name avoid names t = function
+  | Anonymous -> Anonymous, avoid, Anonymous::names
+  | na -> 
+      let id = Termops.next_name_not_occuring false na avoid names t in
+      Name id, id::avoid, Name id::names
+  
+let compute_implicits_gen strict contextual env t =
+  let rec aux env avoid n names t =
+    let t = whd_betadeltaiota env t in
+    match kind_of_term t with
+      | Prod (na,a,b) ->
+	  let na',avoid' = Termops.concrete_name false avoid names na b in
+	  add_free_rels_until strict n env a (Hyp (n+1))
+            (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
+      | _ -> 
+	  let names = List.rev names in
+	  let v = Array.map (fun na -> na,None) (Array.of_list names) in
+	  if contextual then add_free_rels_until strict n env t Conclusion v
+	  else v
+  in 
+  match kind_of_term (whd_betadeltaiota env t) with 
+    | Prod (na,a,b) ->
+	let na',avoid = Termops.concrete_name false [] [] na b in
+	let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
+	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 l = compute_implicits_gen strict contextual env t in
+  List.map (function
+    | (Name id, Some imp) -> Some (id,imp)
+    | (Anonymous, Some _) -> anomaly "Unnamed implicit"
+    | _ -> None) l
+
+type implicit_status =
+    (* None = Not implicit *)
+    (identifier * implicit_explanation) option
+
+type implicits_list = implicit_status list
+
+let is_status_implicit = function
+  | None -> false
+  | _ -> true
+
+let name_of_implicit = function
+  | None -> anomaly "Not an implicit argument"
+  | Some (id,_) -> id
+
+(* [in_ctx] means we now the expected type, [n] is the index of the argument *)
+let is_inferable_implicit in_ctx n = function
+  | None -> false
+  | Some (_,DepRigid (Hyp p)) -> n >= p
+  | Some (_,DepFlex (Hyp p)) -> false
+  | Some (_,DepFlexAndRigid (_,Hyp q)) -> n >= q
+  | Some (_,DepRigid Conclusion) -> in_ctx
+  | Some (_,DepFlex Conclusion) -> false
+  | Some (_,DepFlexAndRigid (_,Conclusion)) -> false
+  | Some (_,Manual) -> true
+
+let positions_of_implicits =
+  let rec aux n = function
+      [] -> []
+    | Some _ :: l -> n :: aux (n+1) l
+    | None :: l -> aux (n+1) l
+  in aux 1
+
+type strict_flag = bool     (* true = strict *)
+type contextual_flag = bool (* true = contextual *)
+
+type implicits =
+  | Impl_auto of strict_flag * contextual_flag * implicits_list
+  | Impl_manual of implicits_list
+  | 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
+
+let list_of_implicits = function 
+  | Impl_auto (_,_,l) -> l
+  | Impl_manual l -> l
+  | No_impl -> []
+
+(*s Constants. *)
+
+let constants_table = ref KNmap.empty
+
+let compute_constant_implicits kn =
+  let env = Global.env () in
+  let cb = lookup_constant kn env in
+  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
+
+(*s Inductives and constructors. Their implicit arguments are stored
+   in an array, indexed by the inductive number, of pairs $(i,v)$ where
+   $i$ are the implicit arguments of the inductive and $v$ the array of 
+   implicit arguments of the constructors. *)
+
+let inductives_table = ref Indmap.empty
+
+let constructors_table = ref Constrmap.empty
+
+let compute_mib_implicits kn =
+  let env = Global.env () in
+  let mib = lookup_mind kn env in
+  let ar =
+    Array.to_list
+      (Array.map  (* No need to lift, arities contain no de Bruijn *)
+        (fun mip -> (Name mip.mind_typename, None, mip.mind_user_arity))
+        mib.mind_packets) in
+  let env_ar = push_rel_context ar env in
+  let imps_one_inductive i mip =
+    let ind = (kn,i) in
+    ((IndRef ind,auto_implicits env (body_of_type mip.mind_user_arity)),
+     Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c))
+       mip.mind_user_lc)
+  in
+  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
+
+let constructor_implicits consp =
+  try Constrmap.find consp !constructors_table with Not_found -> No_impl,No_impl
+(*s Variables. *)
+
+let var_table = ref Idmap.empty
+
+let compute_var_implicits id =
+  let env = Global.env () in
+  let (_,_,ty) = lookup_named id env in
+  auto_implicits env ty
+
+let var_implicits id = 
+  try Idmap.find id !var_table with Not_found -> No_impl,No_impl
+
+(* Caching implicits *)
+
+let cache_implicits_decl (r,imps) =
+  match r with
+  | VarRef id -> 
+      var_table := Idmap.add id imps !var_table
+  | ConstRef kn ->
+      constants_table := KNmap.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 subst_implicits_decl subst (r,imps as o) =
+  let r' = 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
+
+let (in_implicits, _) =
+  declare_object {(default_object "IMPLICITS") with 
+    cache_function = cache_implicits;
+    load_function = (fun _ -> cache_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))
+    declare_implicits_gen r
+
+let declare_var_implicits id =
+  if !implicit_args or !implicit_args_out then
+    declare_implicits_gen (VarRef id)
+
+let declare_constant_implicits kn =
+  if !implicit_args or !implicit_args_out then
+    declare_implicits_gen (ConstRef kn)
+
+let declare_mib_implicits kn =
+  if !implicit_args or !implicit_args_out then
+  let imps = compute_mib_implicits kn in
+  let imps = array_map_to_list
+    (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) imps in
+  add_anonymous_leaf (in_implicits (List.flatten imps))
+
+let implicits_of_global_gen = function
+  | VarRef id -> var_implicits id
+  | ConstRef sp -> constant_implicits sp
+  | IndRef isp -> inductive_implicits isp
+  | 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
+
+(* 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)
+
+let declare_manual_implicits r l =
+  let t = Global.type_of_global r in
+  let autoimps = compute_implicits_gen false true (Global.env()) t in
+  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
+	  with Not_found ->
+	  try list_remove (ExplByName id) l, set_implicit id imp
+	  with Not_found ->
+	  l, None in
+	imp :: merge (k+1) l' imps
+    | (Anonymous,imp)::imps -> 
+	None :: merge (k+1) l imps
+    | [] when l = [] -> []
+    | _ ->
+	match List.hd l with
+	| ExplByName id ->
+	    error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
+	| ExplByPos i ->
+	    if i<1 or i>n then 
+	      error ("Bad implicit argument number: "^(string_of_int i))
+	    else
+	      errorlabstrm ""
+		(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 *)
+
+let test = function
+  | No_impl | Impl_manual _ -> false,false,false
+  | 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)
+    
+let is_implicit_constant sp =
+  test_if_implicit (KNmap.find sp) !constants_table
+
+let is_implicit_inductive_definition indp =
+  test_if_implicit (Indmap.find (indp,0)) !inductives_table
+
+let is_implicit_var id =
+  test_if_implicit (Idmap.find id) !var_table
+
+(*s Registration as global tables *)
+
+let init () =
+  constants_table := KNmap.empty;
+  inductives_table := Indmap.empty;
+  constructors_table := Constrmap.empty;
+  var_table := Idmap.empty
+
+let freeze () =
+  (!constants_table, !inductives_table, 
+   !constructors_table, !var_table)
+
+let unfreeze (ct,it,const,vt) =
+  constants_table := ct;
+  inductives_table := it;
+  constructors_table := const;
+  var_table := vt
+
+let _ = 
+  Summary.declare_summary "implicits"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_module = false;
+      Summary.survive_section = false }
+
+(* 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
new file mode 100644
index 00000000..8db04ee7
--- /dev/null
+++ b/library/impargs.mli
@@ -0,0 +1,69 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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*)
+open Names
+open Libnames
+open Term
+open Environ
+open Nametab
+(*i*)
+
+(*s Implicit arguments. Here we store the implicit arguments. Notice that we 
+    are outside the kernel, which knows nothing about implicit arguments. *)
+
+val make_implicit_args : bool -> unit
+val make_strict_implicit_args : bool -> unit
+val make_contextual_implicit_args : bool -> unit
+
+val is_implicit_args : unit -> bool
+val is_strict_implicit_args : unit -> bool
+val is_contextual_implicit_args : unit -> bool
+
+type implicits_flags
+val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
+
+(*s An [implicits_list] is a list of positions telling which arguments
+    of a reference can be automatically infered *)
+type implicit_status
+type implicits_list = implicit_status list
+
+val is_status_implicit : implicit_status -> bool
+val is_inferable_implicit : bool -> int -> implicit_status -> bool
+val name_of_implicit : implicit_status -> identifier
+
+val 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
+
+(*s Computation of implicits (done using the global environment). *)
+
+val declare_var_implicits : variable -> unit
+val declare_constant_implicits : constant -> unit
+val declare_mib_implicits : mutual_inductive -> unit
+
+val declare_implicits : global_reference -> unit
+
+(* Manual declaration of which arguments are expected implicit *)
+val declare_manual_implicits : global_reference -> 
+  Topconstr.explicitation list -> unit
+
+(* Get implicit arguments *)
+val is_implicit_constant : constant -> implicits_flags
+val is_implicit_inductive_definition : mutual_inductive -> implicits_flags
+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
diff --git a/library/lib.ml b/library/lib.ml
new file mode 100644
index 00000000..b9da6dea
--- /dev/null
+++ b/library/lib.ml
@@ -0,0 +1,566 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: lib.ml,v 1.63.2.2 2004/07/16 19:30:35 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Libnames
+open Nameops
+open Libobject
+open Summary
+
+
+
+type node = 
+  | Leaf of obj
+  | CompilingLibrary of object_prefix
+  | OpenedModule of 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
+  | FrozenState of Summary.frozen
+
+and library_entry = object_name * node
+
+and library_segment = library_entry list
+
+type lib_objects =  (identifier * obj) list
+
+let iter_objects f i prefix =
+  List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
+
+let load_objects = iter_objects load_object
+let open_objects = iter_objects open_object
+
+let subst_objects prefix subst seg = 
+  let subst_one = fun (id,obj as node) ->
+    let obj' = subst_object (make_oname prefix id, subst, obj) in
+      if obj' == obj then node else
+	(id, obj')
+  in
+    list_smartmap subst_one 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 -> 
+	let id = id_of_label (label kn) in
+	  (match classify_object (oname,o) with 
+	     | Dispose -> clean acc stk
+	     | Keep o' -> 
+		 clean (substl, (id,o')::keepl, anticipl) stk
+	     | Substitute o' -> 
+		 clean ((id,o')::substl, keepl, anticipl) stk
+	     | Anticipate o' ->
+		 clean (substl, keepl, o'::anticipl) stk)
+    | (oname,ClosedSection _ as item) :: 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"
+    | (_,FrozenState _) :: stk -> clean acc stk
+  in
+    clean ([],[],[]) (List.rev seg)
+
+
+let segment_of_objects prefix =
+  List.map (fun (id,obj) -> (make_oname prefix id, Leaf obj))
+
+(* We keep trace of operations in the stack [lib_stk]. 
+   [path_prefix] is the current path of sections, where sections are stored in 
+   ``correct'' order, the oldest coming first in the list. It may seems 
+   costly, but in practice there is not so many openings and closings of
+   sections, but on the contrary there are many constructions of section
+   paths based on the library path. *) 
+
+let initial_prefix = default_library,(initial_path,empty_dirpath)
+
+let lib_stk = ref ([] : library_segment)
+
+let comp_name = ref None
+
+let library_dp () =
+  match !comp_name with Some m -> m | None -> default_library
+
+(* [path_prefix] is a pair of absolute dirpath and a pair of current
+   module path and relative section path *)
+let path_prefix = ref initial_prefix
+
+
+let cwd () = fst !path_prefix
+
+let make_path id = Libnames.make_path (cwd ()) id
+
+
+let current_prefix () = snd !path_prefix
+
+let make_kn id = 
+  let mp,dir = current_prefix () in
+    Names.make_kn mp dir (label_of_id id)
+
+
+let make_oname id = make_path id, make_kn id
+
+
+let sections_depth () =
+  List.length (repr_dirpath (snd (snd !path_prefix)))
+
+let sections_are_opened () =
+  match repr_dirpath (snd (snd !path_prefix)) with
+      [] -> false
+    | _ -> true
+
+
+let recalc_path_prefix () =
+  let rec recalc = function
+    | (sp, OpenedSection (dir,_)) :: _ -> dir
+    | (sp, OpenedModule (dir,_)) :: _ -> dir
+    | (sp, OpenedModtype (dir,_)) :: _ -> dir
+    | (sp, CompilingLibrary dir) :: _ -> dir
+    | _::l -> recalc l
+    | [] -> initial_prefix
+  in
+  path_prefix := recalc !lib_stk
+
+let pop_path_prefix () = 
+  let dir,(mp,sec) = !path_prefix in
+    path_prefix := fst (split_dirpath dir), (mp, fst (split_dirpath sec))
+
+let find_entry_p p = 
+  let rec find = function
+    | [] -> raise Not_found
+    | ent::l -> if p ent then ent else find l
+  in
+  find !lib_stk
+
+let find_split_p p = 
+  let rec find = function
+    | [] -> raise Not_found
+    | ent::l -> if p ent then ent,l else find l
+  in
+  find !lib_stk
+
+let split_lib sp = 
+  let rec collect after equal = function
+    | ((sp',_) as hd)::before ->
+      	if sp = sp' then collect after (hd::equal) before else after,equal,hd::before
+    | [] -> after,equal,[]
+  in
+  let rec findeq after = function
+    | ((sp',_) as hd)::before ->
+      	if sp = sp' then collect after [hd] before else findeq (hd::after) before
+    | [] -> error "no such entry"
+  in 
+  findeq [] !lib_stk
+
+(* Adding operations. *)
+
+let add_entry sp node =
+  lib_stk := (sp,node) :: !lib_stk
+
+let anonymous_id = 
+  let n = ref 0 in
+  fun () -> incr n; id_of_string ("_" ^ (string_of_int !n))
+
+let add_anonymous_entry node =
+  let id = anonymous_id () in
+  let name = make_oname id in
+  add_entry name node;
+  name
+
+let add_absolutely_named_leaf sp obj =
+  cache_object (sp,obj);
+  add_entry sp (Leaf obj)
+
+let add_leaf id obj =
+  let oname = make_oname id in
+  cache_object (oname,obj);
+  add_entry oname (Leaf obj);
+  oname
+
+let add_leaves id objs =
+  let oname = make_oname id in
+  let add_obj obj = 
+    add_entry oname (Leaf obj);
+    load_object 1 (oname,obj) 
+  in
+  List.iter add_obj objs;
+  oname
+
+let add_anonymous_leaf obj =
+  let id = anonymous_id () in
+  let oname = make_oname id in
+  cache_object (oname,obj);
+  add_entry oname (Leaf obj)
+
+let add_frozen_state () =
+  let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in ()
+
+(* Modules. *)
+
+let is_something_opened = function 
+    (_,OpenedSection _) -> true 
+  | (_,OpenedModule _) -> true
+  | (_,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 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));
+  path_prefix := prefix;
+  prefix
+(*  add_frozen_state () must be called in declaremods *)
+ 
+let end_module id = 
+  let oname,nametab = 
+    try match find_entry_p is_something_opened with
+      | oname,OpenedModule (_,nametab) -> 
+	  let sp = fst oname in
+	  let id' = basename sp in
+	  if id<>id' then error "this is not the last opened module"; 
+	  oname,nametab
+      | _,OpenedModtype _ ->
+	  error "there are some open module types"
+      | _,OpenedSection _ ->
+	  error "there are some open sections"
+      | _ -> assert false
+    with Not_found ->
+      error "no opened modules"
+  in
+  let (after,_,before) = split_lib oname in
+  lib_stk := before;
+  let prefix = !path_prefix in
+  recalc_path_prefix ();
+  (* add_frozen_state must be called after processing the module, 
+     because we cannot recache interactive modules  *) 
+  (oname, prefix, nametab,after)
+
+let start_modtype id mp nametab = 
+  let dir = extend_dirpath (fst !path_prefix) id in
+  let prefix = dir,(mp,empty_dirpath) in
+  let sp = make_path id in
+  let name = sp, make_kn id in
+  if Nametab.exists_cci sp then
+    errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ;
+  add_entry name (OpenedModtype (prefix,nametab));
+  path_prefix := prefix;
+  prefix
+
+let end_modtype id = 
+  let sp,nametab = 
+    try match find_entry_p is_something_opened with
+      | sp,OpenedModtype (_,nametab) -> 
+	  let id' = basename (fst sp) in
+	  if id<>id' then error "this is not the last opened module"; 
+	  sp,nametab
+      | _,OpenedModule _ ->
+	  error "there are some open modules"
+      | _,OpenedSection _ ->
+	  error "there are some open sections"
+      | _ -> assert false
+    with Not_found ->
+      error "no opened module types"
+  in
+  let (after,_,before) = split_lib sp in
+  lib_stk := before;
+  let dir = !path_prefix in
+  recalc_path_prefix ();
+  (* add_frozen_state must be called after processing the module type.
+     This is because we cannot recache interactive module types *) 
+  (sp,dir,nametab,after)
+
+
+
+let contents_after = function
+  | None -> !lib_stk
+  | Some sp -> let (after,_,_) = split_lib sp in after
+
+(* Modules. *)
+
+let check_for_comp_unit () =
+  let is_decl = function (_,FrozenState _) -> false | _ -> true in
+  try
+    let _ = find_entry_p is_decl in
+    error "a module cannot be started after some declarations"
+  with Not_found -> ()
+
+(* TODO: use check_for_module ? *)
+let start_compilation s mp =
+  if !comp_name <> None then
+    error "compilation unit is already started";
+  if snd (snd (!path_prefix)) <> empty_dirpath then
+    error "some sections are already opened";
+  let prefix = s, (mp, empty_dirpath) in
+  let _ = add_anonymous_entry (CompilingLibrary prefix) in
+  comp_name := Some s;
+  path_prefix := prefix
+
+let end_compilation dir =
+  let _ =
+    try match find_entry_p is_something_opened with
+      | _, OpenedSection _ -> error "There are some open sections"
+      | _, OpenedModule _ -> error "There are some open modules"
+      | _, OpenedModtype _ -> error "There are some open module types"
+      | _ -> assert false
+    with
+	Not_found -> ()
+  in
+  let module_p =
+    function (_,CompilingLibrary _) -> true | x -> is_something_opened x
+  in
+  let oname = 
+    try match find_entry_p module_p with
+	(oname, CompilingLibrary prefix) -> oname
+      | _ -> assert false
+    with
+	Not_found -> anomaly "No module declared"
+  in
+  let _ =  match !comp_name with
+      | None -> anomaly "There should be a module name..."
+      | Some m ->
+	  if m <> dir then anomaly 
+	    ("The current open module has name "^ (string_of_dirpath m) ^ 
+	     " and not " ^ (string_of_dirpath m));
+  in
+  let (after,_,before) = split_lib oname in
+  comp_name := None;
+  !path_prefix,after
+
+(* Returns true if we are inside an opened module type *)
+let is_modtype () = 
+  let opened_p = function
+    | _, OpenedModtype _ -> true 
+    | _ -> false
+  in
+    try 
+      let _ = find_entry_p opened_p in true
+    with
+	Not_found -> false
+
+(* Returns true if we are inside an opened module *)
+let is_module () = 
+  let opened_p = function
+    | _, OpenedModule _ -> true 
+    | _ -> false
+  in
+    try 
+      let _ = find_entry_p opened_p in true
+    with
+	Not_found -> false
+
+
+(* Returns the most recent OpenedThing node *)
+let what_is_opened () = find_entry_p is_something_opened
+
+(* XML output hooks *)
+let xml_open_section = ref (fun id -> ())
+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
+  let prefix = dir, (mp, extend_dirpath oldsec id) in
+  let name = make_path id, make_kn id (* this makes little sense however *) in
+  if Nametab.exists_section dir then
+    errorlabstrm "open_section" (pr_id id ++ str " already exists");
+  let sum = freeze_summaries() in
+  add_entry name (OpenedSection (prefix, sum));
+  (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
+  Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
+  path_prefix := prefix;
+  if !Options.xml_export then !xml_open_section id;
+  prefix
+
+
+(* Restore lib_stk and summaries as before the section opening, and
+   add a ClosedSection object. *)
+let close_section ~export id =
+  let oname,fs = 
+    try match find_entry_p is_something_opened with
+      | oname,OpenedSection (_,fs) -> 
+	  if id <> basename (fst oname) then
+	    error "this is not the last opened section";
+	  (oname,fs)
+      | _ -> assert false 
+    with Not_found ->
+      error "no opened section"
+  in
+  let (after,_,before) = split_lib oname in
+  lib_stk := before;
+  let prefix = !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;
+  if !Options.xml_export then !xml_close_section id;
+  (prefix, after, fs)
+
+(* Backtracking. *)
+
+let recache_decl = function
+  | (sp, Leaf o) -> cache_object (sp,o)
+  | _ -> ()
+
+
+let recache_context ctx =
+  List.iter recache_decl ctx
+
+let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
+
+let reset_to sp =
+  let (_,_,before) = split_lib sp in
+  lib_stk := before;
+  recalc_path_prefix ();
+  let spf = match find_entry_p is_frozen_state with
+    | (sp, FrozenState f) -> unfreeze_summaries f; sp
+    | _ -> assert false
+  in
+  let (after,_,_) = split_lib spf in
+  recache_context after
+
+let reset_name (loc,id) =
+  let (sp,_) = 
+    try
+      find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
+    with Not_found ->
+      user_err_loc (loc,"reset_name",pr_id id ++ str ": no such entry")
+  in
+  reset_to sp
+
+let is_mod_node = function 
+  | OpenedModule _ | OpenedModtype _ | OpenedSection _ 
+  | ClosedSection _ -> true 
+  | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
+  | _ -> false
+
+(* Reset on a module or section name in order to bypass constants with 
+   the same name *) 
+
+let reset_mod (loc,id) =
+  let (ent,before) = 
+    try
+      find_split_p (fun (sp,node) -> 
+                    let (_,spi) = repr_path (fst sp) in id = spi 
+                    && is_mod_node node)
+    with Not_found ->
+      user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry")
+  in
+  lib_stk := before;
+  recalc_path_prefix ();
+  let spf = match find_entry_p is_frozen_state with
+    | (sp, FrozenState f) -> unfreeze_summaries f; sp
+    | _ -> assert false
+  in
+  let (after,_,_) = split_lib spf in
+  recache_context after
+
+
+let point_obj =
+  let (f,_) = declare_object {(default_object "DOT") with
+				classify_function = (fun _ -> Dispose)} in
+    f()
+
+let mark_end_of_command () =
+  match !lib_stk with
+      (_,Leaf o)::_ when object_tag o = "DOT" -> ()
+    | _ -> add_anonymous_leaf point_obj
+
+let rec back_stk n stk =
+  match stk with
+      (sp,Leaf o)::tail when object_tag o = "DOT" ->
+        if n=0 then sp else back_stk (n-1) tail
+    | _::tail -> back_stk n tail
+    | [] -> error "Reached begin of command history"
+
+let back n = reset_to (back_stk n !lib_stk)
+
+(* State and initialization. *)
+
+type frozen = dir_path option * library_segment
+
+let freeze () = (!comp_name, !lib_stk)
+
+let unfreeze (mn,stk) =
+  comp_name := mn;
+  lib_stk := stk;
+  recalc_path_prefix ()
+
+let init () =
+  lib_stk := [];
+  add_frozen_state ();
+  comp_name := None;
+  path_prefix := initial_prefix;
+  init_summaries()
+
+(* Initial state. *)
+
+let initial_state = ref None
+
+let declare_initial_state () = 
+  let name = add_anonymous_entry (FrozenState (freeze_summaries())) in
+  initial_state := Some name
+
+let reset_initial () =
+  match !initial_state with
+    | None -> 
+        error "Resetting to the initial state is possible only interactively"
+    | Some sp -> 
+  	begin match split_lib sp with
+	  | (_,[_,FrozenState fs as hd],before) ->
+	      lib_stk := hd::before;
+	      recalc_path_prefix ();
+	      unfreeze_summaries fs
+	  | _ -> assert false
+	end
+
+
+(* Misc *)
+
+let library_part ref =
+  let sp = Nametab.sp_of_global ref in
+  let dir,_ = repr_path sp in
+  match ref with
+  | VarRef id -> 
+      anomaly "TODO";
+      extract_dirpath_prefix (sections_depth ()) (cwd ())
+  | _ ->
+      if is_dirpath_prefix_of dir (cwd ()) then
+        (* Not yet (fully) discharged *)
+        extract_dirpath_prefix (sections_depth ()) (cwd ())
+      else
+	(* Theorem/Lemma outside its outer section of definition *)
+	dir
diff --git a/library/lib.mli b/library/lib.mli
new file mode 100644
index 00000000..8981754e
--- /dev/null
+++ b/library/lib.mli
@@ -0,0 +1,156 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: lib.mli,v 1.41.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+
+(*i*)
+open Util
+open Names
+open Libnames
+open Libobject
+open Summary
+(*i*)
+
+(*s This module provides a general mechanism to keep a trace of all operations
+   and to backtrack (undo) those operations. It provides also the section
+   mechanism (at a low level; discharge is not known at this step). *)
+
+type node = 
+  | Leaf of obj
+  | CompilingLibrary of object_prefix
+  | OpenedModule of object_prefix * Summary.frozen
+  | OpenedModtype of object_prefix * Summary.frozen
+  | OpenedSection of object_prefix * Summary.frozen
+  | ClosedSection of bool * dir_path * library_segment
+  | FrozenState of Summary.frozen
+
+and library_segment = (object_name * node) list
+
+type lib_objects = (identifier * obj) list
+
+(*s Object iteratation functions. *)
+
+val open_objects : int -> object_prefix -> lib_objects -> unit
+val load_objects : int -> object_prefix -> lib_objects -> unit
+val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects
+
+(* [classify_segment seg] verifies that there are no OpenedThings,
+   clears ClosedSections and FrozenStates and divides Leafs according
+   to their answers to the [classify_object] function in three groups:
+   [Substitute], [Keep], [Anticipate] respectively.  The order of each
+   returned list is the same as in the input list. *)
+val classify_segment : 
+  library_segment -> lib_objects * lib_objects * obj list
+
+(* [segment_of_objects prefix objs] forms a list of Leafs *)
+val segment_of_objects :
+  object_prefix -> lib_objects -> library_segment
+
+
+(*s Adding operations (which call the [cache] method, and getting the
+  current list of operations (most recent ones coming first). *)
+
+val add_leaf : identifier -> obj -> object_name
+val add_absolutely_named_leaf : object_name -> obj -> unit
+val add_anonymous_leaf : obj -> unit
+
+(* this operation adds all objects with the same name and calls load_object 
+   for each of them *)
+val add_leaves : identifier -> obj list -> object_name
+
+val add_frozen_state : unit -> unit
+val mark_end_of_command : unit -> unit
+
+
+(*s The function [contents_after] returns the current library segment, 
+  starting from a given section path. If not given, the entire segment
+  is returned. *)
+
+val contents_after : object_name option -> library_segment
+
+(*s Functions relative to current path *)
+
+(* User-side names *)
+val cwd : unit -> dir_path
+val make_path : identifier -> section_path
+
+(* Kernel-side names *)
+val current_prefix : unit -> module_path * dir_path
+val make_kn : identifier -> kernel_name
+
+(* Are we inside an opened section *)
+val sections_are_opened : unit -> bool
+val sections_depth : unit -> int
+
+(* Are we inside an opened module type *)
+val is_modtype : unit -> bool
+val is_module : unit -> bool
+
+
+(* Returns the most recent OpenedThing node *)
+val what_is_opened : unit -> object_name * node
+
+
+(*s Modules and module types *)
+
+val start_module : 
+  module_ident -> module_path -> Summary.frozen -> object_prefix
+val end_module : module_ident 
+  -> object_name * object_prefix * Summary.frozen * library_segment
+
+val start_modtype : 
+  module_ident -> module_path -> Summary.frozen -> object_prefix
+val end_modtype : module_ident 
+  -> object_name * object_prefix * Summary.frozen * library_segment
+(* Lib.add_frozen_state must be called after each of the above functions *)
+
+(*s Compilation units *)
+
+val start_compilation : dir_path -> module_path -> unit
+val end_compilation : dir_path -> object_prefix * library_segment
+
+(* The function [library_dp] returns the [dir_path] of the current
+   compiling library (or [default_library]) *)
+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
+
+(*s Sections *)
+
+val open_section : identifier -> object_prefix
+
+val close_section : export:bool -> identifier -> 
+  object_prefix * library_segment * Summary.frozen
+
+(*s Backtracking (undo). *)
+
+val reset_to : object_name -> unit
+val reset_name : identifier located -> unit
+val reset_mod : identifier located -> unit
+
+(* [back n] resets to the place corresponding to the $n$-th call of 
+   [mark_end_of_command] (counting backwards) *)
+val back : int -> unit
+
+(*s We can get and set the state of the operations (used in [States]). *)
+
+type frozen
+
+val freeze : unit -> frozen
+val unfreeze : frozen -> unit
+
+val init : unit -> unit
+
+val declare_initial_state : unit -> unit
+val reset_initial : unit -> unit
+
+
+(* XML output hooks *)
+val set_xml_open_section : (identifier -> unit) -> unit
+val set_xml_close_section : (identifier -> unit) -> unit
diff --git a/library/libnames.ml b/library/libnames.ml
new file mode 100644
index 00000000..16f5a917
--- /dev/null
+++ b/library/libnames.ml
@@ -0,0 +1,269 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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*)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+
+type global_reference =
+  | VarRef of variable
+  | ConstRef of constant
+  | IndRef of inductive
+  | ConstructRef of constructor
+
+let subst_global subst ref = match ref with
+  | VarRef _ -> ref
+  | ConstRef kn ->
+      let kn' = subst_kn subst kn in if kn==kn' then ref else
+          ConstRef kn'
+  | IndRef (kn,i) ->
+      let kn' = subst_kn subst kn in if kn==kn' then ref else
+          IndRef(kn',i)
+  | ConstructRef ((kn,i),j) ->
+      let kn' = subst_kn subst kn in if kn==kn' then ref else
+          ConstructRef ((kn',i),j)
+
+let reference_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
+  | VarRef id -> mkVar id
+  | ConstRef sp -> mkConst sp
+  | ConstructRef sp -> mkConstruct sp
+  | IndRef sp -> mkInd sp
+
+module RefOrdered =
+  struct
+    type t = global_reference
+    let compare = Pervasives.compare
+  end
+
+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))
+
+(*s Operations on dirpaths *)
+
+(* Pop the last n module idents *)
+let extract_dirpath_prefix n dir =
+  make_dirpath (list_skipn n (repr_dirpath dir))
+
+let dirpath_prefix p = match repr_dirpath p with
+  | [] -> anomaly "dirpath_prefix: empty dirpath"
+  | _::l -> make_dirpath l
+
+let is_dirpath_prefix_of d1 d2 =
+  list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+
+(* To know how qualified a name should be to be understood in the current env*)
+let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])
+
+let split_dirpath d =
+  let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
+
+let extend_dirpath p id = make_dirpath (id :: repr_dirpath p)
+
+
+(*
+let path_of_constructor env ((sp,tyi),ind) =
+   let mib = Environ.lookup_mind sp env in
+   let mip = mib.mind_packets.(tyi) in 
+   let (pa,_) = repr_path sp in 
+   Names.make_path pa (mip.mind_consnames.(ind-1))
+
+let path_of_inductive env (sp,tyi) =
+  if tyi = 0 then sp
+  else
+    let mib = Environ.lookup_mind sp env in
+    let mip = mib.mind_packets.(tyi) in 
+    let (pa,_) = repr_path sp in 
+    Names.make_path pa (mip.mind_typename) 
+*)
+(* parsing *)
+let parse_dir s =
+  let len = String.length s in
+  let rec decoupe_dirs dirs n =
+    if n>=len then dirs else
+    let pos =
+      try
+	String.index_from s n '.' 
+      with Not_found -> len
+    in
+    let dir = String.sub s n (pos-n) in
+      decoupe_dirs ((id_of_string dir)::dirs) (pos+1)	  
+  in
+    decoupe_dirs [] 0
+
+let dirpath_of_string s = 
+  match parse_dir s with
+      [] -> invalid_arg "dirpath_of_string"
+    | dir -> make_dirpath dir
+
+module Dirset = Set.Make(struct type t = dir_path let compare = compare end)
+module Dirmap = Map.Make(struct type t = dir_path let compare = compare end)
+
+(*s Section paths are absolute names *)
+
+type section_path = {
+  dirpath : dir_path ;
+  basename : identifier }
+
+let make_path pa id = { dirpath = pa; basename = id }
+let repr_path { dirpath = pa; basename = id } = (pa,id)
+
+(* parsing and printing of section paths *)
+let string_of_path sp =
+  let (sl,id) = repr_path sp in
+  if repr_dirpath sl = [] then string_of_id id
+  else (string_of_dirpath sl) ^ "." ^ (string_of_id id)
+
+let sp_ord sp1 sp2 =
+  let (p1,id1) = repr_path sp1
+  and (p2,id2) = repr_path sp2 in
+  let p_bit = compare p1 p2 in
+  if p_bit = 0 then id_ord id1 id2 else p_bit
+
+module SpOrdered =
+  struct
+    type t = section_path
+    let compare = sp_ord
+  end
+
+module Spset = Set.Make(SpOrdered)
+module Sppred = Predicate.Make(SpOrdered)
+module Spmap = Map.Make(SpOrdered)
+
+let dirpath sp = let (p,_) = repr_path sp in p
+let basename sp = let (_,id) = repr_path sp in id
+
+let path_of_string s =
+  try
+    let dir, id = split_dirpath (dirpath_of_string s) in
+    make_path dir id
+  with
+    | Invalid_argument _ -> invalid_arg "path_of_string"
+
+let pr_sp sp = str (string_of_path sp) 
+
+let restrict_path n sp =
+  let dir, s = repr_path sp in
+  let dir' = list_firstn n (repr_dirpath dir) in
+  make_path (make_dirpath dir') s
+
+type extended_global_reference =
+  | TrueGlobal of global_reference
+  | SyntacticDef of kernel_name
+
+let 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 decode_kn kn = 
+  let mp,sec_dir,l = repr_kn 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
+
+let make_qualid = make_path
+let repr_qualid = repr_path
+
+let string_of_qualid = string_of_path
+let pr_qualid = pr_sp
+
+let qualid_of_string = path_of_string
+
+let qualid_of_sp sp = sp
+let make_short_qualid id = make_qualid empty_dirpath id
+let qualid_of_dirpath dir = 
+  let (l,a) = split_dirpath dir in
+  make_qualid l a
+
+type object_name = section_path * kernel_name
+
+type object_prefix = dir_path * (module_path * dir_path)
+
+let make_oname (dirpath,(mp,dir)) id = 
+  make_path dirpath id, make_kn mp dir (label_of_id id)
+
+(* to this type are mapped dir_path's in the nametab *)
+type global_dir_reference = 
+  | DirOpenModule of object_prefix
+  | DirOpenModtype of object_prefix
+  | DirOpenSection of object_prefix
+  | DirModule of object_prefix
+  | DirClosedSection of dir_path
+      (* this won't last long I hope! *)
+
+(*  | ModRef mp ->
+      let mp' = subst_modpath subst mp in if mp==mp' then ref else
+          ModRef mp'
+  | ModTypeRef kn ->
+      let kn' = subst_kernel_name subst kn in if kn==kn' then ref else
+          ModTypeRef kn'
+*)
+
+type reference = 
+  | Qualid of qualid located
+  | Ident of identifier located
+
+let qualid_of_reference = function
+  | Qualid (loc,qid) -> loc, qid
+  | Ident (loc,id) -> loc, make_short_qualid id
+
+let string_of_reference = function
+  | Qualid (loc,qid) -> string_of_qualid qid
+  | Ident (loc,id) -> string_of_id id
+
+let pr_reference = function 
+  | Qualid (_,qid) -> pr_qualid qid
+  | Ident (_,id) -> pr_id id
+
+let loc_of_reference = function
+  | Qualid (loc,qid) -> loc
+  | Ident (loc,id) -> loc
diff --git a/library/libnames.mli b/library/libnames.mli
new file mode 100644
index 00000000..6f05333c
--- /dev/null
+++ b/library/libnames.mli
@@ -0,0 +1,140 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: libnames.mli,v 1.8.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+
+(*i*)
+open Pp
+open Util
+open Names
+open Term
+(*i*)
+
+(*s Global reference is a kernel side type for all references together *)
+type global_reference =
+  | VarRef of variable
+  | ConstRef of constant
+  | IndRef of inductive
+  | ConstructRef of constructor
+
+val subst_global : substitution -> global_reference -> global_reference
+
+(* Turn a global reference into a construction *)
+val constr_of_reference : global_reference -> constr
+
+(* Turn a construction denoting a global into a reference;
+   raise [Not_found] if not a global *)
+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
+
+val dirpath_of_string : string -> dir_path
+
+(* Give the immediate prefix of a [dir_path] *)
+val dirpath_prefix : dir_path -> dir_path 
+
+(* Give the immediate prefix and basename of a [dir_path] *)
+val split_dirpath : dir_path -> dir_path * identifier
+
+val extend_dirpath : dir_path -> module_ident -> dir_path
+val add_dirpath_prefix : module_ident -> dir_path -> dir_path
+
+val extract_dirpath_prefix : int -> dir_path -> dir_path
+val is_dirpath_prefix_of : dir_path -> dir_path -> bool
+
+module Dirset : Set.S with type elt = dir_path
+module Dirmap : Map.S with type key = dir_path
+
+(*s Section paths are {\em absolute} names *)
+type section_path
+
+(* Constructors of [section_path] *)
+val make_path : dir_path -> identifier -> section_path
+
+(* Destructors of [section_path] *)
+val repr_path : section_path -> dir_path * identifier
+val dirpath : section_path -> dir_path
+val basename : section_path -> identifier
+
+(* Parsing and printing of section path as ["coq_root.module.id"] *)
+val path_of_string : string -> section_path
+val string_of_path : section_path -> string
+val pr_sp : section_path -> std_ppcmds
+
+module Sppred : Predicate.S with type elt = section_path
+module Spmap  : Map.S with type key = section_path
+
+val restrict_path : int -> section_path -> section_path
+
+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
+
+
+(*s A [qualid] is a partially qualified ident; it includes fully
+    qualified names (= absolute names) and all intermediate partial
+    qualifications of absolute names, including single identifiers *)
+type qualid
+
+val make_qualid : dir_path -> identifier -> qualid
+val repr_qualid : qualid -> dir_path * identifier
+
+val string_of_qualid : qualid -> string
+val pr_qualid : qualid -> std_ppcmds
+
+val qualid_of_string : string -> qualid
+
+(* Turns an absolute name into a qualified name denoting the same name *)
+val qualid_of_sp : section_path -> qualid
+
+val qualid_of_dirpath : dir_path -> qualid
+
+val make_short_qualid : identifier -> qualid
+
+(* Both names are passed to objects: a "semantic" kernel_name, which
+   can be substituted and a "syntactic" section_path which can be printed
+*)
+
+type object_name = section_path * kernel_name
+
+type object_prefix = dir_path * (module_path * dir_path)
+
+val make_oname : object_prefix -> identifier -> object_name
+
+(* to this type are mapped dir_path's in the nametab *)
+type global_dir_reference = 
+  | DirOpenModule of object_prefix
+  | DirOpenModtype of object_prefix
+  | DirOpenSection of object_prefix
+  | DirModule of object_prefix
+  | DirClosedSection of dir_path
+      (* this won't last long I hope! *)
+
+type reference = 
+  | Qualid of qualid located
+  | Ident of identifier located
+
+val qualid_of_reference : reference -> qualid located
+val string_of_reference : reference -> string
+val pr_reference : reference -> std_ppcmds
+val loc_of_reference : reference -> loc
diff --git a/library/libobject.ml b/library/libobject.ml
new file mode 100644
index 00000000..2e531e05
--- /dev/null
+++ b/library/libobject.ml
@@ -0,0 +1,157 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: libobject.ml,v 1.8.8.1 2004/07/16 19:30:35 herbelin Exp $ *)
+
+open Util
+open Names
+open Libnames
+
+(* The relax flag is used to make it possible to load files while ignoring
+   failures to incorporate some objects.  This can be useful when one
+   wants to work with restricted Coq programs that have only parts of
+   the full capabilities, but may still be able to work correctly for
+   limited purposes.  One example is for the graphical interface, that uses
+   such a limite coq process to do only parsing.  It loads .vo files, but
+   is only interested in loading the grammar rule definitions. *)
+
+let relax_flag = ref false;;
+
+let relax b = relax_flag := b;;
+
+type 'a substitutivity = 
+    Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
+
+
+type 'a object_declaration = {
+  object_name : string;
+  cache_function : object_name * 'a -> unit;
+  load_function : int -> object_name * 'a -> unit;
+  open_function : int -> object_name * 'a -> unit;
+  classify_function : object_name * 'a -> 'a substitutivity;
+  subst_function : object_name * substitution * 'a -> 'a;
+  export_function : 'a -> 'a option }
+
+let yell s = anomaly s
+
+let default_object s = {
+  object_name = s;
+  cache_function = (fun _ -> ());
+  load_function = (fun _ _ -> ());
+  open_function = (fun _ _ -> ());
+  subst_function = (fun _ -> 
+    yell ("The object "^s^" does not know how to substitute!"));
+  classify_function = (fun (_,obj) -> Keep obj);
+  export_function = (fun _ -> None)} 
+
+
+(* The suggested object declaration is the following:
+
+   declare_object { (default_object "MY OBJECT") with
+       cache_function = fun (sp,a) -> Mytbl.add sp a}
+
+   and the listed functions are only those which definitions accually 
+   differ from the default.
+
+   This helps introducing new functions in objects.
+*)
+
+let ident_subst_function (_,_,a) = a
+
+type obj = Dyn.t (* persistent dynamic objects *)
+
+type dynamic_object_declaration = {
+  dyn_cache_function : object_name * obj -> unit;
+  dyn_load_function : int -> object_name * obj -> unit;
+  dyn_open_function : int -> object_name * obj -> unit;
+  dyn_subst_function : object_name * substitution * obj -> obj;
+  dyn_classify_function : object_name * obj -> obj substitutivity;
+  dyn_export_function : obj -> obj option }
+
+let object_tag lobj = Dyn.tag lobj
+
+let cache_tab = 
+  (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
+
+let declare_object odecl =
+  let na = odecl.object_name in
+  let (infun,outfun) = Dyn.create na in
+  let cacher (oname,lobj) =
+    if Dyn.tag lobj = na then odecl.cache_function (oname,outfun lobj)
+    else anomaly "somehow we got the wrong dynamic object in the cachefun"
+  and loader i (oname,lobj) =
+    if Dyn.tag lobj = na then odecl.load_function i (oname,outfun lobj)
+    else anomaly "somehow we got the wrong dynamic object in the loadfun"
+  and opener i (oname,lobj) =
+    if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj)
+    else anomaly "somehow we got the wrong dynamic object in the openfun"
+  and substituter (oname,sub,lobj) = 
+    if Dyn.tag lobj = na then 
+      infun (odecl.subst_function (oname,sub,outfun lobj))
+    else anomaly "somehow we got the wrong dynamic object in the substfun"
+  and classifier (spopt,lobj) = 
+    if Dyn.tag lobj = na then 
+      match odecl.classify_function (spopt,outfun lobj) with
+	| Dispose -> Dispose
+	| Substitute obj -> Substitute (infun obj)
+	| Keep obj -> Keep (infun obj)
+	| Anticipate (obj) -> Anticipate (infun obj)
+    else 
+      anomaly "somehow we got the wrong dynamic object in the classifyfun"
+  and exporter lobj = 
+    if Dyn.tag lobj = na then 
+      option_app infun (odecl.export_function (outfun lobj))
+    else 
+      anomaly "somehow we got the wrong dynamic object in the exportfun"
+
+  in 
+  Hashtbl.add cache_tab na { dyn_cache_function = cacher;
+			     dyn_load_function = loader;
+                             dyn_open_function = opener;
+			     dyn_subst_function = substituter;
+			     dyn_classify_function = classifier;
+                             dyn_export_function = exporter };
+  (infun,outfun)
+
+(* this function describes how the cache, load, open, and export functions
+   are triggered.  In relaxed mode, this function just return a meaningless
+   value instead of raising an exception when they fail. *)
+
+let apply_dyn_fun deflt f lobj =
+  let tag = object_tag lobj in
+    try
+      let dodecl =
+    	try
+	  Hashtbl.find cache_tab tag
+    	with Not_found -> 
+	  if !relax_flag then
+	    failwith "local to_apply_dyn_fun"
+	  else
+	    anomaly
+	      ("Cannot find library functions for an object with tag "^tag) in 
+  	f dodecl
+    with
+	Failure "local to_apply_dyn_fun" -> deflt;;
+
+let cache_object ((_,lobj) as node) =
+  apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj
+
+let load_object i ((_,lobj) as node) = 
+  apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj
+
+let open_object i ((_,lobj) as node) = 
+  apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj
+
+let subst_object ((_,_,lobj) as node) = 
+  apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj
+
+let classify_object ((_,lobj) as node) = 
+  apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj
+
+let 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
new file mode 100644
index 00000000..8a3811e1
--- /dev/null
+++ b/library/libobject.mli
@@ -0,0 +1,105 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: libobject.mli,v 1.9.8.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+
+(*i*)
+open Names
+open Libnames
+(*i*)
+
+(* [Libobject] declares persistent objects, given with methods:
+
+   * a caching function specifying how to add the object in the current
+     scope;
+     If the object wishes to register its visibility in the Nametab, 
+     it should do so for all possible sufixes.
+
+   * a loading function, specifying what to do when the module 
+     containing the object is loaded; 
+     If the object wishes to register its visibility in the Nametab, 
+     it should do so for all sufixes no shorter then the "int" argument
+
+   * an opening function, specifying what to do when the module 
+     containing the object is opened (imported);
+     If the object wishes to register its visibility in the Nametab, 
+     it should do so for the sufix of the length the "int" argument
+
+   * a classification function, specyfying what to do with the object,
+     when the current module (containing the object) is ended;
+     The possibilities are:
+     Dispose   - the object dies at the end of the module
+     Substitue - meaning the object is substitutive and 
+                 the module name must be updated
+     Keep      - the object is not substitutive, but survives module 
+                 closing
+     Anticipate - this is for objects which have to be explicitely 
+                 managed by the end_module function (like Require 
+                 and Read markers)
+
+     The classification function is also an occasion for a cleanup
+     (if this function returns Keep or Substitute of some object, the 
+     cache method is never called for it)
+
+   * a substitution function, performing the substitution; 
+     this function should be declared for substitutive objects 
+     only (see obove)
+
+   * an export function, to enable optional writing of its contents 
+     to disk (.vo). This function is also the oportunity to remove 
+     redundant information in order to keep .vo size small 
+
+     The export function is a little obsolete and will be removed 
+     in the near future... 
+
+*)
+
+type 'a substitutivity = 
+    Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
+
+type 'a object_declaration = {
+  object_name : string;
+  cache_function : object_name * 'a -> unit;
+  load_function : int -> object_name * 'a -> unit;
+  open_function : int -> object_name * 'a -> unit;
+  classify_function : object_name * 'a -> 'a substitutivity;
+  subst_function : object_name * substitution * 'a -> 'a;
+  export_function : 'a -> 'a option }
+
+(* The default object is a "Keep" object with empty methods. 
+   Object creators are advised to use the construction
+   [{(default_object "MY_OBJECT") with
+      cache_function = ...
+   }]
+   and specify only these functions which are not empty/meaningless
+
+*)
+
+val default_object : string -> 'a object_declaration
+
+(* the identity substitution function *)
+val ident_subst_function : object_name * substitution * 'a -> 'a
+
+(*s Given an object declaration, the function [declare_object]
+   will hand back two functions, the "injection" and "projection"
+   functions for dynamically typed library-objects. *)
+
+type obj
+
+val declare_object : 
+  'a object_declaration -> ('a -> obj) * (obj -> 'a)
+
+val object_tag : obj -> string
+
+val cache_object : object_name * obj -> unit
+val load_object : int -> object_name * obj -> unit
+val open_object : int -> object_name * obj -> unit
+val subst_object : object_name * substitution * obj -> obj
+val classify_object : object_name * obj -> obj substitutivity
+val export_object : obj -> obj option
+val relax : bool -> unit
diff --git a/library/library.ml b/library/library.ml
new file mode 100644
index 00000000..0477a8f3
--- /dev/null
+++ b/library/library.ml
@@ -0,0 +1,704 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: library.ml,v 1.79.2.1 2004/07/16 19:30:36 herbelin Exp $ *)
+
+open Pp
+open Util
+
+open Names
+open Libnames
+open Nameops
+open Safe_typing
+open Libobject
+open Lib
+open Nametab
+open Declaremods
+
+(*************************************************************************)
+(*s Load path. Mapping from physical to logical paths etc.*)
+
+type logical_path = dir_path
+
+let load_path = ref ([],[] : System.physical_path list * logical_path list)
+
+let get_load_path () = fst !load_path
+
+(* 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 = canonical_path_name phys_dir in
+  match list_filter2 (fun p d -> p = phys_dir) !load_path with
+  | _,[dir] -> dir
+  | _,[] -> Nameops.default_root_prefix
+  | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
+
+let remove_path dir =
+  load_path := list_filter2 (fun p d -> p <> dir) !load_path
+
+let add_load_path_entry (phys_path,coq_path) =
+  let phys_path = canonical_path_name phys_path in
+  match list_filter2 (fun p d -> p = phys_path) !load_path with
+  | _,[dir] ->
+      if coq_path <> dir 
+        (* If this is not the default -I . to coqtop *)
+        && not
+        (phys_path = canonical_path_name Filename.current_dir_name
+         && coq_path = Nameops.default_root_prefix)
+      then
+	begin
+          (* Assume the user is concerned by library naming *)
+	  if dir <> Nameops.default_root_prefix then
+	    (Options.if_verbose warning (phys_path^" was previously bound to "
+	    ^(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)
+	end
+  | _,[] ->
+      load_path := (phys_path :: fst !load_path, coq_path :: snd !load_path)
+  | _ -> 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 get_full_load_path () = List.combine (fst !load_path) (snd !load_path)
+
+(************************************************************************)
+(*s Modules on disk contain the following informations (after the magic 
+    number, and before the digest). *)
+
+type compilation_unit_name = dir_path
+
+type library_disk = { 
+  md_name : compilation_unit_name;
+  md_compiled : compiled_library;
+  md_objects : library_objects;
+  md_deps : (compilation_unit_name * Digest.t) list;
+  md_imports : compilation_unit_name list }
+
+(*s Modules loaded in memory contain the following informations. They are
+    kept in the global table [libraries_table]. *)
+
+type library_t = {
+  library_name : compilation_unit_name;
+  library_filename : System.physical_path;
+  library_compiled : compiled_library;
+  library_objects : library_objects;
+  library_deps : (compilation_unit_name * Digest.t) list;
+  library_imports : compilation_unit_name list;
+  library_digest : Digest.t }
+
+module CompilingLibraryOrdered = 
+  struct
+    type t = dir_path
+    let compare d1 d2 =
+      Pervasives.compare
+        (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+  end
+
+module CompilingLibraryMap = Map.Make(CompilingLibraryOrdered)
+
+(* This is a map from names to libraries *)
+let libraries_table = ref CompilingLibraryMap.empty
+
+(* These are the _ordered_ lists of loaded, imported and exported libraries *)
+let libraries_loaded_list = ref []
+let libraries_imports_list = ref []
+let libraries_exports_list = ref []
+
+let freeze () =
+  !libraries_table,
+  !libraries_loaded_list,
+  !libraries_imports_list,
+  !libraries_exports_list
+
+let unfreeze (mt,mo,mi,me) = 
+  libraries_table := mt;
+  libraries_loaded_list := mo;
+  libraries_imports_list := mi;
+  libraries_exports_list := me
+
+let init () =
+  libraries_table := CompilingLibraryMap.empty;
+  libraries_loaded_list := [];
+  libraries_imports_list := [];
+  libraries_exports_list := []
+
+let _ = 
+  Summary.declare_summary "MODULES"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_module = false;
+      Summary.survive_section = false }
+
+let find_library s =
+  try
+    CompilingLibraryMap.find s !libraries_table
+  with Not_found ->
+    error ("Unknown library " ^ (string_of_dirpath s))
+
+let library_full_filename m = (find_library m).library_filename
+
+let library_is_loaded dir =
+  try let _ = CompilingLibraryMap.find dir !libraries_table in true
+  with Not_found -> false
+
+let library_is_opened dir = 
+  List.exists (fun m -> m.library_name = dir) !libraries_imports_list
+
+let library_is_exported dir =
+  List.exists (fun m -> m.library_name = dir) !libraries_exports_list
+
+let loaded_libraries () = 
+  List.map (fun m -> m.library_name) !libraries_loaded_list
+
+let opened_libraries () =
+  List.map (fun m -> m.library_name) !libraries_imports_list
+
+  (* If a library is loaded several time, then the first occurrence must
+     be performed first, thus the libraries_loaded_list ... *)
+
+let register_loaded_library m =
+  let rec aux = function
+    | [] -> [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
+
+  (* ... while if a library is imported/exported several time, then
+     only the last occurrence is really needed - though the imported
+     list may differ from the exported list (consider the sequence
+     Export A; Export B; Import A which results in A;B for exports but
+     in B;A for imports) *)
+
+let rec remember_last_of_each l m =
+  match l with
+  | [] -> [m]
+  | m'::l' when m'.library_name = m.library_name -> remember_last_of_each l' m
+  | m'::l' -> m' :: remember_last_of_each l' m
+
+let register_open_library export m =
+  libraries_imports_list := remember_last_of_each !libraries_imports_list m;
+  if export then 
+    libraries_exports_list := remember_last_of_each !libraries_exports_list 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]. *)
+
+let eq_lib_name m1 m2 = m1.library_name = m2.library_name
+
+let open_library export explicit_libs m =
+  if
+    (* Only libraries indirectly to open are not reopen *)
+    (* Libraries explicitly mentionned by the user are always reopen *)
+    List.exists (eq_lib_name m) explicit_libs
+    or not (library_is_opened m.library_name)
+  then begin
+    register_open_library export m;
+    Declaremods.really_import_module (MPfile m.library_name)
+  end
+  else
+    if export then 
+      libraries_exports_list := remember_last_of_each !libraries_exports_list m
+
+let open_libraries export modl = 
+  let to_open_list = 
+    List.fold_left
+      (fun l m ->
+         let subimport =
+           List.fold_left
+             (fun l m -> remember_last_of_each l (find_library m))
+             l m.library_imports
+         in remember_last_of_each subimport m)
+      [] modl in
+  List.iter (open_library export modl) to_open_list
+
+
+(**********************************************************************)
+(* import and export  -  synchronous operations*)
+
+let cache_import (_,(dir,export)) = 
+  open_libraries export [find_library dir]
+
+let open_import i (_,(dir,_) as obj) =
+  if i=1 then
+    (* even if the library is already imported, we re-import it *)
+    (* if not (library_is_opened dir) then *)
+      cache_import obj
+
+let subst_import (_,_,o) = o
+
+let export_import o = Some o
+
+let classify_import (_,(_,export as obj)) = 
+  if export then Substitute obj else Dispose
+
+
+let (in_import, out_import) =
+  declare_object {(default_object "IMPORT LIBRARY") with 
+       cache_function = cache_import;
+       open_function = open_import;
+       subst_function = subst_import;
+       classify_function = classify_import }
+
+
+(************************************************************************)
+(*s Loading from disk to cache (preparation phase) *)
+
+let vo_magic_number7 = 07992 (* V8.0 final old syntax *)
+let vo_magic_number8 = 08002 (* V8.0 final new syntax *)
+
+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"
+
+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 raw_extern_library =
+  if !Options.v7 then raw_extern_library7 else raw_extern_library8
+
+(* cache for loaded libraries *)
+let compunit_cache = ref CompilingLibraryMap.empty
+
+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). *)
+
+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 *)
+  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
+
+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 lighten_library m = 
+  if !Options.dont_load_proofs then lighten_library m else m
+
+let mk_library md f digest = {
+  library_name = md.md_name;
+  library_filename = f;
+  library_compiled = lighten_library md.md_compiled;
+  library_objects = md.md_objects;
+  library_deps = md.md_deps;
+  library_imports = md.md_imports;
+  library_digest = digest }
+
+let intern_from_file f =
+  let ch = with_magic_number_check raw_intern_library f in
+  let md = System.marshal_in ch in
+  let digest = System.marshal_in ch in
+  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
+  with Not_found ->
+  try
+    (* Look if already loaded in cache and consequently its dependencies *)
+    CompilingLibraryMap.find dir !compunit_cache
+  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
+
+and intern_mandatory_library caller (dir,d) =
+  let m = intern_absolute_library_from 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
+
+let rec_intern_library mref = let _ = intern_library mref in ()
+
+let check_library_short_name f dir = function
+  | Some id when id <> snd (split_dirpath dir) ->
+      errorlabstrm "check_library_short_name"
+      (str ("The file " ^ f ^ " contains library") ++ spc () ++
+      pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++
+      pr_id id)
+  | _ -> ()
+
+let rec_intern_by_filename_only id f =
+  let m = intern_from_file f in
+  (* Only the base name is expected to match *)
+  check_library_short_name f m.library_name id;
+  (* We check no other file containing same library is loaded *)
+  try
+    let m' = CompilingLibraryMap.find m.library_name !libraries_table in
+    Options.if_verbose warning 
+      ((string_of_dirpath m.library_name)^" is already loaded from file "^
+       m'.library_filename);
+    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 =
+  (* Look if loaded in current environment *)
+  try 
+    let dir = Nametab.full_name_module qid in
+    (LibLoaded, dir, library_full_filename dir)
+  with Not_found ->
+  (* Look if in loadpath *)
+  try
+    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
+    (LibInPath, extend_dirpath (find_logical_path path) base, 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 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
+  rec_intern_by_filename_only idopt f
+
+(**********************************************************************)
+(*s [require_library] loads and opens a library. This is a synchronized
+    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_* )
+
+  execution phase: (through add_leaf and cache_require)
+    the library is loaded in the environment and Nametab, the objects are 
+    registered etc, using functions from Declaremods (via load_library, 
+    which recursively loads its dependencies)
+
+
+  The [read_library] operation is very similar, but does not "open"
+    the library
+*)
+
+type library_reference = dir_path list * bool option
+
+let string_of_library (_,dir,_) = string_of_id (List.hd (repr_dirpath dir))
+
+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)
+
+  (* 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 (in_require, out_require) =
+  declare_object {(default_object "REQUIRE") with
+       cache_function = cache_require;
+       load_function = load_require;
+       export_function = export_require;
+       classify_function = (fun (_,o) -> Anticipate o) }
+
+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
+    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
+    end
+    else
+      add_anonymous_leaf (in_require (modrefl,Some 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));
+  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) =
+  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))
+      | mp ->
+	  import_module export mp
+  with
+      Not_found ->
+	user_err_loc
+        (loc,"import_library",
+	 str ((string_of_qualid qid)^" is not a module"))
+  
+(************************************************************************)
+(*s [save_library s] saves the library [m] to the disk. *)
+
+let start_library f = 
+  let _,longf = 
+    System.find_file_in_path (get_load_path ()) (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
+
+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 md = { 
+    md_name = s;
+    md_compiled = cenv;
+    md_objects = seg;
+    md_deps = current_deps ();
+    md_imports = current_reexports () } in
+  let (f',ch) = raw_extern_library f in
+  try
+    System.marshal_out ch md;
+    flush ch;
+    let di = Digest.file f' in
+    System.marshal_out ch di;
+    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
+
+let mem s =
+  let m = find_library s in
+  h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)"
+		 (size_kb m) (size_kb m.library_compiled) 
+		 (size_kb m.library_objects)))
diff --git a/library/library.mli b/library/library.mli
new file mode 100644
index 00000000..18be1671
--- /dev/null
+++ b/library/library.mli
@@ -0,0 +1,94 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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*)
+open Util
+open Names
+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]. *)
+
+val read_library : qualid located -> unit
+
+val read_library_from_file : System.physical_path -> unit
+
+(* [import_library true qid] = [export qid] *)
+ 
+val import_library : bool -> qualid located -> unit
+
+val library_is_loaded : dir_path -> bool
+val library_is_opened : dir_path -> bool
+
+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. *)
+
+val library_full_filename : dir_path -> string
+
+
+(*s Global load path *)
+type logical_path = dir_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
+
+exception LibUnmappedDir
+exception LibNotFound
+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. *)
+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
new file mode 100644
index 00000000..ea40aae5
--- /dev/null
+++ b/library/nameops.ml
@@ -0,0 +1,173 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: nameops.ml,v 1.21.2.1 2004/07/16 19:30:36 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+
+(* Identifiers *)
+
+let pr_id id = str (string_of_id id)
+
+let wildcard = id_of_string "_"
+
+(* Utilities *)
+
+let code_of_0 = Char.code '0'
+let code_of_9 = Char.code '9'
+
+let cut_ident skip_quote s =
+  let s = string_of_id s in
+  let slen = String.length s in
+  (* [n'] is the position of the first non nullary digit *)
+  let rec numpart n n' =
+    if n = 0 then 
+      error
+	("The string " ^ s ^ " is not an identifier: it contains only digits or _")
+    else 
+      let c = Char.code (String.get s (n-1)) in
+      if c = code_of_0 && n <> slen then 
+	numpart (n-1) n' 
+      else if code_of_0 <= c && c <= code_of_9 then 
+	numpart (n-1) (n-1)
+      else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then
+	numpart (n-1) (n-1)
+      else
+	n'
+  in
+  numpart slen slen
+
+let repr_ident s =
+  let numstart = cut_ident false s in
+  let s = string_of_id s in
+  let slen = String.length s in
+  if numstart = slen then 
+    (s, None)
+  else
+    (String.sub s 0 numstart,
+     Some (int_of_string (String.sub s numstart (slen - numstart))))
+
+let make_ident sa = function
+  | Some n -> 
+      let c = Char.code (String.get sa (String.length sa -1)) in
+      let s =
+        if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n)
+        else sa ^ "_" ^ (string_of_int n) in
+      id_of_string s
+  | None -> id_of_string (String.copy sa)
+
+let root_of_id id =
+  let suffixstart = cut_ident true id in
+  id_of_string (String.sub (string_of_id id) 0 suffixstart)
+
+(* Rem: semantics is a bit different, if an ident starts with toto00 then
+  after successive renamings it comes to toto09, then it goes on with toto10 *)
+let lift_subscript id =
+  let id = string_of_id id in
+  let len = String.length id in
+  let rec add carrypos =
+    let c = id.[carrypos] in
+    if is_digit c then
+      if c = '9' then begin
+	assert (carrypos>0);
+	add (carrypos-1)
+      end
+      else begin
+	let newid = String.copy id in
+	String.fill newid (carrypos+1) (len-1-carrypos) '0';
+	newid.[carrypos] <- Char.chr (Char.code c + 1);
+	newid
+      end
+    else begin
+      let newid = id^"0" in
+      if carrypos < len-1 then begin
+	String.fill newid (carrypos+1) (len-1-carrypos) '0';
+	newid.[carrypos+1] <- '1'
+      end;
+      newid
+    end
+  in id_of_string (add (len-1))
+
+let has_subscript id =
+  let id = string_of_id id in
+  is_digit (id.[String.length id - 1])
+
+let forget_subscript id =
+  let numstart = cut_ident false id in
+  let newid = String.make (numstart+1) '0' in
+  String.blit (string_of_id id) 0 newid 0 numstart;
+  (id_of_string newid)
+
+let add_suffix id s = id_of_string (string_of_id id ^ s)
+let add_prefix s id = id_of_string (s ^ string_of_id id)
+
+let atompart_of_id id = fst (repr_ident id)
+
+(* Fresh names *)
+
+let lift_ident = lift_subscript
+
+let next_ident_away id avoid = 
+  if List.mem id avoid then
+    let id0 = if not (has_subscript id) then id else 
+    (* Ce serait sans doute mieux avec quelque chose inspiré de 
+       *** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
+    forget_subscript id in
+    let rec name_rec id =
+      if List.mem id avoid then name_rec (lift_ident id) else id in 
+    name_rec id0
+  else id
+
+let next_ident_away_from id avoid = 
+  let rec name_rec id =
+    if List.mem id avoid then name_rec (lift_ident id) else id in 
+  name_rec id 
+
+(* Names *)
+
+let out_name = function
+  | Name id -> id
+  | Anonymous -> anomaly "out_name: expects a defined name"
+
+let name_fold f na a =
+  match na with
+  | Name id -> f id a
+  | Anonymous -> a
+
+let name_cons na l =
+  match na with
+  | Anonymous -> l 
+  | Name id -> id::l
+
+let name_app f = function
+  | Name id -> Name (f id)
+  | Anonymous -> Anonymous
+
+let next_name_away_with_default default name l = 
+  match name with
+    | Name str  -> next_ident_away str l
+    | Anonymous -> next_ident_away (id_of_string default) l
+
+let next_name_away name l = 
+  match name with
+    | Name str  -> next_ident_away str l
+    | Anonymous -> id_of_string "_"
+
+let pr_lab l = str (string_of_label l)
+
+let default_library = Names.initial_dir (* = ["Top"] *)
+
+(*s Roots of the space of absolute names *)
+let coq_root = id_of_string "Coq"
+let default_root_prefix = make_dirpath []
+
+(* Metavariables *)
+let pr_meta = Pp.int
+let string_of_meta = string_of_int
diff --git a/library/nameops.mli b/library/nameops.mli
new file mode 100644
index 00000000..4b7cecda
--- /dev/null
+++ b/library/nameops.mli
@@ -0,0 +1,55 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: nameops.mli,v 1.12.2.1 2004/07/16 19:30:36 herbelin Exp $ *)
+
+open Names
+
+(* Identifiers and names *)
+val pr_id : identifier -> Pp.std_ppcmds
+val wildcard : identifier
+
+val make_ident : string -> int option -> identifier
+val repr_ident : identifier -> string * int option
+
+val atompart_of_id : identifier -> string  (* remove trailing digits *)
+val root_of_id : identifier -> identifier (* remove trailing digits, ' and _ *)
+
+val add_suffix : identifier -> string -> identifier
+val add_prefix : string -> identifier -> identifier
+
+val lift_ident           : identifier -> identifier
+val next_ident_away      : identifier -> identifier list -> identifier
+val next_ident_away_from : identifier -> identifier list -> identifier
+
+val next_name_away : name -> identifier list -> identifier
+val next_name_away_with_default :
+  string -> name -> identifier list -> identifier
+
+val out_name : name -> identifier
+
+val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a
+val name_cons : name -> identifier list -> identifier list
+val name_app : (identifier -> identifier) -> name -> name
+
+val pr_lab : label -> Pp.std_ppcmds
+
+(* some preset paths *)
+
+val default_library : dir_path
+
+(* This is the root of the standard library of Coq *)
+val coq_root : module_ident
+
+(* This is the default root prefix for developments which doesn't
+   mention a root *)
+val default_root_prefix : dir_path
+
+(* Metavariables *)
+val pr_meta : Term.metavariable -> Pp.std_ppcmds
+val string_of_meta : Term.metavariable -> string
diff --git a/library/nametab.ml b/library/nametab.ml
new file mode 100755
index 00000000..f009d867
--- /dev/null
+++ b/library/nametab.ml
@@ -0,0 +1,553 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: nametab.ml,v 1.48.2.1 2004/07/16 19:30:36 herbelin Exp $ *)
+
+open Util
+open Pp
+open Names
+open Libnames
+open Nameops
+open Declarations
+
+
+exception GlobalizationError of qualid
+exception GlobalizationConstantError of qualid
+
+let error_global_not_found_loc loc q =
+  Stdpp.raise_with_loc loc (GlobalizationError q)
+
+let error_global_constant_not_found_loc loc q =
+  Stdpp.raise_with_loc loc (GlobalizationConstantError q)
+
+let error_global_not_found q = raise (GlobalizationError q)
+
+
+
+(* The visibility can be registered either 
+   - for all suffixes not shorter then a given int - when the object
+     is loaded inside a module
+   or
+   - for a precise suffix, when the module containing (the module
+     containing ...) the object is open (imported) 
+*)
+type visibility = Until of int | Exactly of int
+
+
+(* Data structure for nametabs *******************************************)
+
+
+(* This module type will be instantiated by [section_path] of [dir_path] *)
+(* The [repr] function is assumed to return the reversed list of idents. *)
+module type UserName = sig 
+  type t
+  val to_string : t -> string
+  val repr : t -> identifier * module_ident list
+end
+
+
+(* A ['a t] is a map from [user_name] to ['a], with possible lookup by
+   partially qualified names of type [qualid]. The mapping of
+   partially qualified names to ['a] is determined by the [visibility]
+   parameter of [push].
+   
+   The [shortest_qualid] function given a user_name Coq.A.B.x, tries
+   to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes
+   the same object. 
+*)
+module type NAMETREE = sig
+  type 'a t
+  type user_name
+  
+  val empty : 'a t
+  val push : visibility -> user_name -> 'a -> 'a t -> 'a t
+  val locate : qualid -> 'a t -> 'a
+  val find : user_name -> 'a t -> 'a
+  val exists : user_name -> 'a t -> bool
+  val user_name : qualid -> 'a t -> user_name
+  val shortest_qualid : Idset.t -> user_name -> 'a t -> qualid
+  val find_prefixes : qualid -> 'a t -> 'a list
+end
+
+module Make(U:UserName) : NAMETREE with type user_name = U.t 
+				     = 
+struct
+
+  type user_name = U.t
+
+  type 'a path_status = 
+      Nothing 
+    | Relative of user_name * 'a 
+    | Absolute of user_name * 'a
+
+  (* Dictionaries of short names *)
+  type 'a nametree = ('a path_status * 'a nametree ModIdmap.t)
+
+  type 'a t = 'a nametree Idmap.t
+
+  let empty = Idmap.empty
+		
+  (* [push_until] is used to register [Until vis] visibility and 
+     [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*)
+
+  let rec push_until uname o level (current,dirmap) = function
+    | modid :: path as dir ->
+	let mc = 
+	  try ModIdmap.find modid dirmap
+	  with Not_found -> (Nothing, ModIdmap.empty)
+	in
+	let this =
+          if level <= 0 then
+	    match current with
+	      | Absolute (n,_) -> 
+		  (* This is an absolute name, we must keep it 
+		     otherwise it may become unaccessible forever *)
+		  warning ("Trying to mask the absolute name \"" 
+			   ^ U.to_string n ^ "\"!"); 
+		  current
+	      | Nothing
+	      | Relative _ -> Relative (uname,o)
+          else current 
+	in
+	let ptab' = push_until uname o (level-1) mc path in
+	  (this, ModIdmap.add modid ptab' dirmap)
+    | [] -> 
+	match current with
+	  | Absolute (uname',o') -> 
+	      if o'=o then begin
+		assert (uname=uname');
+		current, dirmap 
+		  (* we are putting the same thing for the second time :) *)
+	      end
+	      else
+		(* This is an absolute name, we must keep it otherwise it may
+		   become unaccessible forever *)
+		(* But ours is also absolute! This is an error! *)
+		error ("Cannot mask the absolute name \""
+  		       ^ U.to_string uname' ^ "\"!")
+	  | Nothing
+	  | Relative _ -> Absolute (uname,o), dirmap
+
+
+let rec push_exactly uname o level (current,dirmap) = function
+  | modid :: path as dir ->
+      let mc = 
+	try ModIdmap.find modid dirmap
+	with Not_found -> (Nothing, ModIdmap.empty)
+      in
+        if level = 0 then
+	  let this =
+	    match current with
+	      | Absolute (n,_) -> 
+		  (* This is an absolute name, we must keep it 
+		     otherwise it may become unaccessible forever *)
+		  warning ("Trying to mask the absolute name \""
+  			   ^ U.to_string n ^ "\"!");
+		  current
+	      | Nothing
+	      | Relative _ -> Relative (uname,o)
+	  in
+	    (this, dirmap)
+	else (* not right level *)
+	  let ptab' = push_exactly uname o (level-1) mc path in
+	    (current, ModIdmap.add modid ptab' dirmap)
+  | [] -> 
+      anomaly "Prefix longer than path! Impossible!"
+
+
+let push visibility uname o tab =
+  let id,dir = U.repr uname in
+  let ptab =
+    try Idmap.find id tab
+    with Not_found -> (Nothing, ModIdmap.empty) 
+  in
+  let ptab' = match visibility with
+    | Until i -> push_until uname o (i-1) ptab dir
+    | Exactly i -> push_exactly uname o (i-1) ptab dir
+  in
+    Idmap.add id ptab' tab
+
+
+let rec search (current,modidtab) = function
+  | modid :: path -> search (ModIdmap.find modid modidtab) path
+  | [] -> current
+      
+let find_node qid tab =
+  let (dir,id) = repr_qualid qid in
+    search (Idmap.find id tab) (repr_dirpath dir)
+
+let locate qid tab = 
+  let o = match find_node qid tab with
+    | Absolute (uname,o) | Relative (uname,o) -> o
+    | Nothing -> raise Not_found                                            
+  in
+    o
+
+let user_name qid tab =
+  let uname = match find_node qid tab with
+    | Absolute (uname,o) | Relative (uname,o) -> uname
+    | Nothing -> raise Not_found                                            
+  in
+    uname
+  
+let find uname tab = 
+  let id,l = U.repr uname in
+    match search (Idmap.find id tab) l with
+	Absolute (_,o) -> o
+      | _ -> raise Not_found
+
+let exists uname tab =
+  try 
+    let _ = find uname tab in
+      true
+  with
+      Not_found -> false
+
+let shortest_qualid ctx uname tab = 
+  let id,dir = U.repr uname in
+  let hidden = Idset.mem id ctx in
+  let rec find_uname pos dir (path,tab) = match path with
+    | Absolute (u,_) | Relative (u,_)
+          when u=uname && not(pos=[] && hidden) -> List.rev pos
+    | _ -> 
+	match dir with 
+	    [] -> raise Not_found
+	  | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tab)
+  in
+  let ptab = Idmap.find id tab in
+  let found_dir = find_uname [] dir ptab in
+    make_qualid (make_dirpath found_dir) id
+
+let push_node node l =
+  match node with
+  | Absolute (_,o) | Relative (_,o) when not (List.mem o l) -> o::l
+  | _ -> l
+
+let rec flatten_idmap tab l =
+  ModIdmap.fold (fun _ (current,idtab) l ->
+    flatten_idmap idtab (push_node current l)) tab l
+
+let rec search_prefixes (current,modidtab) = function
+  | modid :: path -> search_prefixes (ModIdmap.find modid modidtab) path
+  | [] -> List.rev (flatten_idmap  modidtab (push_node current []))
+      
+let find_prefixes qid tab =
+  try
+    let (dir,id) = repr_qualid qid in
+    search_prefixes (Idmap.find id tab) (repr_dirpath dir)
+  with Not_found -> []
+
+end
+
+
+
+(* Global name tables *************************************************)
+
+module SpTab = Make (struct 
+		       type t = section_path
+		       let to_string = string_of_path
+		       let repr sp = 
+			 let dir,id = repr_path sp in
+			   id, (repr_dirpath dir)
+		     end)
+
+
+type ccitab = extended_global_reference SpTab.t
+let the_ccitab = ref (SpTab.empty : ccitab)
+
+type kntab = kernel_name SpTab.t
+let the_modtypetab = ref (SpTab.empty : kntab)
+let the_tactictab = ref (SpTab.empty : kntab)
+
+type objtab = unit SpTab.t
+let the_objtab = ref (SpTab.empty : objtab)
+
+
+module DirTab = Make(struct 
+		       type t = dir_path
+		       let to_string = string_of_dirpath
+		       let repr dir = match repr_dirpath dir with
+			 | [] -> anomaly "Empty dirpath"
+			 | id::l -> (id,l)
+		     end)
+
+(* If we have a (closed) module M having a submodule N, than N does not
+   have the entry in [the_dirtab]. *)
+type dirtab = global_dir_reference DirTab.t
+let the_dirtab = ref (DirTab.empty : dirtab)
+
+
+(* Reversed name tables ***************************************************)
+
+(* This table translates extended_global_references back to section paths *)
+module Globrevtab = Map.Make(struct 
+			       type t=extended_global_reference 
+			       let compare = compare 
+			     end)
+
+type globrevtab = section_path Globrevtab.t
+let the_globrevtab = ref (Globrevtab.empty : globrevtab)
+
+
+type mprevtab = dir_path MPmap.t
+let the_modrevtab = ref (MPmap.empty : mprevtab)
+
+type knrevtab = section_path KNmap.t
+let the_modtyperevtab = ref (KNmap.empty : knrevtab)
+let the_tacticrevtab = ref (KNmap.empty : knrevtab)
+
+
+(* Push functions *********************************************************)
+
+(* This is for permanent constructions (never discharged -- but with
+   possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom,
+   Parameter but also Remark and Fact) *)
+
+let push_xref visibility sp xref =
+  the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+  match visibility with
+    | Until _ -> 
+	the_globrevtab := Globrevtab.add xref sp !the_globrevtab
+    | _ -> ()
+
+let push_cci visibility sp ref =
+  push_xref visibility sp (TrueGlobal ref)
+
+(* This is for Syntactic Definitions *)
+let push_syntactic_definition visibility sp kn =
+  push_xref visibility sp (SyntacticDef kn)
+
+let push = push_cci
+
+let push_modtype vis sp kn = 
+  the_modtypetab := SpTab.push vis sp kn !the_modtypetab;
+  the_modtyperevtab := KNmap.add kn sp !the_modtyperevtab
+
+(* This is for tactic definition names *)
+
+let push_tactic vis sp kn = 
+  the_tactictab := SpTab.push vis sp kn !the_tactictab;
+  the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab
+
+
+(* This is for dischargeable non-cci objects (removed at the end of the
+   section -- i.e. Hints, Grammar ...) *) (* --> Unused *)
+
+let push_object visibility sp =
+  the_objtab := SpTab.push visibility sp () !the_objtab
+
+(* This is to remember absolute Section/Module names and to avoid redundancy *)
+let push_dir vis dir dir_ref = 
+  the_dirtab := DirTab.push vis dir dir_ref !the_dirtab;
+  match dir_ref with
+      DirModule (_,(mp,_)) -> the_modrevtab := MPmap.add mp dir !the_modrevtab
+    | _ -> ()
+
+
+(* Locate functions *******************************************************)
+
+
+(* This should be used when syntactic definitions are allowed *)
+let extended_locate qid = SpTab.locate qid !the_ccitab
+
+(* This should be used when no syntactic definitions is expected *)
+let locate qid = match extended_locate qid with
+  | TrueGlobal ref -> ref
+  | SyntacticDef _ -> raise Not_found
+let full_name_cci qid = SpTab.user_name qid !the_ccitab
+
+let locate_syntactic_definition qid = match extended_locate qid with
+  | TrueGlobal _ -> raise Not_found
+  | SyntacticDef kn -> kn
+
+let locate_modtype qid = SpTab.locate qid !the_modtypetab
+let full_name_modtype qid = SpTab.user_name qid !the_modtypetab
+
+let locate_obj qid = SpTab.user_name qid !the_objtab
+
+type ltac_constant = kernel_name
+let locate_tactic qid = SpTab.locate qid !the_tactictab
+let full_name_tactic qid = SpTab.user_name qid !the_tactictab
+
+let locate_dir qid = DirTab.locate qid !the_dirtab
+
+let locate_module qid = 
+  match locate_dir qid with
+    | DirModule (_,(mp,_)) -> mp
+    | _ -> raise Not_found
+
+let full_name_module qid = 
+  match locate_dir qid with
+    | DirModule (dir,_) -> dir
+    | _ -> raise Not_found
+
+let locate_section qid =
+  match locate_dir qid with
+    | DirOpenSection (dir, _) 
+    | DirClosedSection dir -> dir
+    | _ -> raise Not_found
+
+let locate_all qid = 
+  List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l)
+    (SpTab.find_prefixes qid !the_ccitab) []
+
+let extended_locate_all qid = SpTab.find_prefixes qid !the_ccitab
+
+(* Derived functions *)
+
+let locate_constant qid =
+  match extended_locate qid with
+    | TrueGlobal (ConstRef kn) -> kn
+    | _ -> raise Not_found
+
+let locate_mind qid = 
+  match extended_locate qid with
+    | TrueGlobal (IndRef (kn,0)) -> kn
+    | _ -> raise Not_found
+
+
+let absolute_reference sp =
+  match SpTab.find sp !the_ccitab with
+    | TrueGlobal ref -> ref
+    | _ -> raise Not_found
+
+let locate_in_absolute_module dir id =
+  absolute_reference (make_path dir id)
+
+let global r =
+  let (loc,qid) = qualid_of_reference r in
+  try match extended_locate qid with
+    | TrueGlobal ref -> ref
+    | SyntacticDef _ -> 
+        user_err_loc (loc,"global",
+          str "Unexpected reference to a syntactic definition: " ++
+          pr_qualid qid)
+  with Not_found ->
+    error_global_not_found_loc loc qid
+
+(* Exists functions ********************************************************)
+
+let exists_cci sp = SpTab.exists sp !the_ccitab
+      
+let exists_dir dir = DirTab.exists dir !the_dirtab
+
+let exists_section = exists_dir
+
+let exists_module = exists_dir
+
+let exists_modtype sp = SpTab.exists sp !the_modtypetab
+
+let exists_tactic sp = SpTab.exists sp !the_tactictab
+
+(* Reverse locate functions ***********************************************)
+
+let sp_of_global ref = 
+  match ref with
+    | VarRef id -> make_path empty_dirpath id
+    | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
+
+
+let id_of_global ref = 
+  let (_,id) = repr_path (sp_of_global ref) in 
+  id
+
+let sp_of_syntactic_definition kn = 
+  Globrevtab.find (SyntacticDef kn) !the_globrevtab
+
+let dir_of_mp mp =
+  MPmap.find mp !the_modrevtab
+
+
+(* Shortest qualid functions **********************************************)
+
+let shortest_qualid_of_global ctx ref = 
+  match ref with
+    | VarRef id -> make_qualid empty_dirpath id
+    | _ ->
+        let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
+        SpTab.shortest_qualid ctx sp !the_ccitab
+
+let shortest_qualid_of_syndef kn = 
+  let sp = sp_of_syntactic_definition kn in
+    SpTab.shortest_qualid Idset.empty sp !the_ccitab
+
+let shortest_qualid_of_module mp = 
+  let dir = MPmap.find mp !the_modrevtab in
+    DirTab.shortest_qualid Idset.empty dir !the_dirtab
+
+let shortest_qualid_of_modtype kn =
+  let sp = KNmap.find kn !the_modtyperevtab in
+    SpTab.shortest_qualid Idset.empty sp !the_modtypetab
+
+let shortest_qualid_of_tactic kn =
+  let sp = KNmap.find kn !the_tacticrevtab in
+    SpTab.shortest_qualid Idset.empty sp !the_tactictab
+
+let pr_global_env env ref =
+  (* Il est important de laisser le let-in, car les streams s'évaluent
+  paresseusement : il faut forcer l'évaluation pour capturer
+  l'éventuelle levée d'une exception (le cas échoit dans le debugger) *)
+  let s = string_of_qualid (shortest_qualid_of_global env ref) in
+  (str s)
+
+let global_inductive r =
+  match global r with
+  | IndRef ind -> ind
+  | ref ->
+      user_err_loc (loc_of_reference r,"global_inductive",
+        pr_reference r ++ spc () ++ str "is not an inductive type")
+
+(********************************************************************)
+
+(********************************************************************)
+(* Registration of tables as a global table and rollback            *)
+
+type frozen = ccitab * dirtab * objtab * kntab * kntab
+    * globrevtab * mprevtab * knrevtab * knrevtab
+
+let init () = 
+  the_ccitab := SpTab.empty; 
+  the_dirtab := DirTab.empty;
+  the_objtab := SpTab.empty;
+  the_modtypetab := SpTab.empty;
+  the_tactictab := SpTab.empty;
+  the_globrevtab := Globrevtab.empty;
+  the_modrevtab := MPmap.empty;
+  the_modtyperevtab := KNmap.empty;
+  the_tacticrevtab := KNmap.empty
+
+
+let freeze () =
+  !the_ccitab, 
+  !the_dirtab,
+  !the_objtab,
+  !the_modtypetab,
+  !the_tactictab,
+  !the_globrevtab,
+  !the_modrevtab,
+  !the_modtyperevtab,
+  !the_tacticrevtab
+
+let unfreeze (ccit,dirt,objt,mtyt,tact,globr,modr,mtyr,tacr) =
+  the_ccitab := ccit;
+  the_dirtab := dirt;
+  the_objtab := objt;
+  the_modtypetab := mtyt;
+  the_tactictab := tact;
+  the_globrevtab := globr;
+  the_modrevtab := modr;
+  the_modtyperevtab := mtyr;
+  the_tacticrevtab := tacr
+
+let _ = 
+  Summary.declare_summary "names"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_module = false;
+      Summary.survive_section = false }
diff --git a/library/nametab.mli b/library/nametab.mli
new file mode 100755
index 00000000..3a0bd670
--- /dev/null
+++ b/library/nametab.mli
@@ -0,0 +1,171 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: nametab.mli,v 1.43.2.1 2004/07/16 19:30:36 herbelin Exp $ i*)
+
+(*i*)
+open Util
+open Pp
+open Names
+open Libnames
+(*i*)
+
+(*s This module contains the tables for globalization, which
+  associates internal object references to qualified names (qualid). *)
+
+(* Most functions in this module fall into one of the following categories:
+   \begin{itemize}
+   \item [push : visibility -> full_user_name -> object_reference -> unit]
+   
+   Registers the [object_reference] to be referred to by the
+   [full_user_name] (and its suffixes according to [visibility]).
+   [full_user_name] can either be a [section_path] or a [dir_path].
+
+   \item [exists : full_user_name -> bool] 
+   
+   Is the [full_user_name] already atributed as an absolute user name
+   of some object? 
+
+   \item [locate : qualid -> object_reference]
+
+   Finds the object referred to by [qualid] or raises Not_found 
+   
+   \item [name_of] : object_reference -> user_name
+
+   The [user_name] can be for example the shortest non ambiguous [qualid] or 
+   the [full_user_name] or [identifier]. Such a function can also have a 
+   local context argument. 
+*)
+   
+  
+exception GlobalizationError of qualid
+exception GlobalizationConstantError of qualid
+
+(* Raises a globalization error *)
+val error_global_not_found_loc : loc -> qualid -> 'a
+val error_global_not_found     : qualid -> 'a
+val error_global_constant_not_found_loc : loc -> qualid -> 'a
+
+
+
+
+(*s Register visibility of things *)
+
+(* The visibility can be registered either
+   \begin{itemize}
+
+   \item for all suffixes not shorter then a given int -- when the
+   object is loaded inside a module -- or
+
+   \item for a precise suffix, when the module containing (the module
+   containing ...) the object is opened (imported) 
+   \end{itemize}
+*)
+
+type visibility = Until of int | Exactly of int
+
+val push : visibility -> section_path -> global_reference -> unit
+val push_syntactic_definition : 
+  visibility -> section_path -> kernel_name -> unit
+val push_modtype : visibility -> section_path -> kernel_name -> unit
+val push_dir : visibility -> dir_path -> global_dir_reference -> unit
+val push_object : visibility -> section_path -> unit
+val push_tactic : visibility -> section_path -> kernel_name -> unit
+
+
+(*s The following functions perform globalization of qualified names *)
+
+(* This returns the section path of a constant or fails with [Not_found] *)
+val locate : qualid -> global_reference
+
+(* This function is used to transform a qualified identifier into a
+   global reference, with a nice error message in case of failure *)
+val global : reference -> global_reference
+
+(* The same for inductive types *)
+val global_inductive : reference -> inductive
+
+(* This locates also syntactic definitions *)
+val extended_locate : qualid -> extended_global_reference
+
+(* This locates all names with a given suffix, if qualid is valid as
+   such, it comes first in the list *)
+val extended_locate_all : qualid -> extended_global_reference list
+
+(* This locates all global references with a given suffixe *)
+val locate_all : qualid -> global_reference list
+
+val locate_obj : qualid -> section_path
+
+val locate_constant : qualid -> constant
+val locate_mind : qualid -> mutual_inductive
+val locate_section : qualid -> dir_path
+val locate_modtype : qualid -> kernel_name
+val locate_syntactic_definition : qualid -> kernel_name
+
+type ltac_constant = kernel_name
+val locate_tactic : qualid -> ltac_constant
+val locate_dir : qualid -> global_dir_reference
+val locate_module : qualid -> module_path
+
+(* A variant looking up a [section_path] *)
+val absolute_reference : section_path -> global_reference
+
+
+(*s These function tell if the given absolute name is already taken *)
+
+val exists_cci : section_path -> bool
+val exists_modtype : section_path -> bool
+
+(* Those three functions are the same *)
+val exists_dir : dir_path -> bool
+val exists_section : dir_path -> bool (* deprecated *)
+val exists_module : dir_path -> bool (* deprecated *)
+
+
+(*s These functions turn qualids into full user names: [section_path]s
+  or [dir_path]s *)
+
+val full_name_modtype : qualid -> section_path
+val full_name_cci : qualid -> section_path
+
+(* As above but checks that the path found is indeed a module *)
+val full_name_module : qualid -> dir_path
+
+
+(*s Reverse lookup -- finding user names corresponding to the given
+  internal name *)
+
+val sp_of_syntactic_definition : kernel_name -> section_path
+val shortest_qualid_of_global : Idset.t -> global_reference -> qualid
+val shortest_qualid_of_syndef : kernel_name -> qualid
+val shortest_qualid_of_tactic : ltac_constant -> qualid
+
+val dir_of_mp : module_path -> dir_path
+
+val sp_of_global : global_reference -> section_path
+val id_of_global : global_reference -> identifier
+
+(* Printing of global references using names as short as possible *)
+val pr_global_env : Idset.t -> global_reference -> std_ppcmds
+
+
+(* The [shortest_qualid] functions given an object with user_name
+   Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and
+   Coq.A.B.x that denotes the same object. *)
+
+val shortest_qualid_of_module : module_path -> qualid
+val shortest_qualid_of_modtype : kernel_name -> qualid
+
+
+(*
+type frozen
+
+val freeze : unit -> frozen
+val unfreeze : frozen -> unit
+*)
diff --git a/library/states.ml b/library/states.ml
new file mode 100644
index 00000000..7a7f1e06
--- /dev/null
+++ b/library/states.ml
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: states.ml,v 1.8.14.1 2004/07/16 19:30:36 herbelin Exp $ *)
+
+open System
+
+type state = Lib.frozen * Summary.frozen
+
+let get_state () =
+  (Lib.freeze(), Summary.freeze_summaries())
+
+let set_state (fl,fs) =
+  Lib.unfreeze fl;
+  Summary.unfreeze_summaries fs
+
+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))
+
+(* Rollback. *)
+
+let freeze = get_state
+let unfreeze = set_state
+
+let with_heavy_rollback f x =
+  let st = get_state () in
+  try 
+    f x
+  with reraise ->
+    (set_state st; raise reraise)
diff --git a/library/states.mli b/library/states.mli
new file mode 100644
index 00000000..70018180
--- /dev/null
+++ b/library/states.mli
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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*)
+
+(*s States of the system. In that module, we provide functions to get
+  and set the state of the whole system. Internally, it is done by
+  freezing the states of both [Lib] and [Summary]. We provide functions 
+  to write and restore state to and from a given file. *)
+
+val intern_state : string -> unit
+val extern_state : string -> unit
+
+type state
+val freeze : unit -> state
+val unfreeze : state -> unit
+
+(*s Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the
+  state of the whole system as it was before the evaluation if an exception 
+  is raised. *)
+
+val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
+
+
diff --git a/library/summary.ml b/library/summary.ml
new file mode 100644
index 00000000..fc88350a
--- /dev/null
+++ b/library/summary.ml
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: summary.ml,v 1.7.2.1 2004/07/16 19:30:36 herbelin Exp $ *)
+
+open Pp
+open Util
+
+type 'a summary_declaration = {
+  freeze_function : unit -> 'a;
+  unfreeze_function : 'a -> unit;
+  init_function : unit -> unit;
+  survive_module : bool ;
+  survive_section : bool }
+
+let summaries = 
+  (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t)
+
+let internal_declare_summary sumname sdecl =
+  let (infun,outfun) = Dyn.create sumname in
+  let dyn_freeze () = infun (sdecl.freeze_function())
+  and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
+  and dyn_init = sdecl.init_function in
+  let ddecl = {
+    freeze_function = dyn_freeze;
+    unfreeze_function = dyn_unfreeze;
+    init_function = dyn_init;
+    survive_module = sdecl.survive_module;
+    survive_section = sdecl.survive_section } 
+  in
+  if Hashtbl.mem summaries sumname then
+    anomalylabstrm "Summary.declare_summary"
+      (str "Cannot declare a summary twice: " ++ str sumname);
+  Hashtbl.add summaries sumname ddecl
+
+let declare_summary sumname decl = 
+  internal_declare_summary (sumname^"-SUMMARY") decl
+
+type frozen = Dyn.t Stringmap.t
+
+let freeze_summaries () =
+  let m = ref Stringmap.empty in
+  Hashtbl.iter 
+    (fun id decl -> m := Stringmap.add id (decl.freeze_function()) !m)
+    summaries;
+  !m
+
+
+let unfreeze_some_summaries p fs = 
+  Hashtbl.iter
+    (fun id decl -> 
+       try 
+	 if p decl then
+	   decl.unfreeze_function (Stringmap.find id fs)
+       with Not_found -> decl.init_function())
+    summaries
+
+let unfreeze_summaries = 
+  unfreeze_some_summaries (fun _ -> true)
+
+let section_unfreeze_summaries =
+  unfreeze_some_summaries (fun decl -> not decl.survive_section)
+
+let module_unfreeze_summaries =
+  unfreeze_some_summaries (fun decl -> not decl.survive_module)
+
+let init_summaries () =
+  Hashtbl.iter (fun _ decl -> decl.init_function()) summaries
diff --git a/library/summary.mli b/library/summary.mli
new file mode 100644
index 00000000..7e691f0b
--- /dev/null
+++ b/library/summary.mli
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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*)
+
+(* This module registers the declaration of global tables, which will be kept
+   in synchronization during the various backtracks of the system. *)
+
+type 'a summary_declaration = {
+  freeze_function : unit -> 'a;
+  unfreeze_function : 'a -> unit;
+  init_function : unit -> unit;
+  survive_module : bool;    (* should be false is most cases *)
+  survive_section : bool }
+
+val declare_summary : string -> 'a summary_declaration -> unit
+
+type frozen
+
+val freeze_summaries : unit -> frozen
+val unfreeze_summaries : frozen -> unit
+val section_unfreeze_summaries : frozen -> unit
+val module_unfreeze_summaries : frozen -> unit
+val init_summaries : unit -> unit
+
+
+