Remove reference name type.

reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.

We remove the reference type and replace its uses by qualid.

1 files changed, 5 insertions, 5 deletions

diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 6b574d7b5a..e41ef78913 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -17,7 +17,7 @@ open Globnames
    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 -> qualid CAst.t -> GlobRef.t
+val locate_global_with_alias : ?head:bool -> qualid -> GlobRef.t
 
 (** Extract a global_reference from a reference that can be an "alias" *)
 val global_of_extended_global : extended_global_reference -> GlobRef.t
@@ -26,13 +26,13 @@ val global_of_extended_global : extended_global_reference -> GlobRef.t
     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_with_alias : ?head:bool -> reference -> GlobRef.t
+val global_with_alias : ?head:bool -> qualid -> GlobRef.t
 
 (** The same for inductive types *)
-val global_inductive_with_alias : reference -> inductive
+val global_inductive_with_alias : qualid -> inductive
 
 (** Locate a reference taking into account notations and "aliases" *)
-val smart_global : ?head:bool -> reference Constrexpr.or_by_notation -> GlobRef.t
+val smart_global : ?head:bool -> qualid Constrexpr.or_by_notation -> GlobRef.t
 
 (** The same for inductive types *)
-val smart_global_inductive : reference Constrexpr.or_by_notation -> inductive
+val smart_global_inductive : qualid Constrexpr.or_by_notation -> inductive