Module Ind_tables
type mutualtype individualtype 'a scheme_kindtype internal_flag=|UserAutomaticRequest|InternalTacticRequest|UserIndividualRequesttype scheme_dependency=|SchemeMutualDep of Names.MutInd.t * mutual scheme_kind|SchemeIndividualDep of Names.inductive * individual scheme_kindtype mutual_scheme_object_function= internal_flag -> Names.MutInd.t -> Constr.constr array Evd.in_evar_universe_contexttype individual_scheme_object_function= internal_flag -> Names.inductive -> Constr.constr Evd.in_evar_universe_context
val declare_mutual_scheme_object : string -> ?deps:(Names.MutInd.t -> scheme_dependency list) -> ?aux:string -> mutual_scheme_object_function -> mutual scheme_kindval declare_individual_scheme_object : string -> ?deps:(Names.inductive -> scheme_dependency list) -> ?aux:string -> individual_scheme_object_function -> individual scheme_kind
val define_individual_scheme : individual scheme_kind -> internal_flag -> Names.Id.t option -> Names.inductive -> unitval define_mutual_scheme : mutual scheme_kind -> internal_flag -> (int * Names.Id.t) list -> Names.MutInd.t -> unitval find_scheme : ?mode:internal_flag -> 'a scheme_kind -> Names.inductive -> Names.Constant.t Proofview.tacticMain function to retrieve a scheme in the cache or to generate it
val lookup_scheme : 'a scheme_kind -> Names.inductive -> Names.Constant.t optionLike
find_schemebut does not generate a constant on the fly
val pr_scheme_kind : 'a scheme_kind -> Pp.tval declare_definition_scheme : (internal:bool -> univs:Entries.universes_entry -> role:Evd.side_effect_role -> name:Names.Id.t -> Constr.t -> Names.Constant.t * Evd.side_effects) Stdlib.ref