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

0 files changed, 0 insertions, 0 deletions