diff options
Diffstat (limited to 'toplevel/ind_tables.ml')
| -rw-r--r-- | toplevel/ind_tables.ml | 18 |
1 files changed, 5 insertions, 13 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 |