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/extraction/table.ml | 16 ++++------------
 1 file changed, 4 insertions(+), 12 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index e6d6344665..7a265b526f 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -421,9 +421,7 @@ let (extr_lang,_) =
 let _ = declare_summary "Extraction Lang"
 	  { freeze_function = (fun () -> !lang_ref);
 	    unfreeze_function = ((:=) lang_ref);
-	    init_function = (fun () -> lang_ref := Ocaml);
-	    survive_module = true;
-	    survive_section = true }
+	    init_function = (fun () -> lang_ref := Ocaml) }
 
 let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
@@ -460,9 +458,7 @@ let (inline_extraction,_) =
 let _ = declare_summary "Extraction Inline"
 	  { freeze_function = (fun () -> !inline_table);
 	    unfreeze_function = ((:=) inline_table);
-	    init_function = (fun () -> inline_table := empty_inline_table);
-	    survive_module = true;
-	    survive_section = true }
+	    init_function = (fun () -> inline_table := empty_inline_table) }
 
 (* Grammar entries. *)
 
@@ -542,9 +538,7 @@ let (blacklist_extraction,_) =
 let _ = declare_summary "Extraction Blacklist"
 	  { freeze_function = (fun () -> !blacklist_table);
 	    unfreeze_function = ((:=) blacklist_table);
-	    init_function = (fun () -> blacklist_table := Idset.empty);
-	    survive_module = true;
-	    survive_section = true }
+	    init_function = (fun () -> blacklist_table := Idset.empty) }
 
 (* Grammar entries. *)
 
@@ -603,9 +597,7 @@ let (in_customs,_) =
 let _ = declare_summary "ML extractions"
 	  { freeze_function = (fun () -> !customs);
 	    unfreeze_function = ((:=) customs);
-	    init_function = (fun () -> customs := Refmap.empty);
-	    survive_module = true;
-	    survive_section = true }
+	    init_function = (fun () -> customs := Refmap.empty) }
 
 (* Grammar entries. *)
 
-- 
cgit v1.2.3