package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type global_reference =
  1. | VarRef of Names.variable
  2. | ConstRef of Names.constant
  3. | IndRef of Names.inductive
  4. | ConstructRef of Names.constructor
val isVarRef : global_reference -> bool
val isConstRef : global_reference -> bool
val isIndRef : global_reference -> bool
val isConstructRef : global_reference -> bool
val eq_gr : global_reference -> global_reference -> bool
val canonical_gr : global_reference -> global_reference
val destVarRef : global_reference -> Names.variable
val destConstRef : global_reference -> Names.constant
val destIndRef : global_reference -> Names.inductive
val destConstructRef : global_reference -> Names.constructor
val is_global : global_reference -> Term.constr -> bool
val subst_global_reference : Mod_subst.substitution -> global_reference -> global_reference
val printable_constr_of_global : global_reference -> Term.constr
val global_of_constr : Term.constr -> global_reference
val reference_of_constr : Term.constr -> global_reference
module RefOrdered : sig ... end
module RefOrdered_env : sig ... end
module Refset : sig ... end
module Refmap : sig ... end
module Refset_env : sig ... end
module Refmap_env : sig ... end
type syndef_name = Names.kernel_name
type extended_global_reference =
  1. | TrueGlobal of global_reference
  2. | SynDef of syndef_name
module ExtRefOrdered : sig ... end
type global_reference_or_constr =
  1. | IsGlobal of global_reference
  2. | IsConstr of Term.constr
val pop_global_reference : global_reference -> global_reference
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