Correction du bug 335 et Export/Require Export dans un module

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

1 files changed, 3 insertions, 3 deletions

diff --git a/library/summary.mli b/library/summary.mli
index 7ecc5ebf3..23232033a 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -15,17 +15,17 @@ 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
-val declare_global_environment : 'a summary_declaration -> unit
 
 type frozen
 
 val freeze_summaries : unit -> frozen
 val unfreeze_summaries : frozen -> unit
-val unfreeze_lost_summaries : frozen -> unit
-val unfreeze_other_summaries : frozen -> unit
+val section_unfreeze_summaries : frozen -> unit
+val module_unfreeze_summaries : frozen -> unit
 val init_summaries : unit -> unit