Vernacentriesval check_may_eval : Environ.env -> Evd.evar_map -> Redexpr.raw_red_expr option -> Constrexpr.constr_expr -> Pp.tval translate_vernac : ?loc:Loc.t -> atts:Attributes.vernac_flags -> Synterp.vernac_entry -> Vernactypes.typed_vernacVernac Translation into the Vernac DSL
val vernac_require : intern:Library.Intern.t -> Libnames.qualid option -> Vernacexpr.export_with_cats option -> (Libnames.qualid * Vernacexpr.import_filter_expr) list -> unitVernacular 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 -> unitInterp phase of the require command
val command_focus : unit Proof.focus_kindMiscellaneous stuff
module Preprocessed_Mind_decl : sig ... endpre-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.tmodule DefAttributes : sig ... endval show_goal : Vernacexpr.goal_reference -> Proof.t -> Proof.t option option -> Pp.t