val hash : t -> intval mode : st:t -> Pvernac.proof_mode optionval parsing : st:t -> Vernacstate.Parser.tmodule Proof : sig ... endProof states
val in_state : st:t -> f:('a -> 'b) -> 'a -> ('b, Loc.t) Protect.E.tExecute a command in state st. Unfortunately this can produce anomalies as Coq state setting is imperative, so we need to wrap it in protect.
val admit : st:t -> (t, Loc.t) Protect.E.tFully admit an ongoing proof
val admit_goal : st:t -> (t, Loc.t) Protect.E.tAdmit the current sub-goal
val marshal_in : in_channel -> tExtra / interanl
val marshal_out : out_channel -> t -> unitval of_coq : Vernacstate.t -> tval to_coq : t -> Vernacstate.t