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

7 files changed, 12 insertions, 36 deletions

diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 3a408909d..17d41ee8b 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 := []) }  
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index e6d634466..7a265b526 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. *)
 
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index 916294774..7401491e4 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -56,9 +56,7 @@ let _ =
   Summary.declare_summary "field"
     { Summary.freeze_function   = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function     = init;
-      Summary.survive_module = false;
-      Summary.survive_section   = false }
+      Summary.init_function     = init }
 
 let load_addfield _ = ()
 let cache_addfield (_,(typ,th)) = th_tab := Gmap.add typ th !th_tab
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 868a876be..3583c8448 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -434,9 +434,7 @@ let _ =
   Summary.declare_summary "functions_db_sum"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_module = false; 
-      Summary.survive_section = false }
+      Summary.init_function = init }
 
 let find_or_none id = 
   try Some 
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index a07ec4757..2ed20b2bb 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -181,9 +181,7 @@ let _ =
   Summary.declare_summary "tactic-ring-table"
     { Summary.freeze_function = (fun () -> !theories_map);
       Summary.unfreeze_function = (fun t -> theories_map := t);
-      Summary.init_function = (fun () -> theories_map := Cmap.empty);
-      Summary.survive_module = false;
-      Summary.survive_section = false }
+      Summary.init_function = (fun () -> theories_map := Cmap.empty) }
 
 (* declare a new type of object in the environment, "tactic-ring-theory"
    The functions theory_to_obj and obj_to_theory do the conversions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 24cb84ed5..14fd9192e 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -389,9 +389,7 @@ let _ =
       Summary.init_function =
         (fun () ->
           from_carrier := Cmap.empty; from_relation := Cmap.empty;
-          from_name := Spmap.empty);
-      Summary.survive_module = false;
-      Summary.survive_section = false }
+          from_name := Spmap.empty) }
 
 let add_entry (sp,_kn) e =
 (*  let _ = ty e.ring_lemma1 in
@@ -971,9 +969,7 @@ let _ =
       Summary.init_function =
         (fun () ->
           field_from_carrier := Cmap.empty; field_from_relation := Cmap.empty;
-          field_from_name := Spmap.empty);
-      Summary.survive_module = false;
-      Summary.survive_section = false }
+          field_from_name := Spmap.empty) }
 
 let add_field_entry (sp,_kn) e =
 (*
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index a8f5815bc..74ac78706 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -142,9 +142,7 @@ let _ =
   Summary.declare_summary "program-tcc-table"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_module = false;
-      Summary.survive_section = false }
+      Summary.init_function = init }
 
 let progmap_union = ProgMap.fold ProgMap.add