- 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

5 files changed, 14 insertions, 17 deletions

diff --git a/library/declare.ml b/library/declare.ml
index b0ec976326..8da7753625 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 457a27f6e2..f7f6f1a510 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 3d87abe4db..7261ba7e66 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 6edc044a4b..cbd4789532 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 7cc35efca3..f289273ece 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