Module Summary

This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system.

type 'a summary_declaration = {
freeze_function : marshallable:bool -> 'a;

freeze_function true is for marshalling to disk. * e.g. lazy must be forced

unfreeze_function : 'a -> unit;
init_function : unit -> unit;
}

Types of global Coq states. The 'a type should be pure and marshallable by the standard OCaml marshalling function.

val declare_summary : string -> 'a summary_declaration -> unit
module Dyn : Dyn.S

We provide safe projection from the summary to the types stored in it.

val declare_summary_tag : string -> 'a summary_declaration -> 'a Dyn.tag
val ref : ?⁠freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a Stdlib.ref
val ref_tag : ?⁠freeze:(marshallable:bool -> 'a -> 'a) -> name:string -> 'a -> 'a Stdlib.ref * 'a Dyn.tag
module Local : sig ... end
val declare_ml_modules_summary : (bool * string) list summary_declaration -> unit

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 nop : unit -> unit
type frozen
val empty_frozen : frozen
val freeze_summaries : marshallable:bool -> frozen
val unfreeze_summaries : ?⁠partial:bool -> frozen -> unit
val init_summaries : unit -> unit
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
val dump : unit -> (int * string) list
Debug