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 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 ExtRefMap : CMap.ExtS with type key = extended_global_reference and module Set := ExtRefSet