package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 mutual
type individual
type 'a scheme_kind
type handle
type scheme_dependency =
  1. | SchemeMutualDep of Names.MutInd.t * mutual scheme_kind
  2. | 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.

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 is_declared_scheme_object : string -> bool

Is the string used as the name of a 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

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) ref
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct