Module Vernacentries

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

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