Indrectype recursion_scheme_error = | NotMutualInScheme of Names.inductive * Names.inductive |
| DuplicateInductiveBlock of Names.inductive |
Errors related to recursors building
exception RecursionSchemeError of Environ.env * recursion_scheme_errorval build_case_analysis_scheme : Environ.env -> Evd.evar_map -> Names.inductive Evd.puniverses -> dep_flag -> EConstr.ESorts.t -> Evd.evar_map * EConstr.constr * EConstr.constrval build_induction_scheme : Environ.env -> Evd.evar_map -> Names.inductive Evd.puniverses -> dep_flag -> EConstr.ESorts.t -> Evd.evar_map * EConstr.constrBuilds a recursive induction scheme (Peano-induction style) in the given sort.
val build_mutual_induction_scheme : Environ.env -> Evd.evar_map -> ?force_mutual:bool ->
(Names.inductive * dep_flag * EConstr.ESorts.t) list -> Evd.einstance -> Evd.evar_map * EConstr.constr listBuilds mutual (recursive) induction schemes