Module `Vernacentries`

val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit
val get_default_proof_mode : unit -> Pvernac.proof_mode: Default proof mode set by `start_proof`

val proof_mode_opt_name : string list
val vernac_require : Libnames.qualid option -> bool option -> Libnames.qualid list -> unit: Vernacular entries

val interp : ?⁠verbosely:bool -> ?⁠proof:Proof_global.closed_proof -> st:Vernacstate.t -> Vernacexpr.vernac_control CAst.t -> Vernacstate.t: The main interpretation function of vernacular expressions

val make_cases : string -> string list list
val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit: with_fail ~st f runs f () and expects it to fail, otherwise it fails.

val command_focus : unit Proof.focus_kind
val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t
val vernac_require_open_proof : pstate:Proof_global.t option -> (pstate:Proof_global.t -> 'a) -> 'a: Helper

val test_mode : bool Stdlib.ref