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, 7 insertions, 7 deletions

diff --git a/library/library.ml b/library/library.ml
index 56d2709d5..400f3dcf1 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -577,10 +577,10 @@ let require_library_from_dirpath modrefl export =
 
 (* the function called by Vernacentries.vernac_import *)
 
-let safe_locate_module {CAst.loc;v=qid} =
+let safe_locate_module qid =
   try Nametab.locate_module qid
   with Not_found ->
-    user_err ?loc ~hdr:"import_library"
+    user_err ?loc:qid.CAst.loc ~hdr:"import_library"
       (pr_qualid qid ++ str " is not a module")
 
 let import_module export modl =
@@ -595,18 +595,18 @@ let import_module export modl =
     | [] -> ()
     | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
   let rec aux acc = function
-    | ({CAst.loc; v=dir} as m) :: l ->
+    | qid :: l ->
         let m,acc =
-          try Nametab.locate_module dir, acc
-          with Not_found-> flush acc; safe_locate_module m, [] in
+          try Nametab.locate_module qid, acc
+          with Not_found-> flush acc; safe_locate_module qid, [] in
         (match m with
         | MPfile dir -> aux (dir::acc) l
         | mp ->
             flush acc;
             try Declaremods.import_module export mp; aux [] l
             with Not_found ->
-              user_err ?loc ~hdr:"import_library"
-                (pr_qualid dir ++ str " is not a module"))
+              user_err ?loc:qid.CAst.loc ~hdr:"import_library"
+                (pr_qualid qid ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl