Module `Vernacentries`

val translate_vernac : ?⁠loc:Loc.t -> atts:Attributes.vernac_flags -> Vernacexpr.vernac_expr -> Vernacextend.typed_vernac: Vernac Translation into the Vernac DSL

val vernac_require : Libnames.qualid option -> bool option -> Libnames.qualid list -> unit: Vernacular require command

val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t: Hook to dissappear when #8240 is fixed

val command_focus : unit Proof.focus_kind: Miscellaneous stuff

val allow_sprop_opt_name : string list