Vernacentries (coq-core.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 -> Vernacexpr.export_with_cats option -> (Libnames.qualid * Vernacexpr.import_filter_expr) list -> unit

Vernacular require command, used by the command line

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.decl_notation list) list -> Preprocessed_Mind_decl.t