- constantes avec recettes

 - discharge en deux temps, avec état remis comme au début de la section
(mais c'est toujours buggé)


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

15 files changed, 223 insertions, 138 deletions

diff --git a/kernel/constant.ml b/kernel/constant.ml
index c93d486fa..dda7274af 100644
--- a/kernel/constant.ml
+++ b/kernel/constant.ml
@@ -7,13 +7,15 @@ open Generic
 open Term
 open Sign
 
-type constant_entry = {
-  const_entry_body : constr;
-  const_entry_type : constr option }
+type lazy_constant_value =
+  | Cooked of constr
+  | Recipe of (unit -> constr)
+
+type constant_value = lazy_constant_value ref
 
 type constant_body = {
   const_kind : path_kind;
-  const_body : constr option;
+  const_body : constant_value option;
   const_type : typed_type;
   const_hyps : typed_type signature;
   const_constraints : constraints;
@@ -23,3 +25,12 @@ let is_defined cb =
   match cb.const_body with Some _ -> true | _ -> false
 
 let is_opaque cb = cb.const_opaque
+
+let cook_constant = function
+  | { contents = Cooked c } -> c
+  | { contents = Recipe f } as v -> let c = f () in v := Cooked c; c
+
+type constant_entry = {
+  const_entry_body : lazy_constant_value;
+  const_entry_type : constr option }
+
diff --git a/kernel/constant.mli b/kernel/constant.mli
index 800f95811..c24280c40 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -10,9 +10,15 @@ open Sign
 
 (* Constants (internal representation). *)
 
+type lazy_constant_value =
+  | Cooked of constr
+  | Recipe of (unit -> constr)
+
+type constant_value = lazy_constant_value ref
+
 type constant_body = {
   const_kind : path_kind;
-  const_body : constr option;
+  const_body : constant_value option;
   const_type : typed_type;
   const_hyps : typed_type signature;
   const_constraints : constraints;
@@ -22,9 +28,11 @@ val is_defined : constant_body -> bool
 
 val is_opaque : constant_body -> bool
 
+val cook_constant : constant_value -> constr
+
 (*s Constant declaration. *)
 
 type constant_entry= {
-  const_entry_body : constr;
+  const_entry_body : lazy_constant_value;
   const_entry_type : constr option }
 
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index f3634eac5..e2afdb2a7 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -43,7 +43,8 @@ let constant_value env k =
   let cb = lookup_constant sp env in
   if not cb.const_opaque & defined_constant env k then
     match cb.const_body with
-      | Some body -> 
+      | Some v -> 
+	  let body = cook_constant v in
           instantiate_constr 
 	    (ids_of_sign cb.const_hyps) body (Array.to_list args)
       | None -> 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index efa860fa2..a4cde0371 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -262,11 +262,11 @@ let push_rels vars env =
 
 (* Insertion of constants and parameters in environment. *)
 
-let add_constant sp ce env =
-  let (jb,cst) = safe_machine env ce.const_entry_body in
+let add_constant_with_value sp body typ env =
+  let (jb,cst) = safe_machine env body in
   let env' = add_constraints cst env in
   let (env'',ty,cst') = 
-    match ce.const_entry_type with
+    match typ with
       | None -> 
 	  env', typed_type_of_judgment env' Evd.empty jb, Constraint.empty
       | Some ty -> 
@@ -281,11 +281,11 @@ let add_constant sp ce env =
 	    error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
   in
   let ids = 
-    Idset.union (global_vars_set ce.const_entry_body) (global_vars_set ty.body)
+    Idset.union (global_vars_set body) (global_vars_set ty.body)
   in
   let cb = { 
     const_kind = kind_of_path sp;
-    const_body = Some ce.const_entry_body;
+    const_body = Some (ref (Cooked body));
     const_type = ty;
     const_hyps = keep_hyps (var_context env) ids;
     const_constraints = Constraint.union cst cst';
@@ -293,6 +293,28 @@ let add_constant sp ce env =
   in
   add_constant sp cb env''
 
+let add_lazy_constant sp f t env =
+  let (jt,cst) = safe_machine env t in
+  let env' = add_constraints cst env in
+  let ids = global_vars_set jt.uj_val in
+  let cb = {
+    const_kind = kind_of_path sp;
+    const_body = Some (ref (Recipe f));
+    const_type = assumption_of_judgment env' Evd.empty jt;
+    const_hyps = keep_hyps (var_context env) ids;
+    const_constraints = cst;
+    const_opaque = false } 
+  in
+  add_constant sp cb env'
+
+let add_constant sp ce env =
+  match ce.const_entry_body with
+    | Cooked c -> add_constant_with_value sp c ce.const_entry_type env
+    | Recipe f -> 
+	(match ce.const_entry_type with
+	   | Some typ -> add_lazy_constant sp f typ env
+	   | None -> error "you cannot declare a lazy constant without type")
+
 let add_parameter sp t env =
   let (jt,cst) = safe_machine env t in
   let env' = add_constraints cst env in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index eae3f77df..314796ee6 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -30,10 +30,14 @@ val push_var : identifier * constr -> safe_environment -> safe_environment
 val push_rel : name * constr -> safe_environment -> safe_environment
 val add_constant : 
   section_path -> constant_entry -> safe_environment -> safe_environment
+val add_lazy_constant : 
+  section_path -> (unit -> constr) -> constr -> safe_environment 
+    -> safe_environment
 val add_parameter :
   section_path -> constr -> safe_environment -> safe_environment
 val add_mind : 
-  section_path -> mutual_inductive_entry -> safe_environment -> safe_environment
+  section_path -> mutual_inductive_entry -> safe_environment 
+    -> safe_environment
 val add_constraints : constraints -> safe_environment -> safe_environment
 
 val lookup_var : identifier -> safe_environment -> name * typed_type
diff --git a/library/declare.ml b/library/declare.ml
index b0ec97632..8da775362 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -98,7 +98,7 @@ let (in_parameter, out_parameter) =
 
 let declare_parameter id c =
   let _ = add_leaf id CCI (in_parameter c) in ()
- 
+
 (* Constants. *)
 
 type constant_declaration = constant_entry * strength
@@ -294,7 +294,8 @@ let declare_eliminations sp i =
   let mindstr = string_of_id (mis_typename mispec) in
   let declare na c =
     declare_constant (id_of_string na)
-      ({ const_entry_body = c; const_entry_type = None }, NeverDischarge);
+      ({ const_entry_body = Cooked c; const_entry_type = None }, 
+       NeverDischarge);
     pPNL [< 'sTR na; 'sTR " is defined" >]
   in
   let env = Global.env () in
diff --git a/library/lib.ml b/library/lib.ml
index 457a27f6e..f7f6f1a51 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -8,8 +8,7 @@ open Summary
 
 type node = 
   | Leaf of obj
-  | OpenedSection of string
-  | ClosedSection of string * library_segment
+  | OpenedSection of string * Summary.frozen
   | FrozenState of Summary.frozen
 
 and library_segment = (section_path * node) list
@@ -101,7 +100,8 @@ let contents_after = function
 
 let open_section s =
   let sp = make_path (id_of_string s) OBJ in
-  add_entry sp (OpenedSection s);
+  let fs = freeze_summaries () in
+  add_entry sp (OpenedSection (s,fs));
   path_prefix := !path_prefix @ [s];
   sp
 
@@ -120,20 +120,18 @@ let open_module s =
 let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
 
 let close_section s =
-  let sp = 
+  let (sp,frozen) = 
     try match find_entry_p is_opened_section with
-      | sp,OpenedSection s' -> 
-	  if s <> s' then error "this is not the last opened section"; sp
+      | sp,OpenedSection (s',fs) -> 
+	  if s <> s' then error "this is not the last opened section"; (sp,fs)
       | _ -> assert false
     with Not_found ->
       error "no opened section"
   in
   let (after,_,before) = split_lib sp in
   lib_stk := before;
-  add_entry sp (ClosedSection (s,after));
-  add_frozen_state ();
   pop_path_prefix ();
-  (sp,after)
+  (sp,after,frozen)
 
 (* The following function exports the whole library segment, that will be 
    saved as a module. Objects are presented in chronological order, and
@@ -145,7 +143,7 @@ let export_module () =
     | [] -> acc
     | (_,Leaf _) as node :: stk -> export (node::acc) stk
     | (_,OpenedSection _) :: _ -> error "there are still opened sections"
-    | (_,(FrozenState _ | ClosedSection _)) :: stk -> export acc stk
+    | (_,FrozenState _) :: stk -> export acc stk
   in
   export [] !lib_stk
 
diff --git a/library/lib.mli b/library/lib.mli
index 3d87abe4d..7261ba7e6 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -13,8 +13,7 @@ open Summary
 
 type node = 
   | Leaf of obj
-  | OpenedSection of string
-  | ClosedSection of string * library_segment
+  | OpenedSection of string * Summary.frozen
   | FrozenState of Summary.frozen
 
 and library_segment = (section_path * node) list
@@ -34,7 +33,7 @@ val contents_after : section_path option -> library_segment
 (*s Opening and closing a section. *)
 
 val open_section : string -> section_path
-val close_section : string -> section_path * library_segment
+val close_section : string -> section_path * library_segment * Summary.frozen
 
 val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> string list
diff --git a/library/library.ml b/library/library.ml
index 6edc044a4..cbd478953 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -62,7 +62,6 @@ let (raw_extern_module, raw_intern_module) =
 let segment_iter f =
   let rec apply = function
     | sp,Leaf obj -> f (sp,obj)
-    | _,ClosedSection (_,mseg) -> iter mseg
     | _,OpenedSection _ -> assert false
     | _,FrozenState _ -> ()
   and iter seg =
diff --git a/library/redinfo.ml b/library/redinfo.ml
index 7cc35efca..f289273ec 100644
--- a/library/redinfo.ml
+++ b/library/redinfo.ml
@@ -68,7 +68,7 @@ let constant_eval sp =
       let cb = Global.lookup_constant sp in
       match cb.const_body with
 	| None -> NotAnElimination
-	| Some c -> compute_consteval c
+	| Some v -> let c = cook_constant v in compute_consteval c
     in
     eval_table := Spmap.add sp v !eval_table;
     v
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index f12f5edec..848a2132e 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -49,7 +49,8 @@ let print_typed_value_in_env env (trm,typ) =
 let print_typed_value x = print_typed_value_in_env (Global.env ()) x
 			  		  
 let print_recipe = function
-  | Some c -> prterm c
+  | Some { contents = Cooked c } -> prterm c
+  | Some { contents = Recipe _ } -> [< 'sTR"<recipe>" >]
   | None -> [< 'sTR"<uncookable>" >]
 
 let fprint_recipe = function
@@ -280,13 +281,7 @@ let rec print_library_entry with_values ent =
   match ent with
     | (sp,Lib.Leaf lobj) -> 
 	[< print_leaf_entry with_values sep (sp,lobj) >]
-    | (s,Lib.ClosedSection(_,ctxt)) ->
-	[< 'sTR"Closed Section " ; 'sTR (string_of_path s) ; 'fNL ;
-	   if !print_closed_sections then
-             [< 'sTR " " ; hOV 0 [< print_context with_values ctxt >] >]
-	   else 
-	     [< >] >]
-    | (_,Lib.OpenedSection str) -> 
+    | (_,Lib.OpenedSection (str,_)) -> 
         [< 'sTR(" >>>>>>> Section " ^ str) ; 'fNL >]
     | (_,Lib.FrozenState _) ->
 	[< >]
@@ -379,8 +374,7 @@ let crible (fn:string -> unit assumptions -> constr -> unit) name =
                crible_rec rest
 	   | _ -> crible_rec rest)
 
-    | (_, (Lib.OpenedSection _ | Lib.ClosedSection _ 
-	  | Lib.FrozenState _))::rest -> 
+    | (_, (Lib.OpenedSection _ | Lib.FrozenState _))::rest -> 
 	crible_rec rest
     | []      -> ()
   in 
@@ -396,7 +390,7 @@ let print_crible name =
 
 let read_sec_context sec =
   let rec get_cxt in_cxt = function
-    | ((sp,Lib.OpenedSection str) as hd)::rest ->
+    | ((sp,Lib.OpenedSection (str,_)) as hd)::rest ->
         if str = sec then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
     | [] -> []
     | hd::rest -> get_cxt (hd::in_cxt) rest 
@@ -495,7 +489,6 @@ let print_local_context () =
                [< print_last_const rest;print_mutual sp mib; 'fNL >]
            | "VARIABLE" ->  [< >]
            | _          ->  print_last_const rest)
-    | (sp,Lib.ClosedSection _)::rest -> print_last_const rest
     | _ -> [< >]
   in 
   [< print_var_rec env;  print_last_const env >]
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 12f53c685..e2f5ce94b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -175,7 +175,8 @@ let save_named opacity =
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in 
   declare_constant (id_of_string ident)
-    ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength);
+    ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl }, 
+     strength);
   del_proof ident;
   message(ident ^ " is defined")
     
@@ -187,11 +188,13 @@ let save_anonymous opacity save_ident n =
   let pfterm = extract_pftreestate pfs in 
   if ident = "Unnamed_thm" then
     declare_constant (id_of_string save_ident)
-      ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength)
+      ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl }, 
+       strength)
   else begin
     message("Overriding name " ^ ident ^ " and using " ^ save_ident);
     declare_constant (id_of_string save_ident)
-      ({ const_entry_body = pfterm; const_entry_type = Some concl }, strength)
+      ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl }, 
+       strength)
   end;
   del_proof ident;
   message(save_ident ^ " is defined")
diff --git a/toplevel/class.ml b/toplevel/class.ml
index d4cd6fec6..7912b2fdf 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -289,7 +289,8 @@ let build_id_coercion idf_opt ids =
 	  id_of_string ("Id_"^(string_of_id ids)^"_"^
                         (string_of_cl (fst (constructor_at_head t)))) 
   in
-  let constr_entry = {const_entry_body = constr_f; const_entry_type = None } in
+  let constr_entry = 
+    { const_entry_body = Cooked constr_f; const_entry_type = None } in
   declare_constant idf (constr_entry,NeverDischarge);
   idf
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 882033919..776864d70 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -32,10 +32,10 @@ let constant_entry_of_com com =
   let env = Global.env() in
   match com with
     | Node(_,"CAST",[_;t]) ->
-        { const_entry_body = constr_of_com sigma env com;
+        { const_entry_body = Cooked (constr_of_com sigma env com);
 	  const_entry_type = Some (constr_of_com1 true sigma env t) }
     | _ -> 
-	{ const_entry_body = constr_of_com sigma env com;
+	{ const_entry_body = Cooked (constr_of_com sigma env com);
 	  const_entry_type = None }
 
 let definition_body ident n com = 
@@ -44,9 +44,13 @@ let definition_body ident n com =
 
 let red_constant_entry ce = function
   | None -> ce
-  | Some red -> 
+  | Some red ->
+      let body = match ce.const_entry_body with
+	| Cooked c -> c
+	| Recipe _ -> assert false
+      in
       { const_entry_body = 
-	  reduction_of_redexp red (Global.env()) Evd.empty ce.const_entry_body;
+	  Cooked (reduction_of_redexp red (Global.env()) Evd.empty body); 
 	const_entry_type = 
 	  ce.const_entry_type }
 
@@ -233,9 +237,11 @@ let build_recursive lnameargsardef =
     let varrec = Array.of_list larrec in
     let rec declare i = function 
       | fi::lf ->
-	  let ce = { const_entry_body = 
-		       mkFixDlam (Array.of_list nvrec) i varrec recvec;
-		     const_entry_type = None } in
+	  let ce = 
+	    { const_entry_body =
+		Cooked (mkFixDlam (Array.of_list nvrec) i varrec recvec);
+	      const_entry_type = None } 
+	  in
 	  declare_constant fi (ce, n);
           declare (i+1) lf
       | _ -> () 
@@ -249,7 +255,7 @@ let build_recursive lnameargsardef =
   let _ = 
     List.fold_left
       (fun subst (f,def) ->
-	 let ce = { const_entry_body = Generic.replace_vars subst def;
+	 let ce = { const_entry_body = Cooked (Generic.replace_vars subst def);
 		    const_entry_type = None } in
 	 declare_constant f (ce,n);
       	 warning ((string_of_id f)^" is non-recursively defined");
@@ -297,9 +303,11 @@ let build_corecursive lnameardef =
     in
     let rec declare i = function 
       | fi::lf ->
-	  let ce = { const_entry_body = 
-		       mkCoFixDlam i (Array.of_list larrec) recvec;
-		     const_entry_type = None } in
+	  let ce = 
+	    { const_entry_body = 
+		Cooked (mkCoFixDlam i (Array.of_list larrec) recvec);
+	      const_entry_type = None } 
+	  in
           declare_constant fi (ce,n);
           declare (i+1) lf
       | _        -> () 
@@ -312,7 +320,7 @@ let build_corecursive lnameardef =
   let _ = 
     List.fold_left
       (fun subst (f,def) ->
-	 let ce = { const_entry_body = Generic.replace_vars subst def;
+	 let ce = { const_entry_body = Cooked (Generic.replace_vars subst def);
 		    const_entry_type = None } in
 	 declare_constant f (ce,n);
       	 warning ((string_of_id f)^" is non-recursively defined");
@@ -337,7 +345,8 @@ let build_scheme lnamedepindsort =
   let rec declare i = function 
     | fi::lf -> 
 	let ce = 
-	  { const_entry_body = listdecl.(i); const_entry_type = None } in
+	  { const_entry_body = Cooked listdecl.(i); const_entry_type = None } 
+	in
 	declare_constant fi (ce,n);
         declare (i+1) lf
     | _        -> ()
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 84b357c5d..f0a97c218 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -74,7 +74,14 @@ let abstract_constant ids_to_abs hyps (body,typ) =
       let name = Name id in
       let var = snd (hd_sign hyps) in
       let cvar = incast_type var in
-      let body' = mkLambda name cvar (subst_var id body) in
+      let body' = match body with
+	| None -> None
+	| Some { contents = Cooked c } -> 
+	    Some (ref (Cooked (mkLambda name cvar (subst_var id c))))
+	| Some { contents = Recipe f } ->
+	    Some (ref (Recipe 
+			 (fun () -> mkLambda name cvar (subst_var id (f())))))
+      in
       let typ' =
     	{ body = mkProd name cvar (subst_var id typ.body);
 	  typ  = sort_of_product_without_univ var.typ typ.typ } 
@@ -88,29 +95,21 @@ let abstract_constant ids_to_abs hyps (body,typ) =
 
 (* Substitutions. *)
 
-let expmod_constr modlist c =
-  let env = Global.env() in
+let expmod_constr oldenv modlist c =
   let sigma = Evd.empty in
-  let simpfun = if modlist = [] then fun x -> x else nf_betaiota env sigma in
-  let expfun c = 
-    let (sp,_) = destConst c in 
+  let simpfun = 
+    if modlist = [] then fun x -> x else nf_betaiota oldenv sigma in
+  let expfun cst = 
     try 
-      constant_value env c
-    with Failure _ -> begin
-      mSGERRNL 
+      constant_value oldenv cst
+    with Failure _ ->
+      let (sp,_) = destConst cst in
+      errorlabstrm "expmod_constr"
 	[< 'sTR"Cannot unfold the value of " ;
            'sTR(string_of_path sp) ; 'sPC;
            'sTR"You cannot declare local lemmas as being opaque"; 'sPC;
            'sTR"and then require that theorems which use them"; 'sPC;
            'sTR"be transparent" >];
-      let cb = Global.lookup_constant sp in
-      cb.const_opaque <- false;
-      (try
-         let v = constant_value env c in 
-	 cb.const_opaque <- true; 
-	 v
-       with _ -> anomaly "expmod_constr")
-    end
   in
   let under_casts f = function
     | DOP2(Cast,c,t) -> (DOP2(Cast,f c,f t))
@@ -118,27 +117,34 @@ let expmod_constr modlist c =
   in
   let c' = modify_opers expfun (fun a b -> mkAppL [|a; b|]) modlist c in
   match c' with
-    | DOP2(Cast,val_0,typ) -> DOP2(Cast,simpfun val_0,simpfun typ)
-    | DOP2(XTRA "IND",c,DLAMV(na,lc)) ->
-	DOP2(XTRA "IND",under_casts simpfun c,
-             DLAMV(na,Array.map (under_casts simpfun) lc))
+    | DOP2 (Cast,val_0,typ) -> DOP2 (Cast,simpfun val_0,simpfun typ)
     | _ -> simpfun c'
 
-let expmod_type modlist {body=c;typ=s} = {body=expmod_constr modlist c;typ=s}
+let expmod_type oldenv modlist {body=c;typ=s} = 
+  { body = expmod_constr oldenv modlist c; typ = s }
 
+let expmod_constant_value opaque oldenv modlist = function
+  | None -> None
+  | Some { contents = Cooked c } -> 
+      if opaque then 
+	Some (ref (Recipe (fun () -> expmod_constr oldenv modlist c)))
+      else
+	Some (ref (Cooked (expmod_constr oldenv modlist c)))
+  | Some { contents = Recipe f } -> 
+      Some (ref (Recipe (fun () -> expmod_constr oldenv modlist (f ()))))
 
 (* Discharge of inductive types. *)
 
-let process_inductive osecsp nsecsp (ids_to_discard,modlist) mib =
+let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
   assert (Array.length mib.mind_packets > 0);
   let finite = mib.mind_packets.(0).mind_finite in
   let inds = 
     array_map_to_list
       (fun mip ->
 	 (mip.mind_typename,
-	  expmod_type modlist mip.mind_arity,
+	  expmod_type oldenv modlist mip.mind_arity,
 	  Array.to_list mip.mind_consnames,
-	  under_dlams (expmod_constr modlist) mip.mind_lc))
+	  under_dlams (expmod_constr oldenv modlist) mip.mind_lc))
       mib.mind_packets
   in
   let (inds',modl) = abstract_inductive ids_to_discard mib.mind_hyps inds in
@@ -162,22 +168,22 @@ let process_inductive osecsp nsecsp (ids_to_discard,modlist) mib =
 
 (* Discharge of constants. *)
 
-let process_constant osecsp nsecsp (ids_to_discard,modlist) cb =
-  let body = global_reference CCI (basename osecsp) in
-  let typ = expmod_type modlist cb.const_type in
+let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb =
+  let body = 
+    expmod_constant_value cb.const_opaque oldenv modlist cb.const_body in
+  let typ = expmod_type oldenv modlist cb.const_type in
   let (body',typ',modl) = 
     abstract_constant ids_to_discard cb.const_hyps (body,typ)
   in
   let mods = (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) :: modlist in
-  ({ const_entry_body = body'; const_entry_type = Some typ'.body },
-   mods)
+  (body', typ'.body, mods)
 
 
 (* Discharge of the various objects of the environment. *)
 
-let constant_message sp =
+let constant_message id =
   if Options.verbose() then 
-    pPNL [< print_id (basename sp); 'sTR " is discharged." >]
+    pPNL [< print_id id; 'sTR " is discharged." >]
 
 let inductive_message inds =
   if Options.verbose() then 
@@ -189,74 +195,80 @@ let inductive_message inds =
 			   (fun (id,_,_,_) -> print_id id) l;
 			 'sPC; 'sTR "are discharged.">]))
 
-let process_object sec_sp (ids_to_discard,work_alist) (sp,lobj) =
+type discharge_operation = 
+  | Variable of identifier * constr * strength * bool
+  | Parameter of identifier * constr
+  | Constant of identifier * constant_entry * strength
+  | Inductive of mutual_inductive_entry
+  | Class of cl_typ * cl_info_typ
+  | Struc of section_path * struc_typ
+  | Coercion of ((coe_typ * coe_info_typ) * cl_typ * cl_typ) 
+              * identifier * int 
+
+let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
   let tag = object_tag lobj in 
   match tag with
     | "VARIABLE" ->
 	let (id,a,stre,sticky) = out_variable sp in
 	if stre = (DischargeAt sec_sp) or ids_to_discard <> [] then
-	  (id::ids_to_discard,work_alist)
-	else begin
-	  let expmod_a = expmod_constr work_alist a.body in
-	  declare_variable id (expmod_a,stre,sticky);
-          (ids_to_discard,work_alist)
-	end
+	  (ops,id::ids_to_discard,work_alist)
+	else
+	  let expmod_a = expmod_constr oldenv work_alist a.body in
+	  (Variable (id,expmod_a,stre,sticky) :: ops,
+           ids_to_discard,work_alist)
 
     | "CONSTANT" ->
 	let stre = constant_strength sp in
 	if stre = (DischargeAt sec_sp) then
-	  (ids_to_discard, (Const sp, DO_REPLACE) :: work_alist)
-	else begin
-	  let cb = Global.lookup_constant sp in
+	  (ops, ids_to_discard, (Const sp, DO_REPLACE) :: work_alist)
+	else
+	  let cb = Environ.lookup_constant sp oldenv in
 	  let spid = basename sp in
 	  let newsp = recalc_sp sp in
-	  let (ce,mods) = 
-	    process_constant sp newsp (ids_to_discard,work_alist) cb in
-	  declare_constant spid (ce,stre);
-	  constant_message sp;
-          (ids_to_discard,mods@work_alist)
-	end
+	  let (body,typ,mods) = 
+	    process_constant sp newsp oldenv (ids_to_discard,work_alist) cb in
+	  let op = match body with
+	    | None -> 
+		Parameter (spid,typ)
+	    | Some { contents = b } -> 
+		let ce = 
+		  { const_entry_body = b; const_entry_type = Some typ } in
+		Constant (spid,ce,stre)
+	  in
+          (op::ops, ids_to_discard, mods@work_alist)
   
     | "INDUCTIVE" ->
-	let mib = Global.lookup_mind sp in
+	let mib = Environ.lookup_mind sp oldenv in
 	let newsp = recalc_sp sp in
 	let (mie,mods) = 
-	  process_inductive sp newsp (ids_to_discard,work_alist) mib in
-	let _ = declare_mind mie in
-	inductive_message mie.mind_entry_inds;
-        (ids_to_discard,mods@work_alist)
+	  process_inductive sp newsp oldenv (ids_to_discard,work_alist) mib in
+        ((Inductive mie)::ops, ids_to_discard, mods@work_alist)
 
     | "CLASS" -> 
 	let ((cl,clinfo) as x) = outClass lobj in
 	if clinfo.cL_STRE = (DischargeAt sec_sp) then 
-	  (ids_to_discard,work_alist)
-	else begin 
-	  let y = process_class sec_sp x in
-          Lib.add_anonymous_leaf (inClass y);
-          (ids_to_discard,work_alist)
-	end
+	  (ops,ids_to_discard,work_alist)
+	else
+	  let (y1,y2) = process_class sec_sp x in
+          ((Class (y1,y2))::ops, ids_to_discard, work_alist)
 	  
     | "COERCION" -> 
 	let (((_,coeinfo),_,_)as x) = outCoercion lobj in
         if coeinfo.cOE_STRE = (DischargeAt sec_sp) then 
-	  (ids_to_discard,work_alist)
-        else begin 
-	  let ((_,_,clt) as y),idf,ps = process_coercion sec_sp x in
-          Lib.add_anonymous_leaf (inCoercion y); 
-          coercion_syntax idf ps clt;
-          (ids_to_discard,work_alist)
-	end
+	  (ops,ids_to_discard,work_alist)
+        else
+	  let (y,idf,ps) = process_coercion sec_sp x in
+          ((Coercion (y,idf,ps))::ops, ids_to_discard, work_alist)
                     
     | "STRUCTURE" ->
 	let (sp,info) = outStruc lobj in
 	let newsp = recalc_sp sp in
-	let mib = Global.lookup_mind (ccisp_of newsp) in
+	let mib = Environ.lookup_mind newsp oldenv in
 	let strobj =
-	  { s_CONST= info.s_CONST;
-	    s_PARAM= mib.mind_nparams;
-	    s_PROJ= List.map (option_app recalc_sp) info.s_PROJ} in
-	Lib.add_anonymous_leaf (inStruc (newsp,strobj));
-	(ids_to_discard,work_alist)
+	  { s_CONST = info.s_CONST;
+	    s_PARAM = mib.mind_nparams;
+	    s_PROJ = List.map (option_app recalc_sp) info.s_PROJ } in
+	((Struc (newsp,strobj))::ops, ids_to_discard, work_alist)
 
     (***TODO
     | "OBJDEF1" -> 
@@ -266,14 +278,38 @@ let process_object sec_sp (ids_to_discard,work_alist) (sp,lobj) =
         (ids_to_discard,work_alist)
     ***)
 
-    | _ -> 
-	(ids_to_discard,work_alist)
+    | _ -> (ops,ids_to_discard,work_alist)
 
-let process_item sec_sp acc = function
-  | (sp,Leaf lobj) -> process_object sec_sp acc (sp,lobj)
+let process_item oldenv sec_sp acc = function
+  | (sp,Leaf lobj) -> process_object oldenv sec_sp acc (sp,lobj)
   | (_,_) -> acc
 
+let process_operation = function
+  | Variable (id,expmod_a,stre,sticky) ->
+      declare_variable id (expmod_a,stre,sticky)
+  | Parameter (spid,typ) ->
+      declare_parameter spid typ;
+      constant_message spid
+  | Constant (spid,ce,stre) ->
+      declare_constant spid (ce,stre);
+      constant_message spid
+  | Inductive mie ->
+      let _ = declare_mind mie in
+      inductive_message mie.mind_entry_inds
+  | Class (y1,y2) ->
+      Lib.add_anonymous_leaf (inClass (y1,y2))
+  | Struc (newsp,strobj) ->
+      Lib.add_anonymous_leaf (inStruc (newsp,strobj))
+  | Coercion ((_,_,clt) as y,idf,ps) ->
+      Lib.add_anonymous_leaf (inCoercion y); 
+      coercion_syntax idf ps clt
+
 let close_section _ s = 
-  let (sec_sp,decls) = close_section s in
-  let _ = List.fold_left (process_item sec_sp) ([],[]) decls in 
-  ()
+  let oldenv = Global.env() in
+  let (sec_sp,decls,frozen) = close_section s in
+  let (ops,_,_) = 
+    List.fold_left (process_item oldenv sec_sp) ([],[],[]) decls in 
+  Summary.unfreeze_summaries frozen;
+  List.iter process_operation (List.rev ops)
+
+