Module Vernacstate

module Parser : sig ... end
module System : sig ... end

System State

module LemmaStack : sig ... end
type t = {
parsing : Parser.t;(*

parsing state parsing state may not behave 100% functionally yet, beware

*)
system : System.t;(*

summary + libstack

*)
lemmas : LemmaStack.t option;(*

proofs of lemmas currently opened

*)
program : Declare.OblState.t NeList.t;(*

program mode table. One per open module/section including the toplevel module.

*)
opaques : Opaques.Summary.t;(*

qed-terminated proofs

*)
shallow : bool;(*

is the state trimmed down (libstack)

*)
}
val freeze_interp_state : marshallable:bool -> t
val unfreeze_interp_state : t -> unit
val invalidate_cache : unit -> unit
module Stm : sig ... end

STM-specific state handling

module Declare : sig ... end