certains effets disparaissent a la sortie des sections, d'autres non (selon Summary.survive_section)

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

1 files changed, 3 insertions, 1 deletions

diff --git a/library/summary.mli b/library/summary.mli
index 0d329a947..fc639d7f8 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -11,7 +11,8 @@ open Names
 type 'a summary_declaration = {
   freeze_function : unit -> 'a;
   unfreeze_function : 'a -> unit;
-  init_function : unit -> unit }
+  init_function : unit -> unit;
+  survive_section : bool }
 
 val declare_summary : string -> 'a summary_declaration -> unit
 
@@ -19,6 +20,7 @@ type frozen
 
 val freeze_summaries : unit -> frozen
 val unfreeze_summaries : frozen -> unit
+val unfreeze_lost_summaries : frozen -> unit
 val init_summaries : unit -> unit