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_ustate
type individual_scheme_object_function = Environ.env -> handle -> Names.inductive -> Constr.constr Evd.in_ustate
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.
In declare_X_scheme_object key ?suff ?deps f
, key
is the name of the scheme kind. It must be unique across the Coq process's lifetime. It is used to generate scheme_kind
in a marshal-stable way and as the scheme name in Register Scheme.
suff
defaults to key
, generated schemes which aren't given an explicit name will be named "ind_suff" where "ind" is the inductive's name.
val declare_mutual_scheme_object : string -> ?suff:string -> ?deps:(Environ.env -> Names.MutInd.t -> scheme_dependency list) ->
mutual_scheme_object_function -> mutual scheme_kind
val declare_individual_scheme_object : string -> ?suff:string ->
?deps:(Environ.env -> Names.inductive -> scheme_dependency list) -> individual_scheme_object_function -> individual scheme_kind
val scheme_kind_name : _ scheme_kind -> string
Name of a scheme_kind
. Can be used to register with DeclareScheme.
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