Module `Ind_tables`

type mutual
type individual
type 'a scheme_kind
type handle
type scheme_dependency = | SchemeMutualDep of Names.MutInd.t * mutual scheme_kind | SchemeIndividualDep of Names.inductive * individual scheme_kind
type mutual_scheme_object_function = Environ.env -> handle -> Names.MutInd.t -> Constr.constr array Evd.in_evar_universe_context
type individual_scheme_object_function = Environ.env -> handle -> Names.inductive -> Constr.constr Evd.in_evar_universe_context

val declare_mutual_scheme_object : string -> ?⁠deps:(Environ.env -> Names.MutInd.t -> scheme_dependency list) -> ?⁠aux:string -> mutual_scheme_object_function -> mutual scheme_kind
val declare_individual_scheme_object : string -> ?⁠deps:(Environ.env -> Names.inductive -> scheme_dependency list) -> ?⁠aux:string -> individual_scheme_object_function -> individual scheme_kind

val define_individual_scheme : ?⁠loc:Loc.t -> individual scheme_kind -> Names.Id.t option -> Names.inductive -> unit

module Locmap : sig ... end

val define_mutual_scheme : ?⁠locmap:Locmap.t -> mutual scheme_kind -> (int * Names.Id.t) list -> Names.MutInd.t -> unit
val find_scheme : 'a scheme_kind -> Names.inductive -> Names.Constant.t Proofview.tactic: Main function to retrieve a scheme in the cache or to generate it

val lookup_scheme : 'a scheme_kind -> Names.inductive -> Names.Constant.t option: Like find_scheme but does not generate a constant on the fly

val local_lookup_scheme : handle -> 'a scheme_kind -> Names.inductive -> Names.Constant.t option: To be used by scheme-generating functions when looking for a subscheme.

val pr_scheme_kind : 'a scheme_kind -> Pp.t
val declare_definition_scheme : (internal:bool -> univs:UState.named_universes_entry -> role:Evd.side_effect_role -> name:Names.Id.t -> ?⁠loc:Loc.t -> Constr.t -> Names.Constant.t * Evd.side_effects) Stdlib.ref