package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type global_reference = Names.GlobRef.t =
  1. | VarRef of Names.variable
  2. | ConstRef of Names.Constant.t
  3. | IndRef of Names.inductive
  4. | ConstructRef of Names.constructor
  • deprecated Use Names.GlobRef.t
val isVarRef : Names.GlobRef.t -> bool
val isConstRef : Names.GlobRef.t -> bool
val isIndRef : Names.GlobRef.t -> bool
val isConstructRef : Names.GlobRef.t -> bool
val eq_gr : Names.GlobRef.t -> Names.GlobRef.t -> bool
  • deprecated Use Names.GlobRef.equal
val canonical_gr : Names.GlobRef.t -> Names.GlobRef.t
val destVarRef : Names.GlobRef.t -> Names.variable
val destConstRef : Names.GlobRef.t -> Names.Constant.t
val destIndRef : Names.GlobRef.t -> Names.inductive
val destConstructRef : Names.GlobRef.t -> Names.constructor
val is_global : Names.GlobRef.t -> Constr.constr -> bool
val subst_global_reference : Mod_subst.substitution -> Names.GlobRef.t -> Names.GlobRef.t
val printable_constr_of_global : Names.GlobRef.t -> Constr.constr
val global_of_constr : Constr.constr -> Names.GlobRef.t
module RefOrdered = Names.GlobRef.Ordered
module RefOrdered_env = Names.GlobRef.Ordered_env
module Refset = Names.GlobRef.Set
module Refmap = Names.GlobRef.Map
module Refset_env = Names.GlobRef.Set_env
module Refmap_env = Names.GlobRef.Map_env
type syndef_name = Names.KerName.t
type extended_global_reference =
  1. | TrueGlobal of Names.GlobRef.t
  2. | SynDef of syndef_name
module ExtRefOrdered : sig ... end
type global_reference_or_constr =
  1. | IsGlobal of Names.GlobRef.t
  2. | IsConstr of Constr.constr
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