Module Vernacstate
module Parser : sig ... endtype t={parsing : Parser.state;system : States.state;proof : Proof_global.t option;shallow : bool;}
val freeze_interp_state : marshallable:bool -> tval unfreeze_interp_state : t -> unitval make_shallow : t -> tval invalidate_cache : unit -> unit
module Proof_global : sig ... end