Module Smartlocate

val locate_global_with_alias : ?⁠head:bool -> Libnames.qualid -> Names.GlobRef.t
val global_of_extended_global : Globnames.extended_global_reference -> Names.GlobRef.t

Extract a global_reference from a reference that can be an "alias"

val global_with_alias : ?⁠head:bool -> Libnames.qualid -> Names.GlobRef.t

Locate a reference taking into account possible "alias" notations. May raise Nametab.GlobalizationError _ for an unknown reference, or a UserError if bound to a syntactic def that does not denote a reference.

val global_constant_with_alias : Libnames.qualid -> Names.Constant.t

The same for constants

val global_inductive_with_alias : Libnames.qualid -> Names.inductive

The same for inductive types

val global_constructor_with_alias : Libnames.qualid -> Names.constructor

The same for constructors of an inductive type

val smart_global : ?⁠head:bool -> Libnames.qualid Constrexpr.or_by_notation -> Names.GlobRef.t

Locate a reference taking into account notations and "aliases"

val smart_global_constant : Libnames.qualid Constrexpr.or_by_notation -> Names.Constant.t

The same for constants

val smart_global_inductive : Libnames.qualid Constrexpr.or_by_notation -> Names.inductive

The same for inductive types

val smart_global_constructor : Libnames.qualid Constrexpr.or_by_notation -> Names.constructor

The same for constructors of an inductive type