Module Vernacstate.Interp

module System : sig ... end
type t = {
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

*)
}
val freeze_interp_state : unit -> t
val unfreeze_interp_state : t -> unit
val invalidate_cache : unit -> unit