diff options
Diffstat (limited to 'toplevel/ind_tables.ml')
| -rw-r--r-- | toplevel/ind_tables.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 5df33d459..49c8ce715 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -11,9 +11,9 @@ open Names open Mod_subst -let eq_scheme_map = ref Indmap.empty +let eq_scheme_map = ref Indmap.empty -let cache_scheme (_,(ind,const)) = +let cache_scheme (_,(ind,const)) = eq_scheme_map := Indmap.add ind const (!eq_scheme_map) let export_scheme obj = @@ -26,10 +26,10 @@ let _ = Summary.declare_summary "eqscheme" Summary.unfreeze_function = (fun fs -> eq_scheme_map := fs); Summary.init_function = (fun () -> eq_scheme_map := Indmap.empty) } -let find_eq_scheme ind = +let find_eq_scheme ind = Indmap.find ind !eq_scheme_map -let check_eq_scheme ind = +let check_eq_scheme ind = Indmap.mem ind !eq_scheme_map let bl_map = ref Indmap.empty @@ -37,13 +37,13 @@ let lb_map = ref Indmap.empty let dec_map = ref Indmap.empty -let cache_bl (_,(ind,const)) = +let cache_bl (_,(ind,const)) = bl_map := Indmap.add ind const (!bl_map) -let cache_lb (_,(ind,const)) = +let cache_lb (_,(ind,const)) = lb_map := Indmap.add ind const (!lb_map) -let cache_dec (_,(ind,const)) = +let cache_dec (_,(ind,const)) = dec_map := Indmap.add ind const (!dec_map) let export_bool_leib obj = @@ -62,7 +62,7 @@ let _ = Summary.declare_summary "bl_proof" Summary.unfreeze_function = (fun fs -> bl_map := fs); Summary.init_function = (fun () -> bl_map := Indmap.empty) } -let find_bl_proof ind = +let find_bl_proof ind = Indmap.find ind !bl_map let check_bl_proof ind = @@ -73,7 +73,7 @@ let _ = Summary.declare_summary "lb_proof" Summary.unfreeze_function = (fun fs -> lb_map := fs); Summary.init_function = (fun () -> lb_map := Indmap.empty) } -let find_lb_proof ind = +let find_lb_proof ind = Indmap.find ind !lb_map let check_lb_proof ind = @@ -84,7 +84,7 @@ let _ = Summary.declare_summary "eq_dec_proof" Summary.unfreeze_function = (fun fs -> dec_map := fs); Summary.init_function = (fun () -> dec_map := Indmap.empty) } -let find_eq_dec_proof ind = +let find_eq_dec_proof ind = Indmap.find ind !dec_map let check_dec_proof ind = |