Globnamesval isVarRef : Names.GlobRef.t -> boolval isConstRef : Names.GlobRef.t -> boolval isIndRef : Names.GlobRef.t -> boolval isConstructRef : Names.GlobRef.t -> boolval canonical_gr : Names.GlobRef.t -> Names.GlobRef.tval destVarRef : Names.GlobRef.t -> Names.variableval destConstRef : Names.GlobRef.t -> Names.Constant.tval destIndRef : Names.GlobRef.t -> Names.inductiveval destConstructRef : Names.GlobRef.t -> Names.constructorval subst_global : Mod_subst.substitution -> Names.GlobRef.t -> Names.GlobRef.t * Constr.constr UVars.univ_abstracted optionval subst_global_reference : Mod_subst.substitution -> Names.GlobRef.t -> Names.GlobRef.ttype abbreviation = Names.KerName.tval abbreviation_eq : abbreviation -> abbreviation -> boolmodule ExtRefOrdered : sig ... endmodule ExtRefSet : CSig.USetS with type elt = extended_global_referencemodule ExtRefMap : CMap.UExtS with type key = extended_global_reference and module Set := ExtRefSetval subst_extended_reference : Mod_subst.substitution -> extended_global_reference -> extended_global_reference