[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.

1 files changed, 1 insertions, 1 deletions

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 }