From 79a25a71dd3519d8e7a6bd9f3a004c7c0da3a1b5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 13 Aug 2009 19:10:11 +0000
Subject: Death of "survive_module" and "survive_section" (the first one was
 only used to allow a module to be ended before the summaries were restored
 what can be solved by moving upwards the place where the summaries are
 restored).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/dp/dp.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'plugins/dp')

diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 3a408909d0..17d41ee8b1 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -203,9 +203,7 @@ let () =
     { Summary.freeze_function = (fun () -> !globals, !globals_stack);
       Summary.unfreeze_function = 
 	(fun (g,s) -> globals := g; globals_stack := s);
-      Summary.init_function = (fun () -> ());
-      Summary.survive_module = false;
-      Summary.survive_section = false }
+      Summary.init_function = (fun () -> ()) }
 
 let add_global r d = globals := Refmap.add r d !globals
 let mem_global r = Refmap.mem r !globals
@@ -986,6 +984,4 @@ let _ = declare_summary "Dp options"
 	    init_function = 
 	      (fun () -> 
 		debug := false; trace := false; timeout := 10; 
-		prelude_files := []);
-	    survive_module = true;
-	    survive_section = true }  
+		prelude_files := []) }  
-- 
cgit v1.2.3