package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type mutual
type individual
type 'a scheme_kind
type internal_flag =
  1. | UserAutomaticRequest
  2. | InternalTacticRequest
  3. | UserIndividualRequest
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 = internal_flag -> Names.MutInd.t -> Constr.constr array Evd.in_evar_universe_context
type individual_scheme_object_function = internal_flag -> Names.inductive -> Constr.constr Evd.in_evar_universe_context
val declare_mutual_scheme_object : string -> ?deps:(Names.MutInd.t -> scheme_dependency list) -> ?aux:string -> mutual_scheme_object_function -> mutual scheme_kind
val declare_individual_scheme_object : string -> ?deps:(Names.inductive -> scheme_dependency list) -> ?aux:string -> individual_scheme_object_function -> individual scheme_kind
val define_individual_scheme : individual scheme_kind -> internal_flag -> Names.Id.t option -> Names.inductive -> unit
val define_mutual_scheme : mutual scheme_kind -> internal_flag -> (int * Names.Id.t) list -> Names.MutInd.t -> unit
val lookup_scheme : 'a scheme_kind -> Names.inductive -> Names.Constant.t option
val pr_scheme_kind : 'a scheme_kind -> Pp.t
val declare_definition_scheme : (internal:bool -> univs:Entries.universes_entry -> role:Evd.side_effect_role -> name:Names.Id.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