Module Summary

module Stage : sig ... end

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 = {
stage : Stage.t;
freeze_function : unit -> 'a;
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 -> ?⁠make_marshallable:('a -> 'a) -> '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 -> ?⁠make_marshallable:('a -> 'a) -> 'a summary_declaration -> 'a Dyn.tag
val ref : ?⁠stage:Stage.t -> ?⁠local:bool -> name:string -> 'a -> 'a Stdlib.ref
val ref_tag : ?⁠stage:Stage.t -> name:string -> 'a -> 'a Stdlib.ref * 'a Dyn.tag
val declare_ml_modules_summary : (string option * 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.

The args correspond to Mltop.PluginSpec.t , that is to say, the optional legacy plugin name, and the findlib name for the plugin.

val nop : unit -> unit
module type FrozenStage = sig ... end
module Synterp : FrozenStage
module Interp : sig ... end
val dump : unit -> (int * string) list
Debug