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

3 files changed, 7 insertions, 19 deletions

diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index ae4e8cf52..5df33d459 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 open Names
 open Mod_subst
@@ -24,9 +24,7 @@ let export_scheme obj =
 let _ = Summary.declare_summary "eqscheme"
     { Summary.freeze_function = (fun () -> !eq_scheme_map);
       Summary.unfreeze_function = (fun fs -> eq_scheme_map := fs);
-      Summary.init_function = (fun () -> eq_scheme_map := Indmap.empty);
-      Summary.survive_module = false;
-      Summary.survive_section = true}
+      Summary.init_function = (fun () -> eq_scheme_map := Indmap.empty) }
 
 let find_eq_scheme ind = 
   Indmap.find ind !eq_scheme_map
@@ -62,9 +60,7 @@ let export_dec_proof obj =
 let _ = Summary.declare_summary "bl_proof"
     { Summary.freeze_function = (fun () -> !bl_map);
       Summary.unfreeze_function = (fun fs -> bl_map := fs);
-      Summary.init_function = (fun () -> bl_map := Indmap.empty);
-      Summary.survive_module = false;
-      Summary.survive_section = true}
+      Summary.init_function = (fun () -> bl_map := Indmap.empty) }
 
 let find_bl_proof ind = 
   Indmap.find ind !bl_map
@@ -75,9 +71,7 @@ let check_bl_proof ind =
 let _ = Summary.declare_summary "lb_proof"
     { Summary.freeze_function = (fun () -> !lb_map);
       Summary.unfreeze_function = (fun fs -> lb_map := fs);
-      Summary.init_function = (fun () -> lb_map := Indmap.empty);
-      Summary.survive_module = false;
-      Summary.survive_section = true}
+      Summary.init_function = (fun () -> lb_map := Indmap.empty) }
 
 let find_lb_proof ind = 
   Indmap.find ind !lb_map
@@ -88,9 +82,7 @@ let check_lb_proof ind =
 let _ = Summary.declare_summary "eq_dec_proof"
     { Summary.freeze_function = (fun () -> !dec_map);
       Summary.unfreeze_function = (fun fs -> dec_map := fs);
-      Summary.init_function = (fun () -> dec_map := Indmap.empty);
-      Summary.survive_module = false;
-      Summary.survive_section = true}
+      Summary.init_function = (fun () -> dec_map := Indmap.empty) }
 
 let find_eq_dec_proof ind = 
   Indmap.find ind !dec_map
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
index 4e10d1d52..c999c0609 100644
--- a/toplevel/libtypes.ml
+++ b/toplevel/libtypes.ml
@@ -51,9 +51,7 @@ let _ =
   declare_summary "type-library-state"
     { freeze_function = freeze;
       unfreeze_function = unfreeze;
-      init_function = init;
-      survive_module = false;
-      survive_section = false }
+      init_function = init }
 
 let load (_,d) =
 (*  Profile.print_logical_stats !all_types;
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 837d50207..c390c7c52 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -274,9 +274,7 @@ let _ =
   Summary.declare_summary "ML-MODULES"
     { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules()));
       Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x);
-      Summary.init_function = (fun () -> init_ml_modules ());
-      Summary.survive_module = false;
-      Summary.survive_section = true }
+      Summary.init_function = (fun () -> init_ml_modules ()) }
 
 (* Same as restore_ml_modules, but verbosely *)