Vernacentries.Preprocessed_Mind_declpre-processing and validation of VernacInductive
type flags = ComInductive.flagstype record = {flags : flags; |
udecl : Constrexpr.cumul_univ_decl_expr option; |
primitive_proj : bool; |
kind : Vernacexpr.inductive_kind; |
records : Record.Ast.t list; |
}type inductive = {flags : flags; |
udecl : Constrexpr.cumul_univ_decl_expr option; |
typing_flags : Declarations.typing_flags option; |
private_ind : bool; |
uniform : ComInductive.uniform_inductive_flag; |
inductives : (Vernacexpr.one_inductive_expr * Vernacexpr.notation_declaration list) list; |
}