Module `Pvernac.Vernac_`

val gallina : Vernacexpr.synpure_vernac_expr Pcoq.Entry.t
val gallina_ext : Vernacexpr.vernac_expr Pcoq.Entry.t
val command : Vernacexpr.vernac_expr Pcoq.Entry.t
val syntax : Vernacexpr.vernac_expr Pcoq.Entry.t
val vernac_control : Vernacexpr.vernac_control Pcoq.Entry.t
val inductive_or_record_definition : (Vernacexpr.inductive_expr * Vernacexpr.notation_declaration list) Pcoq.Entry.t
val fix_definition : Vernacexpr.fixpoint_expr Pcoq.Entry.t
val noedit_mode : Vernacexpr.vernac_expr Pcoq.Entry.t
val command_entry : Vernacexpr.vernac_expr Pcoq.Entry.t
val main_entry : Vernacexpr.vernac_control option Pcoq.Entry.t
val red_expr : Genredexpr.raw_red_expr Pcoq.Entry.t
val hint_info : Vernacexpr.hint_info_expr Pcoq.Entry.t