Moving centralised discharge into dispatched discharge_function; required to delay some computation from before to after caching time + various simplifications and uniformisations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 307 insertions, 163 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 2109c6325..6bace2654 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -31,11 +31,7 @@ open Decl_kinds
 
 (**********************************************)
 
-(* For [DischargeAt (dir,n)], [dir] is the minimum prefix that a
-   construction keeps in its name (if persistent), or the section name
-   beyond which it is discharged (if volatile); the integer [n]
-   (useful only for persistent constructions), is the length of the section
-   part in [dir] *)
+(* Strength *)
 
 open Nametab
 
@@ -75,13 +71,16 @@ type checked_variable_declaration =
 let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t)
 
 let _ = Summary.declare_summary "VARIABLE"
-	  { Summary.freeze_function = (fun () -> !vartab);
-	    Summary.unfreeze_function = (fun ft -> vartab := ft);
-	    Summary.init_function = (fun () -> vartab := Idmap.empty);
-	    Summary.survive_module = false;
-	    Summary.survive_section = false }
-
-let cache_variable ((sp,_),(id,(p,d,mk))) =
+  { Summary.freeze_function = (fun () -> !vartab);
+    Summary.unfreeze_function = (fun ft -> vartab := ft);
+    Summary.init_function = (fun () -> vartab := Idmap.empty);
+    Summary.survive_module = false;
+    Summary.survive_section = false }
+
+let cache_variable ((sp,_),o) =
+  match o with
+  | Inl cst -> Global.add_constraints cst
+  | Inr (id,(p,d,mk)) ->
   (* Constr raisonne sur les noms courts *)
   if Idmap.mem id !vartab then
     errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
@@ -95,31 +94,33 @@ let cache_variable ((sp,_),(id,(p,d,mk))) =
         let (_,bd,ty) = Global.lookup_named id in
         CheckedSectionLocalDef (out_some bd,ty,cst,opaq) in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
+  add_section_variable id;
+  Dischargedhypsmap.set_discharged_hyps sp [];
   vartab := Idmap.add id (p,vd,mk) !vartab
 
+let get_variable_constraints id = 
+  match pi2 (Idmap.find id !vartab) with
+  | CheckedSectionLocalDef (c,ty,cst,opaq) -> cst
+  | CheckedSectionLocalAssum (ty,cst) -> cst
+
+let discharge_variable (_,o) = match o with
+  | Inr (id,_) -> Some (Inl (get_variable_constraints id))
+  | Inl _ -> Some o
+
 let (in_variable, out_variable) =
   declare_object { (default_object "VARIABLE") with
     cache_function = cache_variable;
+    discharge_function = discharge_variable;
     classify_function = (fun _ -> Dispose) }
 
-let declare_variable_common id obj =
-  let oname = add_leaf id (in_variable (id,obj)) in
-  declare_var_implicits id;
-  Notation.declare_ref_arguments_scope (VarRef id);
-  oname
-
 (* for initial declaration *)
 let declare_variable id obj =
-  let (sp,kn as oname) = declare_variable_common id obj in
+  let oname = add_leaf id (in_variable (Inr (id,obj))) in
+  declare_var_implicits id;
+  Notation.declare_ref_arguments_scope (VarRef id);
   !xml_declare_variable oname;
-  Dischargedhypsmap.set_discharged_hyps sp [];
   oname
 
-(* when coming from discharge: no xml output *)
-let redeclare_variable id discharged_hyps obj =
-  let oname = declare_variable_common id obj in
-  Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps
-
 (* Globals: constants and parameters *)
 
 type constant_declaration = constant_entry * global_kind
@@ -133,37 +134,56 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.survive_module = false;
 	    Summary.survive_section = false }
 
-let cache_constant ((sp,kn),(cdt,kind)) =
-  (if Idmap.mem (basename sp) !vartab then
-    errorlabstrm "cache_constant" 
-      (pr_id (basename sp) ++ str " already exists"));
-  (if Nametab.exists_cci sp then
-    let (_,id) = repr_path sp in
-    errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
-  let _,dir,_ = repr_kn kn in
-  let kn' = Global.add_constant dir (basename sp) cdt in
-    if kn' <> (constant_of_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 (constant_of_kn kn))
+let load_constant i ((sp,kn),(_,_,_,kind)) =
+  if Nametab.exists_cci sp then
+    errorlabstrm "cache_constant" 
+      (pr_id (basename sp) ++ str " already exists");
+  Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn));
+  csttab := Spmap.add sp kind !csttab
 
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn),_) =
   Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn))
 
+let cache_constant ((sp,kn),(cdt,dhyps,imps,kind) as o) =
+  let id = basename sp in
+  let _,dir,_ = repr_kn kn in
+  if Idmap.mem id !vartab then
+    errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+  if Nametab.exists_cci sp then
+    errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
+  let kn' = Global.add_constant dir id cdt in
+  assert (kn' = constant_of_kn kn);
+  Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
+  add_section_constant kn' (Global.lookup_constant kn').const_hyps;
+  Dischargedhypsmap.set_discharged_hyps sp dhyps;
+  with_implicits imps declare_constant_implicits kn';
+  Notation.declare_ref_arguments_scope (ConstRef kn');
+  csttab := Spmap.add sp kind !csttab
+
+(*s Registration as global tables and rollback. *)
+
+open Cooking
+
+let discharged_hyps kn sechyps =
+  let (_,dir,_) = repr_kn kn in
+  let args = array_map_to_list destVar (instance_from_named_context sechyps) in
+  List.rev (List.map (Libnames.make_path dir) args)
+
+let discharge_constant ((sp,kn),(cdt,dhyps,imps,kind)) =
+  let con = constant_of_kn kn in
+  let cb = Global.lookup_constant con in
+  let (repl1,_ as repl) = replacement_context () in
+  let sechyps = section_segment (ConstRef con) in
+  let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in
+  Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,imps,kind)
+
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp)
 
-let dummy_constant (ce,mk) = dummy_constant_entry,mk
+let dummy_constant (ce,_,imps,mk) = dummy_constant_entry,[],imps,mk
 
 let export_constant cst = Some (dummy_constant cst)
 
@@ -176,6 +196,7 @@ let (in_constant, out_constant) =
     open_function = open_constant;
     classify_function = classify_constant;
     subst_function = ident_subst_function;
+    discharge_function = discharge_constant;
     export_function = export_constant } 
 
 let hcons_constant_declaration = function
@@ -188,12 +209,10 @@ let hcons_constant_declaration = function
          const_entry_boxed = ce.const_entry_boxed }
   | cd -> cd
 
-let declare_constant_common id discharged_hyps (cd,kind) =
-  let (sp,kn as oname) = add_leaf id (in_constant (cd,kind)) in
+let declare_constant_common id dhyps (cd,kind) =
+  let imps = implicits_flags () in
+  let (sp,kn as oname) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in
   let kn = constant_of_kn kn in
-  declare_constant_implicits kn;
-  Notation.declare_ref_arguments_scope (ConstRef kn);
-  Dischargedhypsmap.set_discharged_hyps sp discharged_hyps;
   kn
 
 let declare_constant_gen internal id (cd,kind) =
@@ -205,13 +224,15 @@ let declare_constant_gen internal id (cd,kind) =
 let declare_internal_constant = declare_constant_gen true
 let declare_constant = declare_constant_gen false
 
-(* when coming from discharge *)
-let redeclare_constant id discharged_hyps (cd,kind) =
-  let _ = declare_constant_common id discharged_hyps (GlobalRecipe cd,kind) in
-  ()
-
 (* Inductives. *)
 
+let declare_inductive_argument_scopes kn mie =
+  list_iter_i (fun i {mind_entry_consnames=lc} ->
+    Notation.declare_ref_arguments_scope (IndRef (kn,i));
+    for j=1 to List.length lc do
+      Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j));
+    done) mie.mind_entry_inds
+
 let inductive_names sp kn mie =
   let (dp,_) = repr_path sp in
   let names, _ = 
@@ -232,37 +253,43 @@ let inductive_names sp kn mie =
       ([], 0) mie.mind_entry_inds
   in names
 
-
 let check_exists_inductive (sp,_) =
   (if Idmap.mem (basename sp) !vartab then
-    errorlabstrm "cache_inductive" 
+    errorlabstrm ""
       (pr_id (basename sp) ++ str " already exists"));
   if Nametab.exists_cci sp then
     let (_,id) = repr_path sp in
-    errorlabstrm "cache_inductive" (pr_id id ++ str " already exists")
-
-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
+    errorlabstrm "" (pr_id id ++ str " already exists")
 
-let load_inductive i ((sp,kn),mie) =
+let load_inductive i ((sp,kn),(_,_,mie)) =
   let names = inductive_names sp kn mie in
   List.iter check_exists_inductive names;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref) names
 
-let open_inductive i ((sp,kn),mie) =
+let open_inductive i ((sp,kn),(_,_,mie)) =
   let names = inductive_names sp kn mie in
-(*  List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names*)
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
 
+let cache_inductive ((sp,kn),(dhyps,imps,mie)) =
+  let names = inductive_names sp kn mie in
+  List.iter check_exists_inductive names;
+  let id = basename sp in
+  let _,dir,_ = repr_kn kn in
+  let kn' = Global.add_mind dir id mie in
+  assert (kn'=kn);
+  add_section_kn kn (Global.lookup_mind kn').mind_hyps;
+  Dischargedhypsmap.set_discharged_hyps sp dhyps;
+  with_implicits imps declare_mib_implicits kn;
+  declare_inductive_argument_scopes kn mie;
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
+
+let discharge_inductive ((sp,kn),(dhyps,imps,mie)) =
+  let mie = Global.lookup_mind kn in
+  let repl = replacement_context () in
+  let sechyps = section_segment (IndRef (kn,0)) in
+  Some (discharged_hyps kn sechyps,imps,
+        Discharge.process_inductive sechyps repl mie)
+
 let dummy_one_inductive_entry mie = {
   mind_entry_params = [];
   mind_entry_typename = mie.mind_entry_typename;
@@ -272,10 +299,10 @@ let dummy_one_inductive_entry mie = {
 }
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_inductive_entry m = {
+let dummy_inductive_entry (_,imps,m) = ([],imps,{
   mind_entry_record = false;
   mind_entry_finite = true;
-  mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }
+  mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
 
 let export_inductive x = Some (dummy_inductive_entry x)
 
@@ -286,38 +313,19 @@ let (in_inductive, out_inductive) =
     open_function = open_inductive;
     classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a));
     subst_function = ident_subst_function;
+    discharge_function = discharge_inductive;
     export_function = export_inductive } 
 
-let declare_inductive_argument_scopes kn mie =
-  list_iter_i (fun i {mind_entry_consnames=lc} ->
-    Notation.declare_ref_arguments_scope (IndRef (kn,i));
-    for j=1 to List.length lc do
-      Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j));
-    done) mie.mind_entry_inds
-
-let declare_inductive_common mie =
-  let id = match mie.mind_entry_inds with
-    | ind::_ -> ind.mind_entry_typename
-    | [] -> anomaly "cannot declare an empty list of inductives"
-  in
-  let oname = add_leaf id (in_inductive mie) in
-  declare_mib_implicits (snd oname);
-  declare_inductive_argument_scopes (snd oname) mie;
-  oname
-
 (* for initial declaration *)
 let declare_mind isrecord mie =
-  let (sp,kn as oname) = declare_inductive_common mie in
-  Dischargedhypsmap.set_discharged_hyps sp [] ;
+  let imps = implicits_flags () in
+  let id = match mie.mind_entry_inds with
+    | ind::_ -> ind.mind_entry_typename
+    | [] -> anomaly "cannot declare an empty list of inductives" in
+  let oname = add_leaf id (in_inductive ([],imps,mie)) in
   !xml_declare_inductive (isrecord,oname);
   oname
 
-(* when coming from discharge: no xml output *)
-let redeclare_inductive discharged_hyps mie =
- let oname = declare_inductive_common mie in
- Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps ;
- oname
-
 (*s Test and access functions. *)
 
 let is_constant sp = 
@@ -332,12 +340,6 @@ let get_variable id =
     | CheckedSectionLocalDef (c,ty,cst,opaq) -> (id,Some c,ty)
     | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty)
 
-let get_variable_with_constraints id = 
-  let (p,x,_) = Idmap.find id !vartab in
-  match x with
-    | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst)
-    | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst)
-
 let variable_strength _ = Local
 
 let find_section_variable id =
@@ -380,12 +382,6 @@ let mind_oper_of_id sp id mib =
 	   mip.mind_consnames)
     mib.mind_packets
 
-let context_of_global_reference = function
-  | VarRef id -> []
-  | ConstRef sp -> (Global.lookup_constant sp).const_hyps
-  | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps
-  | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps
-
 let last_section_hyps dir =
   fold_named_context
     (fun (id,_,_) sec_ids ->
diff --git a/library/declare.mli b/library/declare.mli
index 6af513888..c141985be 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -40,10 +40,6 @@ 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/... *)
 
@@ -58,21 +54,11 @@ val declare_constant :
 val declare_internal_constant :
   identifier -> constant_declaration -> constant
 
-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
 
@@ -82,10 +68,7 @@ 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
@@ -94,7 +77,6 @@ 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 *)
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index 96ed944b2..0e7bdef30 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -24,13 +24,16 @@ type discharged_hyps = section_path list
 
 let discharged_hyps_map = ref Spmap.empty
 
-let cache_discharged_hyps_map (_,(sp,hyps)) = 
+let load_discharged_hyps_map _ (_,(sp,hyps)) = 
   discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
 
+let cache_discharged_hyps_map o =
+  load_discharged_hyps_map 1 o
+
 let (in_discharged_hyps_map, _) =
   declare_object { (default_object "DISCHARGED-HYPS-MAP") with
     cache_function = cache_discharged_hyps_map;
-    load_function = (fun _ -> cache_discharged_hyps_map);
+    load_function = load_discharged_hyps_map;
     export_function = (fun x -> Some x) }
 
 let set_discharged_hyps sp hyps =
diff --git a/library/impargs.ml b/library/impargs.ml
index 8daf939ef..f41d26c99 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -55,6 +55,14 @@ let is_contextual_implicit_args () = !contextual_implicit_args
 
 type implicits_flags = (bool * bool * bool) * (bool * bool * bool)
 
+let implicits_flags () = 
+  (!implicit_args,
+  !strict_implicit_args,
+  !contextual_implicit_args),
+  (!implicit_args_out,
+  !strict_implicit_args_out,
+  !contextual_implicit_args_out)
+
 let with_implicits ((a,b,c),(d,e,g)) f x =
   let oa = !implicit_args in
   let ob = !strict_implicit_args in
@@ -342,6 +350,16 @@ let compute_var_implicits id =
 let var_implicits id = 
   try Idmap.find id !var_table with Not_found -> No_impl,No_impl
 
+(* Implicits of a global reference. *)
+
+let compute_global_implicits = function
+  | VarRef id -> compute_var_implicits id
+  | ConstRef kn -> compute_constant_implicits kn
+  | IndRef (kn,i) -> 
+      let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps
+  | ConstructRef ((kn,i),j) -> 
+      let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1)
+
 (* Caching implicits *)
 
 let cache_implicits_decl (r,imps) =
@@ -355,7 +373,15 @@ let cache_implicits_decl (r,imps) =
   | ConstructRef consp -> 
       constructors_table := Constrmap.add consp imps !constructors_table
 
-let cache_implicits (_,l) = List.iter cache_implicits_decl l
+let load_implicits _ (_,l) = List.iter cache_implicits_decl l
+
+let cache_implicits o =
+  load_implicits 1 o
+
+(*
+let discharge_implicits (_,(r,imps)) =
+  match r with VarRef _ -> None | _ -> Some (r,compute_global_implicits r)
+*)
 
 let subst_implicits_decl subst (r,imps as o) =
   let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
@@ -366,21 +392,11 @@ let subst_implicits (_,subst,l) =
 let (in_implicits, _) =
   declare_object {(default_object "IMPLICITS") with 
     cache_function = cache_implicits;
-    load_function = (fun _ -> cache_implicits);
+    load_function = load_implicits;
     subst_function = subst_implicits;
     classify_function = (fun (_,x) -> Substitute x);
     export_function = (fun x -> Some x) }
 
-(* Implicits of a global reference. *)
-
-let compute_global_implicits = function
-  | VarRef id -> compute_var_implicits id
-  | ConstRef kn -> compute_constant_implicits kn
-  | IndRef (kn,i) -> 
-      let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps
-  | ConstructRef ((kn,i),j) -> 
-      let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1)
-
 let declare_implicits_gen r = 
   add_anonymous_leaf (in_implicits [r,compute_global_implicits r])
 
diff --git a/library/impargs.mli b/library/impargs.mli
index c1eba6923..212a93a0f 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -64,6 +64,8 @@ val is_implicit_var : variable -> implicits_flags
 
 val implicits_of_global : global_reference -> implicits_list
 
+val implicits_flags : unit -> implicits_flags
+
 (* 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
index babb3863b..548b80d42 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -215,6 +215,7 @@ let is_something_opened = function
   | (_,OpenedModtype _) -> true
   | _ -> false
 
+(*
 let export_segment seg =
   let rec clean acc = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
@@ -229,7 +230,7 @@ let export_segment seg =
     | (_,FrozenState _) :: stk -> clean acc stk
   in
     clean [] seg
-
+*)
 
 let start_module export id mp nametab = 
   let dir = extend_dirpath (fst !path_prefix) id in
@@ -383,6 +384,70 @@ let is_module () =
 (* Returns the most recent OpenedThing node *)
 let what_is_opened () = find_entry_p is_something_opened
 
+(* Discharge tables *)
+
+let sectab =
+  ref ([] : (identifier list *
+             (identifier array Cmap.t * identifier array KNmap.t) *
+             (Sign.named_context Cmap.t * Sign.named_context KNmap.t)) list)
+
+let add_section () =
+  sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
+
+let add_section_variable id =
+  match !sectab with
+    | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
+    | (vars,repl,abs)::sl -> sectab := (id::vars,repl,abs)::sl
+
+let rec extract_hyps = function
+  | (id::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
+  | (id::idl,hyps) -> extract_hyps (idl,hyps)
+  | [], _ -> []
+
+let add_section_replacement f g hyps =
+  match !sectab with
+  | [] -> ()
+  | (vars,exps,abs)::sl ->
+    let sechyps = extract_hyps (vars,hyps) in
+    let args = Sign.instance_from_named_context (List.rev sechyps) in
+    sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl
+	
+let add_section_kn kn =
+  let f = (fun x (l1,l2) -> (l1,KNmap.add kn x l2)) in
+  add_section_replacement f f
+
+let add_section_constant kn =
+  let f = (fun x (l1,l2) -> (Cmap.add kn x l1,l2)) in
+  add_section_replacement f f
+
+let replacement_context () = pi2 (List.hd !sectab)
+
+let section_segment = function
+  | VarRef id ->
+      []
+  | ConstRef con -> 
+      Cmap.find con (fst (pi3 (List.hd !sectab)))
+  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+      KNmap.find kn (snd (pi3 (List.hd !sectab)))
+
+let section_instance r =
+  Sign.instance_from_named_context (List.rev (section_segment r))
+
+let init () = sectab := []
+let freeze () = !sectab
+let unfreeze s = sectab := s
+
+let _ = 
+  Summary.declare_summary "section-context"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_module = false;
+      Summary.survive_section = false }
+
+(*************)
+(* Sections. *)
+
 (* XML output hooks *)
 let xml_open_section = ref (fun id -> ())
 let xml_close_section = ref (fun id -> ())
@@ -390,8 +455,6 @@ let xml_close_section = ref (fun id -> ())
 let set_xml_open_section f = xml_open_section := f
 let set_xml_close_section f = xml_close_section := f
 
-(* Sections. *)
-
 let open_section id =
   let olddir,(mp,oldsec) = !path_prefix in
   let dir = extend_dirpath olddir id in
@@ -405,11 +468,19 @@ let open_section id =
   Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
   path_prefix := prefix;
   if !Options.xml_export then !xml_open_section id;
+  add_section ();
   prefix
 
 
 (* Restore lib_stk and summaries as before the section opening, and
    add a ClosedSection object. *)
+
+let discharge_item = function
+  | ((sp,_ as oname),Leaf lobj) ->
+      option_app (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
+  | _ ->
+      None
+
 let close_section ~export id =
   let oname,fs = 
     try match find_entry_p is_something_opened with
@@ -421,25 +492,31 @@ let close_section ~export id =
     with Not_found ->
       error "no opened section"
   in
-  let (after,_,before) = split_lib oname in
+  let (secdecls,_,before) = split_lib oname in
   lib_stk := before;
-  let prefix = !path_prefix in
+  let full_olddir = fst !path_prefix in
   pop_path_prefix ();
+(*
   let closed_sec = 
-    ClosedSection (export, (fst prefix), export_segment after)
-  in
+    ClosedSection (export, full_olddir, export_segment secdecls) 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)
+  let newdecls = List.map discharge_item secdecls in
+  Summary.section_unfreeze_summaries fs;
+  List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls;
+  Cooking.clear_cooking_sharing ();
+  Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
 
+(*****************)
 (* Backtracking. *)
 
 let recache_decl = function
   | (sp, Leaf o) -> cache_object (sp,o)
+  | (_,OpenedSection _) -> add_section ()
   | _ -> ()
 
-
 let recache_context ctx =
   List.iter recache_decl ctx
 
@@ -475,7 +552,7 @@ let is_mod_node = function
    the same name *) 
 
 let reset_mod (loc,id) =
-  let (ent,before) = 
+  let (_,before) = 
     try
       find_split_p (fun (sp,node) -> 
                     let (_,spi) = repr_path (fst sp) in id = spi 
@@ -583,3 +660,40 @@ let library_part ref =
       else
 	(* Theorem/Lemma outside its outer section of definition *)
 	dir
+
+(************************)
+(* Discharging names *)
+
+let pop_kn kn =
+  let (mp,dir,l) = Names.repr_kn kn in
+  Names.make_kn mp (dirpath_prefix dir) l
+
+let pop_con con = 
+  let (mp,dir,l) = Names.repr_con con in
+  Names.make_con mp (dirpath_prefix dir) l
+
+let con_defined_in_sec kn = 
+  let _,dir,_ = repr_con kn in
+  dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+
+let defined_in_sec kn = 
+  let _,dir,_ = repr_kn kn in
+  dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+
+let discharge_global = function
+  | ConstRef kn when con_defined_in_sec kn ->
+      ConstRef (pop_con kn)
+  | IndRef (kn,i) when defined_in_sec kn ->
+      IndRef (pop_kn kn,i)
+  | ConstructRef ((kn,i),j) when defined_in_sec kn ->
+      ConstructRef ((pop_kn kn,i),j)
+  | r -> r
+
+let discharge_kn kn = 
+  if defined_in_sec kn then pop_kn kn else kn
+
+let discharge_con cst = 
+  if con_defined_in_sec cst then pop_con cst else cst
+
+let discharge_inductive (kn,i) =
+  (discharge_kn kn,i)
diff --git a/library/lib.mli b/library/lib.mli
index 0433897ba..9a4a810ae 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -128,8 +128,7 @@ val library_part : global_reference -> dir_path
 
 val open_section : identifier -> object_prefix
 
-val close_section : export:bool -> identifier -> 
-  object_prefix * library_segment * Summary.frozen
+val close_section : export:bool -> identifier -> unit
 
 (*s Backtracking (undo). *)
 
@@ -157,3 +156,24 @@ val reset_initial : unit -> unit
 (* XML output hooks *)
 val set_xml_open_section : (identifier -> unit) -> unit
 val set_xml_close_section : (identifier -> unit) -> unit
+
+
+(*s Section management for discharge *)
+
+val section_segment : global_reference -> Sign.named_context
+val section_instance : global_reference -> Term.constr array
+
+val add_section_variable : identifier -> unit
+val add_section_constant : constant -> Sign.named_context -> unit
+val add_section_kn : kernel_name -> Sign.named_context -> unit
+val replacement_context : unit ->
+  (identifier array Cmap.t * identifier array KNmap.t)
+
+(*s Discharge: decrease the section level if in the current section *)
+
+val discharge_kn :  kernel_name -> kernel_name
+val discharge_con : constant -> constant
+val discharge_global : global_reference -> global_reference
+val discharge_inductive : inductive -> inductive
+
+
diff --git a/library/libobject.ml b/library/libobject.ml
index 25d5a329f..d84e0bc26 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -36,6 +36,7 @@ type 'a object_declaration = {
   open_function : int -> object_name * 'a -> unit;
   classify_function : object_name * 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
+  discharge_function : object_name * 'a -> 'a option;
   export_function : 'a -> 'a option }
 
 let yell s = anomaly s
@@ -48,6 +49,7 @@ let default_object s = {
   subst_function = (fun _ -> 
     yell ("The object "^s^" does not know how to substitute!"));
   classify_function = (fun (_,obj) -> Keep obj);
+  discharge_function = (fun _ -> None);
   export_function = (fun _ -> None)} 
 
 
@@ -72,6 +74,7 @@ type dynamic_object_declaration = {
   dyn_open_function : int -> object_name * obj -> unit;
   dyn_subst_function : object_name * substitution * obj -> obj;
   dyn_classify_function : object_name * obj -> obj substitutivity;
+  dyn_discharge_function : object_name * obj -> obj option;
   dyn_export_function : obj -> obj option }
 
 let object_tag lobj = Dyn.tag lobj
@@ -104,6 +107,11 @@ let declare_object odecl =
 	| Anticipate (obj) -> Anticipate (infun obj)
     else 
       anomaly "somehow we got the wrong dynamic object in the classifyfun"
+  and discharge (oname,lobj) = 
+    if Dyn.tag lobj = na then 
+      option_app infun (odecl.discharge_function (oname,outfun lobj))
+    else 
+      anomaly "somehow we got the wrong dynamic object in the dischargefun"
   and exporter lobj = 
     if Dyn.tag lobj = na then 
       option_app infun (odecl.export_function (outfun lobj))
@@ -116,6 +124,7 @@ let declare_object odecl =
                              dyn_open_function = opener;
 			     dyn_subst_function = substituter;
 			     dyn_classify_function = classifier;
+			     dyn_discharge_function = discharge;
                              dyn_export_function = exporter };
   (infun,outfun)
 
@@ -154,5 +163,8 @@ let subst_object ((_,_,lobj) as node) =
 let classify_object ((_,lobj) as node) = 
   apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj
 
+let discharge_object ((_,lobj) as node) = 
+  apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
+
 let export_object lobj =
   apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index 37447ffbe..3d60e48ad 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -70,6 +70,7 @@ type 'a object_declaration = {
   open_function : int -> object_name * 'a -> unit;
   classify_function : object_name * 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
+  discharge_function : object_name * 'a -> 'a option;
   export_function : 'a -> 'a option }
 
 (* The default object is a "Keep" object with empty methods. 
@@ -103,4 +104,5 @@ val open_object : int -> object_name * obj -> unit
 val subst_object : object_name * substitution * obj -> obj
 val classify_object : object_name * obj -> obj substitutivity
 val export_object : obj -> obj option
+val discharge_object : object_name * obj -> obj option
 val relax : bool -> unit
diff --git a/library/library.ml b/library/library.ml
index fee383233..09169c4ae 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -554,11 +554,14 @@ let load_require  _ (_,(modl,_)) =
      OS dependent fields from .vo files for cross-platform compatibility *)
 let export_require (l,e) = Some (l,e)
 
+let discharge_require (_,o) = Some o
+
 let (in_require, out_require) =
   declare_object {(default_object "REQUIRE") with
        cache_function = cache_require;
        load_function = load_require;
        export_function = export_require;
+       discharge_function = discharge_require;
        classify_function = (fun (_,o) -> Anticipate o) }
 
 (* Require libraries, import them if [export <> None], mark them for export
diff --git a/library/library.mli b/library/library.mli
index 4ecc76809..bfcc04eb9 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -76,9 +76,3 @@ val locate_qualified_library :
 
 (*s Statistics: display the memory use of a library. *)
 val mem : dir_path -> Pp.std_ppcmds
-
-(*s For discharge *)
-type library_reference
-
-val out_require : Libobject.obj -> library_reference
-val reload_library : library_reference -> unit