Ind_tables
This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand
A scheme is either a "mutual scheme_kind" or an "individual scheme_kind"
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
Main functions to register a scheme builder. Note these functions are not safe to be used by plugins as their effects won't be undone on backtracking
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
Force generation of a (mutually) scheme with possibly user-level names
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