package coq

  1. Overview
  2. Docs
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
val global_of_constr : Constr.constr -> Names.GlobRef.t
  • deprecated Use [Constr.destRef] instead (throws DestKO instead of Not_found).
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
module ExtRefSet : sig ... end
module ExtRefMap : sig ... end