Module `Indschemes`

type resolved_scheme = Names.Id.t CAst.t * Indrec.dep_flag * Names.inductive * Sorts.family

val name_and_process_schemes : Environ.env -> (Names.lident option * Vernacexpr.scheme) list -> resolved_scheme list: Resolve the names of a list of inductive schemes with respect to an environment

val declare_beq_scheme : Names.MutInd.t -> unit
val declare_eq_decidability : Names.MutInd.t -> unit

val declare_congr_scheme : Names.inductive -> unit

val declare_rewriting_schemes : Names.inductive -> unit

val do_mutual_induction_scheme : ?⁠force_mutual:bool -> Environ.env -> resolved_scheme list -> unit

val do_scheme : Environ.env -> (Names.Id.t CAst.t option * Vernacexpr.scheme) list -> unit

val do_scheme_equality : Vernacexpr.equality_scheme_type -> Libnames.qualid Constrexpr.or_by_notation -> unit

val build_combined_scheme : Environ.env -> Names.Constant.t list -> Evd.evar_map * Constr.constr * Constr.types
val do_combined_scheme : Names.lident -> Names.lident list -> unit

val declare_default_schemes : Names.MutInd.t -> unit