coq 8.8.1 · OCaml Package

type global_reference = Names.global_reference =

val isVarRef : global_reference -> bool

val isConstRef : global_reference -> bool

val isIndRef : global_reference -> bool

val isConstructRef : global_reference -> bool

val eq_gr : global_reference -> global_reference -> bool

val canonical_gr : global_reference -> global_reference

val destVarRef : global_reference -> Names.variable

val destConstRef : global_reference -> Names.Constant.t

val destIndRef : global_reference -> Names.inductive

val destConstructRef : global_reference -> Names.constructor

val is_global : global_reference -> Constr.constr -> bool

val subst_constructor : 
  Mod_subst.substitution ->
  Names.constructor ->
  Names.constructor * Constr.constr

val subst_global : 
  Mod_subst.substitution ->
  global_reference ->
  global_reference * Constr.constr

val subst_global_reference : 
  Mod_subst.substitution ->
  global_reference ->
  global_reference

val printable_constr_of_global : global_reference -> Constr.constr

val global_of_constr : Constr.constr -> global_reference

val reference_of_constr : Constr.constr -> global_reference

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 =

module ExtRefOrdered : sig ... end

type global_reference_or_constr =

val encode_mind : Names.DirPath.t -> Names.Id.t -> Names.MutInd.t

val decode_mind : Names.MutInd.t -> Names.DirPath.t * Names.Id.t

val encode_con : Names.DirPath.t -> Names.Id.t -> Names.Constant.t

val decode_con : Names.Constant.t -> Names.DirPath.t * Names.Id.t

val pop_con : Names.Constant.t -> Names.Constant.t

val pop_kn : Names.MutInd.t -> Names.MutInd.t

val pop_global_reference : global_reference -> global_reference

package coq