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 : 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.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
val encode_mind : Names.DirPath.t -> Names.Id.t -> Names.MutInd.t
val pop_global_reference : Names.GlobRef.t -> Names.GlobRef.t
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