Module Ind_tables

This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand

type mutual
type individual
type 'a scheme_kind
type mutual_scheme_object_function = Declare.internal_flag -> Names.MutInd.t -> Constr.constr array Evd.in_evar_universe_context * Safe_typing.private_constants
type individual_scheme_object_function = Declare.internal_flag -> Names.inductive -> Constr.constr Evd.in_evar_universe_context * Safe_typing.private_constants
val declare_mutual_scheme_object : string -> ?⁠aux:string -> mutual_scheme_object_function -> mutual scheme_kind
val declare_individual_scheme_object : string -> ?⁠aux:string -> individual_scheme_object_function -> individual scheme_kind
val define_individual_scheme : individual scheme_kind -> Declare.internal_flag -> Names.Id.t option -> Names.inductive -> Names.Constant.t * Safe_typing.private_constants
val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag -> (int * Names.Id.t) list -> Names.MutInd.t -> Names.Constant.t array * Safe_typing.private_constants
val find_scheme : ?⁠mode:Declare.internal_flag -> 'a scheme_kind -> Names.inductive -> Names.Constant.t * Safe_typing.private_constants

Main function to retrieve a scheme in the cache or to generate it

val check_scheme : 'a scheme_kind -> Names.inductive -> bool
val pr_scheme_kind : 'a scheme_kind -> Pp.t