From 8c9166435d6926babf697c3f575a8653f465cc76 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 1 Dec 2017 19:13:04 +0100 Subject: [summary] Allow typed projections from global state + rework of internals. In the transition towards a less global state handling we have the necessity of mix imperative setting [notably for the modules/section code] and functional handling of state [notably in the STM]. In that scenario, it is very convenient to have typed access to the Coq's `summary`. Thus, I reify the API to support typed access to the `summary`, and implement such access in a couple of convenient places. We also update some internal datatypes to simplify the `frozen` data type. We also remove the use of hashes as it doesn't really make things faster, and most operations are now over `Maps` anyways. I believe this goes in line with recent work by @ppedrot. We also deprecate the non-typed accessors, which were only supposed to be used in the STM, which is now ported to the finer primitives. --- vernac/mltop.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/mltop.ml') diff --git a/vernac/mltop.ml b/vernac/mltop.ml index d3de10235..00554e3ba 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -378,7 +378,7 @@ let unfreeze_ml_modules x = (fun (name,path) -> trigger_ml_object false false false ?path name) x let _ = - Summary.declare_summary Summary.ml_modules + Summary.declare_ml_modules_summary { Summary.freeze_function = (fun _ -> get_loaded_modules ()); Summary.unfreeze_function = unfreeze_ml_modules; Summary.init_function = reset_loaded_modules } -- cgit v1.2.3