From 12965209478bd99dfbe57f07d5b525e51b903f22 Mon Sep 17 00:00:00 2001
From: coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 2 Aug 2002 17:17:42 +0000
Subject: Modules dans COQ\!\!\!\!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/summary.ml | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

(limited to 'library/summary.ml')

diff --git a/library/summary.ml b/library/summary.ml
index 210a1a81b..59560af22 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -10,7 +10,6 @@
 
 open Pp
 open Util
-open Names
 
 type 'a summary_declaration = {
   freeze_function : unit -> 'a;
@@ -21,8 +20,8 @@ type 'a summary_declaration = {
 let summaries = 
   (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t)
 
-let declare_summary sumname sdecl =
-  let (infun,outfun) = Dyn.create (sumname^"-SUMMARY") in
+let internal_declare_summary sumname sdecl =
+  let (infun,outfun) = Dyn.create sumname in
   let dyn_freeze () = infun (sdecl.freeze_function())
   and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
   and dyn_init = sdecl.init_function in
@@ -37,6 +36,14 @@ let declare_summary sumname sdecl =
       (str "Cannot declare a summary twice: " ++ str sumname);
   Hashtbl.add summaries sumname ddecl
 
+let declare_summary sumname decl = 
+  internal_declare_summary (sumname^"-SUMMARY") decl
+
+let envsummary = "Global environment SUMMARY"
+
+let declare_global_environment sdecl = 
+  internal_declare_summary envsummary sdecl
+
 type frozen = Dyn.t Stringmap.t
 
 let freeze_summaries () =
@@ -62,5 +69,14 @@ let unfreeze_lost_summaries fs =
        with Not_found -> decl.init_function())
     summaries
 
+let unfreeze_other_summaries fs = 
+  Hashtbl.iter
+    (fun id decl -> 
+       try 
+	 if id <> envsummary then
+	   decl.unfreeze_function (Stringmap.find id fs)
+       with Not_found -> decl.init_function())
+    summaries
+
 let init_summaries () =
   Hashtbl.iter (fun _ decl -> decl.init_function()) summaries
-- 
cgit v1.2.3