aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/dischargedhypsmap.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/dischargedhypsmap.ml')
-rw-r--r--library/dischargedhypsmap.ml7
1 files changed, 5 insertions, 2 deletions
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index 96ed944b2..0e7bdef30 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -24,13 +24,16 @@ type discharged_hyps = section_path list
let discharged_hyps_map = ref Spmap.empty
-let cache_discharged_hyps_map (_,(sp,hyps)) =
+let load_discharged_hyps_map _ (_,(sp,hyps)) =
discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
+let cache_discharged_hyps_map o =
+ load_discharged_hyps_map 1 o
+
let (in_discharged_hyps_map, _) =
declare_object { (default_object "DISCHARGED-HYPS-MAP") with
cache_function = cache_discharged_hyps_map;
- load_function = (fun _ -> cache_discharged_hyps_map);
+ load_function = load_discharged_hyps_map;
export_function = (fun x -> Some x) }
let set_discharged_hyps sp hyps =