Indschemestype resolved_scheme = Names.Id.t CAst.t * Indrec.dep_flag * Names.inductive * Sorts.familySee also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ...
Build and register the boolean equalities associated to an inductive type
val declare_beq_scheme : ?locmap:Ind_tables.Locmap.t -> Names.MutInd.t -> unitval declare_eq_decidability : ?locmap:Ind_tables.Locmap.t -> Names.MutInd.t -> unitBuild and register a congruence scheme for an equality-like inductive type
val declare_congr_scheme : ?loc:Loc.t -> Names.inductive -> unitBuild and register rewriting schemes for an equality-like inductive type
val declare_rewriting_schemes : ?loc:Loc.t -> Names.inductive -> unitMutual Minimality/Induction scheme. force_mutual forces the construction of eliminators having the same predicates and methods even if some of the inductives are not recursive. By default it is false and some of the eliminators are defined as simple case analysis. By default isrec is true.
val do_mutual_induction_scheme : ?force_mutual:bool -> Environ.env -> ?isrec:bool ->
resolved_scheme list -> unitMain calls to interpret the Scheme command
val do_scheme : Environ.env -> (Names.Id.t CAst.t option * Vernacexpr.scheme) list -> unitMain call to Scheme Equality command
val do_scheme_equality : ?locmap:Ind_tables.Locmap.t -> Vernacexpr.equality_scheme_type -> Libnames.qualid Constrexpr.or_by_notation -> unitCombine a list of schemes into a conjunction of them
val build_combined_scheme : Environ.env -> Names.Constant.t list -> Evd.evar_map * Constr.constr * Constr.typesval do_combined_scheme : Names.lident -> Names.Constant.t list -> unitHook called at each inductive type definition
val declare_default_schemes : ?locmap:Ind_tables.Locmap.t -> Names.MutInd.t -> unit