coq 8.7.2 · OCaml Package

type 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

val destIndRef : global_reference -> Names.inductive

val destConstructRef : global_reference -> Names.constructor

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

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

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

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

val printable_constr_of_global : global_reference -> Term.constr

val global_of_constr : Term.constr -> global_reference

val reference_of_constr : Term.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.kernel_name

type extended_global_reference =

module ExtRefOrdered : sig ... end

type global_reference_or_constr =

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

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

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

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

val pop_con : Names.constant -> Names.constant

val pop_kn : Names.mutual_inductive -> Names.mutual_inductive

val pop_global_reference : global_reference -> global_reference

package coq