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