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.

3 files changed, 14 insertions, 6 deletions

diff --git a/dev/base_include b/dev/base_include
index 574bc097e..6f54ecb24 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -229,7 +229,7 @@ let pf_e gl s =
 let _ = Flags.in_debugger := false
 let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
-  (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
+  (fun ?loc _ r -> Nametab.shortest_qualid_of_global ?loc Id.Set.empty r);;
 
 let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc))
 
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index bb8189efc..f3fc126f9 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,14 @@
 
 ### ML API
 
+Names
+
+- In `Libnames`, the type `reference` and its two constructors `Qualid` and
+  `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity,
+  `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be
+  replaced by a test using `qualid_is_ident`. Extracting the ident part of a
+  qualid can be done using `qualid_basename`.
+
 Misctypes
 
 - Syntax for universe sorts and kinds has been moved from `Misctypes`
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 10a7a4158..844ad9188 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -549,8 +549,8 @@ let encode_path ?loc prefix mpdir suffix id =
     | Some (mp,dir) ->
 	(DirPath.repr (dirpath_of_string (ModPath.to_string mp))@
 	DirPath.repr dir) in
-  CAst.make ?loc @@ Qualid (make_qualid
-    (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
+  make_qualid ?loc
+    (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id
 
 let raw_string_of_ref ?loc _ = function
   | ConstRef cst ->
@@ -569,9 +569,9 @@ let raw_string_of_ref ?loc _ = function
       encode_path ?loc "SECVAR" None [] id
 
 let short_string_of_ref ?loc _ = function
-  | VarRef id -> CAst.make ?loc @@ Ident id
-  | ConstRef cst -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (Constant.repr3 cst)))
-  | IndRef (kn,0) -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (MutInd.repr3 kn)))
+  | VarRef id -> qualid_of_ident ?loc id
+  | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (pi3 (Constant.repr3 cst)))
+  | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (pi3 (MutInd.repr3 kn)))
   | IndRef (kn,i) ->
       encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))]
         (Id.of_string ("_"^string_of_int i))