Module Pvernac.Vernac_

val inductive_or_record_definition : (Vernacexpr.inductive_expr * Vernacexpr.notation_declaration list) Procq.Entry.t
val command_entry : Vernacexpr.vernac_expr Procq.Entry.t
val main_entry : Vernacexpr.vernac_control option Procq.Entry.t