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