Module `Vernacentries`

val check_may_eval : Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr option -> Constrexpr.constr_expr -> Pp.t
val translate_vernac : ?⁠loc:Loc.t -> atts:Attributes.vernac_flags -> Synterp.vernac_entry -> Vernactypes.typed_vernac: Vernac Translation into the Vernac DSL

val vernac_require : Libnames.qualid option -> Vernacexpr.export_with_cats option -> (Libnames.qualid * Vernacexpr.import_filter_expr) list -> unit: Vernacular require command, used by the command line

val vernac_require_interp : Library.library_t list -> Names.DirPath.t list -> Vernacexpr.export_with_cats option -> (Libnames.qualid * Vernacexpr.import_filter_expr) list -> unit: Interp phase of the 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

module Preprocessed_Mind_decl : sig ... end: pre-processing and validation of VernacInductive

val preprocess_inductive_decl : atts:Attributes.vernac_flags -> Vernacexpr.inductive_kind -> (Vernacexpr.inductive_expr * Vernacexpr.notation_declaration list) list -> Preprocessed_Mind_decl.t