Module Pvernac.Vernac_

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