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