Smartlocatelocate_global_with_alias locates global reference possibly following a notation if this notation has a role of aliasing; raise Not_found if not bound in the global env; raise a UserError if bound to a syntactic def that does not denote a reference
val locate_global_with_alias : ?head:bool -> Libnames.qualid -> Names.GlobRef.tval global_of_extended_global :
Globnames.extended_global_reference ->
Names.GlobRef.t optionExtract a global_reference from a reference that can be an "alias". If the reference points to a more complex term, we return None
val global_with_alias : ?head:bool -> Libnames.qualid -> Names.GlobRef.tLocate 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.tThe same for constants
val global_inductive_with_alias : Libnames.qualid -> Names.inductiveThe same for inductive types
val global_constructor_with_alias : Libnames.qualid -> Names.constructorThe same for constructors of an inductive type
val smart_global :
?head:bool ->
Libnames.qualid Constrexpr.or_by_notation ->
Names.GlobRef.tLocate a reference taking into account notations and "aliases"
val smart_global_constant :
Libnames.qualid Constrexpr.or_by_notation ->
Names.Constant.tThe same for constants
val smart_global_inductive :
Libnames.qualid Constrexpr.or_by_notation ->
Names.inductiveThe same for inductive types
val smart_global_constructor :
Libnames.qualid Constrexpr.or_by_notation ->
Names.constructorThe same for constructors of an inductive type