Merge PR #6275: [summary] Allow typed projections from global state.

16 files changed, 191 insertions, 155 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 907f1b1ac..3445b744a 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -199,9 +199,10 @@ let whd_head_evar sigma c =
 let meta_counter_summary_name = "meta counter"
 
 (* Generator of metavariables *)
-let new_meta =
-  let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
-  fun () -> incr meta_ctr; !meta_ctr
+let meta_ctr, meta_counter_summary_tag =
+  Summary.ref_tag 0 ~name:meta_counter_summary_name
+
+let new_meta () = incr meta_ctr; !meta_ctr
 
 let mk_new_meta () = EConstr.mkMeta(new_meta())
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 5fd4634d6..9d0b973a7 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -236,7 +236,7 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b ->
 val subterm_source : Evar.t -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
 
-val meta_counter_summary_name : string
+val meta_counter_summary_tag : int Summary.Dyn.tag
 
 (** Deprecated *)
 type type_constraint = types option
diff --git a/engine/evd.ml b/engine/evd.ml
index 45d2a8b08..e33c851f6 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -466,9 +466,8 @@ let add d e i = add_with_name d e i
 let evar_counter_summary_name = "evar counter"
 
 (* Generator of existential names *)
-let new_untyped_evar =
-  let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
-  fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
+let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name
+let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
 let new_evar evd ?name evi =
   let evk = new_untyped_evar () in
diff --git a/engine/evd.mli b/engine/evd.mli
index 636bd1be1..b28ce2a62 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -613,7 +613,7 @@ type unsolvability_explanation = SeveralInstancesFound of int
 
 (* This stuff is internal and should not be used. Currently a hack in
    the STM relies on it. *)
-val evar_counter_summary_name : string
+val evar_counter_summary_tag : int Summary.Dyn.tag
 
 (** {5 Deprecated functions} *)
 val create_evar_defs : evar_map -> evar_map
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 83e673d2c..64535d35f 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -55,6 +55,8 @@ sig
   include PreS
 
   module Easy : sig
+
+    val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
     val make_dyn : string -> ('a -> t) * (t -> 'a)
     val inj : 'a -> 'a tag -> t
     val prj : t -> 'a tag -> 'a option
@@ -129,8 +131,9 @@ end
 include Self
 
 module Easy = struct
+
 (* now tags are opaque, we can do the trick *)
-let make_dyn (s : string) =
+let make_dyn_tag (s : string) =
  (fun (type a) (tag : a tag) ->
   let infun : (a -> t) = fun x -> Dyn (tag, x) in
   let outfun : (t -> a) = fun (Dyn (t, x)) ->
@@ -138,9 +141,12 @@ let make_dyn (s : string) =
     | None -> assert false
     | Some CSig.Refl -> x
   in
-  (infun, outfun))
+  infun, outfun, tag)
  (create s)
 
+let make_dyn (s : string) =
+  let inf, outf, _ = make_dyn_tag s in inf, outf
+
 let inj x tag = Dyn(tag,x)
 let prj : type a. t -> a tag -> a option =
     fun (Dyn(tag',x)) tag ->
diff --git a/lib/dyn.mli b/lib/dyn.mli
index e0e1a9d14..2206394e2 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -53,6 +53,7 @@ val dump : unit -> (int * string) list
 module Easy : sig
 
   (* To create a dynamic type on the fly *)
+  val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
   val make_dyn : string -> ('a -> t) * (t -> 'a)
 
   (* For types declared with the [create] function above *)
diff --git a/library/global.ml b/library/global.ml
index 03d7612a4..ce37dfecf 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -20,6 +20,7 @@ module GlobalSafeEnv : sig
   val set_safe_env : Safe_typing.safe_environment -> unit
   val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
   val is_joined_environment : unit -> bool
+  val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag
 
 end = struct
 
@@ -30,9 +31,9 @@ let join_safe_environment ?except () =
 
 let is_joined_environment () =
   Safe_typing.is_joined_environment !global_env
-  
-let () =
-  Summary.declare_summary global_env_summary_name
+
+let global_env_summary_tag =
+  Summary.declare_summary_tag global_env_summary_name
     { Summary.freeze_function = (function
         | `Yes -> join_safe_environment (); !global_env
         | `No -> !global_env
@@ -51,6 +52,8 @@ let set_safe_env e = global_env := e
 
 end
 
+let global_env_summary_tag = GlobalSafeEnv.global_env_summary_tag
+
 let safe_env = GlobalSafeEnv.safe_env
 let join_safe_environment ?except () =
   GlobalSafeEnv.join_safe_environment ?except ()
diff --git a/library/global.mli b/library/global.mli
index c62462f9f..324181e79 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -159,4 +159,4 @@ val current_dirpath : unit -> DirPath.t
 
 val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a
 
-val global_env_summary_name : string
+val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag
diff --git a/library/summary.ml b/library/summary.ml
index 9f49d1f83..6df17476b 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -13,17 +13,22 @@ open Util
 module Dyn = Dyn.Make ()
 
 type marshallable = [ `Yes | `No | `Shallow ]
+
 type 'a summary_declaration = {
   freeze_function : marshallable -> 'a;
   unfreeze_function : 'a -> unit;
   init_function : unit -> unit }
 
-let summaries = ref Int.Map.empty
+let sum_mod = ref None
+let sum_map = ref String.Map.empty
 
 let mangle id = id ^ "-SUMMARY"
+let unmangle id = String.(sub id 0 (length id - 8))
+
+let ml_modules = "ML-MODULES"
 
-let internal_declare_summary hash sumname sdecl =
-  let (infun, outfun) = Dyn.Easy.make_dyn (mangle sumname) in
+let internal_declare_summary fadd sumname sdecl =
+  let infun, outfun, tag = Dyn.Easy.make_dyn_tag (mangle sumname) in
   let dyn_freeze b = infun (sdecl.freeze_function b)
   and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum)
   and dyn_init = sdecl.init_function in
@@ -32,140 +37,116 @@ let internal_declare_summary hash sumname sdecl =
     unfreeze_function = dyn_unfreeze;
     init_function = dyn_init }
   in
-  summaries := Int.Map.add hash (sumname, ddecl) !summaries
+  fadd sumname ddecl;
+  tag
 
-let all_declared_summaries = ref Int.Set.empty
+let declare_ml_modules_summary decl =
+  let ml_add _ ddecl = sum_mod := Some ddecl in
+  internal_declare_summary ml_add ml_modules decl
 
-let summary_names = ref []
-let name_of_summary name =
-  try List.assoc name !summary_names
-  with Not_found -> "summary name not found"
+let declare_ml_modules_summary decl =
+  ignore(declare_ml_modules_summary decl)
 
-let declare_summary sumname decl =
-  let hash = String.hash sumname in
-  let () = if Int.Map.mem hash !summaries then
-    let (name, _) = Int.Map.find hash !summaries in
-    anomaly ~label:"Summary.declare_summary"
-      (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str name ++ str ".")
+let declare_summary_tag sumname decl =
+  let fadd name ddecl = sum_map := String.Map.add name ddecl !sum_map in
+  let () = if String.Map.mem sumname !sum_map then
+      anomaly ~label:"Summary.declare_summary"
+        (str "Colliding summary names: " ++ str sumname ++ str " vs. " ++ str sumname ++ str ".")
   in
-  all_declared_summaries := Int.Set.add hash !all_declared_summaries;
-  summary_names := (hash, sumname) :: !summary_names;
-  internal_declare_summary hash sumname decl
+  internal_declare_summary fadd sumname decl
+
+let declare_summary sumname decl =
+  ignore(declare_summary_tag sumname decl)
 
 type frozen = {
-  summaries : (int * Dyn.t) list;
+  summaries : Dyn.t String.Map.t;
   (** Ordered list w.r.t. the first component. *)
   ml_module : Dyn.t option;
   (** Special handling of the ml_module summary. *)
 }
 
-let empty_frozen = { summaries = []; ml_module = None; }
-
-let ml_modules = "ML-MODULES"
-let ml_modules_summary = String.hash ml_modules
+let empty_frozen = { summaries = String.Map.empty; ml_module = None }
 
 let freeze_summaries ~marshallable : frozen =
-  let fold id (_, decl) accu =
-    (* to debug missing Lazy.force
-    if marshallable <> `No then begin
-      let id, _ = Int.Map.find id !summaries in
-      prerr_endline ("begin marshalling " ^ id);
-      ignore(Marshal.to_string (decl.freeze_function marshallable) []);
-      prerr_endline ("end marshalling " ^ id);
-    end;
-    /debug *)
-    let state = decl.freeze_function marshallable in
-    if Int.equal id ml_modules_summary then { accu with ml_module = Some state }
-    else { accu with summaries = (id, state) :: accu.summaries }
+  let smap decl = decl.freeze_function marshallable in
+  { summaries = String.Map.map smap !sum_map;
+    ml_module = Option.map (fun decl -> decl.freeze_function marshallable) !sum_mod;
+  }
+
+let unfreeze_single name state =
+  let decl =
+    try String.Map.find name !sum_map
+    with
+    | Not_found ->
+      CErrors.anomaly Pp.(str "trying to unfreeze unregistered summary " ++ str name)
   in
-  Int.Map.fold_right fold !summaries empty_frozen
-
-let unfreeze_summaries fs =
+  try decl.unfreeze_function state
+  with e when CErrors.noncritical e ->
+    let e = CErrors.push e in
+    Feedback.msg_warning
+      Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]);
+    iraise e
+
+let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
   (* The unfreezing of [ml_modules_summary] has to be anticipated since it
-   * may modify the content of [summaries] ny loading new ML modules *)
-  let (_, decl) =
-    try Int.Map.find ml_modules_summary !summaries
-    with Not_found -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
-  in
-  let () = match fs.ml_module with
+   * may modify the content of [summaries] by loading new ML modules *)
+  begin match !sum_mod with
   | None -> anomaly (str "Undeclared summary " ++ str ml_modules ++ str ".")
-  | Some state -> decl.unfreeze_function state
-  in
-  let fold id (_, decl) states =
-    if Int.equal id ml_modules_summary then states
-    else match states with
-    | [] ->
-      let () = decl.init_function () in
-      []
-    | (nid, state) :: rstates ->
-      if Int.equal id nid then
-        let () = decl.unfreeze_function state in rstates
-      else
-        let () = decl.init_function () in states
+  | Some decl -> Option.iter (fun state -> decl.unfreeze_function state) ml_module
+  end;
+  (** We must be independent on the order of the map! *)
+  let ufz name decl =
+    try decl.unfreeze_function String.Map.(find name summaries)
+    with Not_found ->
+      if not partial then begin
+        Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name);
+        decl.init_function ()
+      end;
   in
-  let fold id decl state =
-    try fold id decl state
-    with e when CErrors.noncritical e ->
-      let e = CErrors.push e in
-      Feedback.msg_error
-        Pp.(seq [str "Error unfreezing summary %s\n%s\n%!";
-                 str (name_of_summary id);
-                 CErrors.iprint e]);
-      iraise e
-  in
-  (** We rely on the order of the frozen list, and the order of folding *)
-  ignore (Int.Map.fold_left fold !summaries fs.summaries)
+  (* String.Map.iter unfreeze_single !sum_map *)
+  String.Map.iter ufz !sum_map
 
 let init_summaries () =
-  Int.Map.iter (fun _ (_, decl) -> decl.init_function ()) !summaries
+  String.Map.iter (fun _ decl -> decl.init_function ()) !sum_map
 
 (** For global tables registered statically before the end of coqtop
     launch, the following empty [init_function] could be used. *)
 
 let nop () = ()
 
-(** Selective freeze *)
+(** Summary projection *)
+let project_from_summary { summaries } tag =
+  let id = unmangle (Dyn.repr tag) in
+  let state = String.Map.find id summaries in
+  Option.get (Dyn.Easy.prj state tag)
+
+let modify_summary st tag v =
+  let id = unmangle (Dyn.repr tag) in
+  let summaries = String.Map.set id (Dyn.Easy.inj v tag) st.summaries in
+  {st with summaries}
 
-type frozen_bits = (int * Dyn.t) list
+let remove_from_summary st tag =
+  let id = unmangle (Dyn.repr tag) in
+  let summaries = String.Map.remove id st.summaries in
+  {st with summaries}
+
+(** Selective freeze *)
 
-let ids_of_string_list complement ids =
-  if not complement then List.map String.hash ids
-  else
-    let fold accu id =
-      let id = String.hash id in
-      Int.Set.remove id accu
-    in
-    let ids = List.fold_left fold !all_declared_summaries ids in
-    Int.Set.elements ids
+type frozen_bits = Dyn.t String.Map.t
 
 let freeze_summary ~marshallable ?(complement=false) ids =
-  let ids = ids_of_string_list complement ids in
-  List.map (fun id ->
-    let (_, summary) = Int.Map.find id !summaries in
-    id, summary.freeze_function marshallable)
-  ids
-
-let unfreeze_summary datas =
-  List.iter
-    (fun (id, data) ->
-      let (name, summary) = Int.Map.find id !summaries in
-      try summary.unfreeze_function data
-      with e ->
-        let e = CErrors.push e in
-        prerr_endline ("Exception unfreezing " ^ name);
-        iraise e)
-  datas
+  let sub_map = String.Map.filter (fun id _ -> complement <> List.(mem id ids)) !sum_map in
+  String.Map.map (fun decl -> decl.freeze_function marshallable) sub_map
+
+let unfreeze_summary = String.Map.iter unfreeze_single
 
 let surgery_summary { summaries; ml_module } bits =
-  let summaries = List.map (fun (id, _ as orig) ->
-      try id, List.assoc id bits
-      with Not_found -> orig)
-    summaries in
+  let summaries =
+    String.Map.fold (fun hash state sum -> String.Map.set hash state sum ) summaries bits in
   { summaries; ml_module }
 
 let project_summary { summaries; ml_module } ?(complement=false) ids =
-  let ids = ids_of_string_list complement ids in
-  List.filter (fun (id, _) -> List.mem id ids) summaries
+  String.Map.filter (fun name _ -> complement <> List.(mem name ids)) summaries
 
 let pointer_equal l1 l2 =
   let ptr_equal d1 d2 =
@@ -174,19 +155,22 @@ let pointer_equal l1 l2 =
     match Dyn.eq t1 t2 with
     | None -> false
     | Some Refl -> x1 == x2
-    in
+  in
+  let l1, l2 = String.Map.bindings l1, String.Map.bindings l2 in
   CList.for_all2eq
     (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2
 
 (** All-in-one reference declaration + registration *)
 
-let ref ?(freeze=fun _ r -> r) ~name x =
+let ref_tag ?(freeze=fun _ r -> r) ~name x =
   let r = ref x in
-  declare_summary name
+  let tag = declare_summary_tag name
     { freeze_function = (fun b -> freeze b !r);
       unfreeze_function = ((:=) r);
-      init_function = (fun () -> r := x) };
-  r
+      init_function = (fun () -> r := x) } in
+  r, tag
+
+let ref ?freeze ~name x = fst @@ ref_tag ?freeze ~name x
 
 module Local = struct
 
@@ -198,8 +182,7 @@ let (!) r =
   let key, name = !r in
   try CEphemeron.get key
   with CEphemeron.InvalidKey ->
-    let _, { init_function } =
-      Int.Map.find (String.hash (mangle name)) !summaries in
+    let { init_function } = String.Map.find name !sum_map in
     init_function ();
     CEphemeron.get (fst !r)
 
diff --git a/library/summary.mli b/library/summary.mli
index d093d95f2..09447199e 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -36,6 +36,12 @@ type 'a summary_declaration = {
 
 val declare_summary : string -> 'a summary_declaration -> unit
 
+(** We provide safe projection from the summary to the types stored in
+   it.*)
+module Dyn : Dyn.S
+
+val declare_summary_tag : string -> 'a summary_declaration -> 'a Dyn.tag
+
 (** All-in-one reference declaration + summary registration.
     It behaves just as OCaml's standard [ref] function, except
     that a [declare_summary] is done, with [name] as string.
@@ -43,6 +49,7 @@ val declare_summary : string -> 'a summary_declaration -> unit
     The [freeze_function] can be overridden *)
 
 val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
+val ref_tag : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref * 'a Dyn.tag
 
 (* As [ref] but the value is local to a process, i.e. not sent to, say, proof
  * workers.  It is useful to implement a local cache for example. *)
@@ -55,10 +62,11 @@ module Local : sig
 
 end
 
-(** Special name for the summary of ML modules.  This summary entry is
-    special because its unfreeze may load ML code and hence add summary
-    entries.  Thus is has to be recognizable, and handled appropriately *)
-val ml_modules : string
+(** Special summary for ML modules.  This summary entry is special
+    because its unfreeze may load ML code and hence add summary
+    entries.  Thus is has to be recognizable, and handled properly.
+   *)
+val declare_ml_modules_summary : 'a summary_declaration -> unit
 
 (** For global tables registered statically before the end of coqtop
     launch, the following empty [init_function] could be used. *)
@@ -72,19 +80,34 @@ type frozen
 
 val empty_frozen : frozen
 val freeze_summaries : marshallable:marshallable -> frozen
-val unfreeze_summaries : frozen -> unit
+val unfreeze_summaries : ?partial:bool -> frozen -> unit
 val init_summaries : unit -> unit
 
-(** The type [frozen_bits] is a snapshot of some of the registered tables *)
+(** Typed projection of the summary. Experimental API, use with CARE *)
+
+val modify_summary : frozen -> 'a Dyn.tag -> 'a -> frozen
+val project_from_summary : frozen -> 'a Dyn.tag -> 'a
+val remove_from_summary : frozen -> 'a Dyn.tag -> frozen
+
+(** The type [frozen_bits] is a snapshot of some of the registered
+    tables. It is DEPRECATED in favor of the typed projection
+    version. *)
+
 type frozen_bits
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
 
-val freeze_summary :
-  marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits
+[@@@ocaml.warning "-3"]
+val freeze_summary : marshallable:marshallable -> ?complement:bool -> string list -> frozen_bits
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
 val unfreeze_summary : frozen_bits -> unit
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
 val surgery_summary : frozen -> frozen_bits -> frozen
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
 val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
 val pointer_equal : frozen_bits -> frozen_bits -> bool
+[@@ocaml.deprecated "Please use the typed version of summary projection"]
+[@@@ocaml.warning "+3"]
 
 (** {6 Debug} *)
-
 val dump : unit -> (int * string) list
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8e6a01aa3..b766f0c6b 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -611,8 +611,8 @@ let unfreeze (grams, lex) =
     the lexer state should not be resetted, since it contains
     keywords declared in g_*.ml4 *)
 
-let _ =
-  Summary.declare_summary "GRAMMAR_LEXER"
+let parser_summary_tag =
+  Summary.declare_summary_tag "GRAMMAR_LEXER"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = Summary.nop }
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d17ccb0b4..3ca013a96 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -313,3 +313,6 @@ val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
 (** Location Utils  *)
 val to_coqloc : Ploc.t -> Loc.t
 val (!@) : Ploc.t -> Loc.t
+
+type frozen_t
+val parser_summary_tag : frozen_t Summary.Dyn.tag
diff --git a/stm/stm.ml b/stm/stm.ml
index 8aa832da8..0dbe168b7 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -158,9 +158,10 @@ let mkTransCmd cast cids ceff cqueue =
   Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff }
 
 (* Parts of the system state that are morally part of the proof state *)
-let summary_pstate = [ Evarutil.meta_counter_summary_name;
-                       Evd.evar_counter_summary_name;
-                       "program-tcc-table" ]
+let summary_pstate = Evarutil.meta_counter_summary_tag,
+                     Evd.evar_counter_summary_tag,
+                     Obligations.program_tcc_summary_tag
+
 type cached_state =
   | Empty
   | Error of Exninfo.iexn
@@ -762,15 +763,21 @@ end = struct (* {{{ *)
   let fix_exn_ref = ref (fun x -> x)
 
   type proof_part =
-    Proof_global.t * Summary.frozen_bits (* only meta counters *)
+    Proof_global.t *
+    int *                                   (* Evarutil.meta_counter_summary_tag *)
+    int *                                   (* Evd.evar_counter_summary_tag *)
+    Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
 
   type partial_state =
     [ `Full of Vernacstate.t
     | `ProofOnly of Stateid.t * proof_part ]
 
   let proof_part_of_frozen { Vernacstate.proof; system } =
+    let st = States.summary_of_state system in
     proof,
-    Summary.project_summary (States.summary_of_state system) summary_pstate
+    Summary.project_from_summary st Util.(pi1 summary_pstate),
+    Summary.project_from_summary st Util.(pi2 summary_pstate),
+    Summary.project_from_summary st Util.(pi3 summary_pstate)
 
   let freeze marshallable id =
     VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable))
@@ -830,16 +837,21 @@ end = struct (* {{{ *)
             else s
            with VCS.Expired -> s in
          VCS.set_state id (Valid s)
-    | `ProofOnly(ontop,(pstate,counters)) ->
+    | `ProofOnly(ontop,(pstate,c1,c2,c3)) ->
          if is_cached_and_valid ontop then
            let s = get_cached ontop in
            let s = { s with proof =
              Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
            let s = { s with system =
              States.replace_summary s.system
-               (Summary.surgery_summary
-                 (States.summary_of_state s.system)
-               counters) } in
+               begin
+                 let st = States.summary_of_state s.system in
+                 let st = Summary.modify_summary st Util.(pi1 summary_pstate) c1 in
+                 let st = Summary.modify_summary st Util.(pi2 summary_pstate) c2 in
+                 let st = Summary.modify_summary st Util.(pi3 summary_pstate) c3 in
+                 st
+               end
+                } in
            VCS.set_state id (Valid s)
     with VCS.Expired -> ()
 
@@ -854,10 +866,10 @@ end = struct (* {{{ *)
 
   let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } =
     let s1 = States.summary_of_state s1 in
-    let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in
+    let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in
     let s2 = States.summary_of_state s2 in
-    let e2 = Summary.project_summary s2 [Global.global_env_summary_name] in
-    Summary.pointer_equal e1 e2
+    let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in
+    e1 == e2
 
   let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
         f id
@@ -2040,8 +2052,6 @@ and Reach : sig
 
 end = struct (* {{{ *)
 
-let pstate = summary_pstate
-
 let async_policy () =
   let open Flags in
   if is_universe_polymorphism () then false
@@ -2254,10 +2264,14 @@ let known_state ?(redefine_qed=false) ~cache id =
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
   let cherry_pick_non_pstate () =
-    Summary.freeze_summary ~marshallable:`No ~complement:true pstate,
-    Lib.freeze ~marshallable:`No in
+    let st = Summary.freeze_summaries ~marshallable:`No in
+    let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in
+    let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in
+    let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in
+    st, Lib.freeze ~marshallable:`No in
+
   let inject_non_pstate (s,l) =
-    Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
+    Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env ()
   in
   let rec pure_cherry_pick_non_pstate safe_id id =
     stm_purify (fun id ->
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 }
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 4f011e6ad..181068089 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -429,8 +429,8 @@ let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
 
 let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
 
-let from_prg : program_info ProgMap.t ref =
-  Summary.ref ProgMap.empty ~name:"program-tcc-table"
+let from_prg, program_tcc_summary_tag =
+  Summary.ref_tag ProgMap.empty ~name:"program-tcc-table"
 
 let close sec =
   if not (ProgMap.is_empty !from_prg) then
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 0602e52e9..bdc97d48c 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -104,3 +104,6 @@ exception NoObligations of Names.Id.t option
 val explain_no_obligations : Names.Id.t option -> Pp.t
 
 val set_program_mode : bool -> unit
+
+type program_info
+val program_tcc_summary_tag : program_info Id.Map.t Summary.Dyn.tag