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
    (*
    • deprecated Use Names.GlobRef.VarRef
    *)
  2. | ConstRef of Names.Constant.t
    (*
    • deprecated Use Names.GlobRef.ConstRef
    *)
  3. | IndRef of Names.inductive
    (*
    • deprecated Use Names.GlobRef.IndRef
    *)
  4. | ConstructRef of Names.constructor
    (*
    • deprecated Use Names.GlobRef.ConstructRef
    *)
  • 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 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
  • deprecated Use [Constr.isRefX] instead.
val subst_global_reference : Mod_subst.substitution -> Names.GlobRef.t -> Names.GlobRef.t
val printable_constr_of_global : Names.GlobRef.t -> Constr.constr

This constr is not safe to be typechecked, universe polymorphism is not handled here: just use for printing

val global_of_constr : Constr.constr -> Names.GlobRef.t

Turn a construction denoting a global reference into a global reference; raise Not_found if not a global reference

  • deprecated Use [Constr.destRef] instead (throws DestKO instead of Not_found).
Extended global references
type abbreviation = Names.KerName.t
type extended_global_reference =
  1. | TrueGlobal of Names.GlobRef.t
  2. | Abbrev of abbreviation
module ExtRefOrdered : sig ... end
module ExtRefMap : CMap.ExtS with type key = extended_global_reference and module Set := ExtRefSet
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