From 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 13 Jun 2018 00:22:57 +0200
Subject: 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.
---
 printing/printer.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 72030dc9f6..d76bd1e2b2 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -229,15 +229,15 @@ let dirpath_of_global = function
     dirpath_of_mp (MutInd.modpath kn)
   | VarRef _ -> DirPath.empty
 
-let qualid_of_global env r =
-  Libnames.make_qualid (dirpath_of_global r) (id_of_global env r)
+let qualid_of_global ?loc env r =
+  Libnames.make_qualid ?loc (dirpath_of_global r) (id_of_global env r)
 
 let safe_gen f env sigma c =
   let orig_extern_ref = Constrextern.get_extern_reference () in
   let extern_ref ?loc vars r =
     try orig_extern_ref vars r
     with e when CErrors.noncritical e ->
-      CAst.make ?loc @@ Libnames.Qualid (qualid_of_global env r)
+      qualid_of_global ?loc env r
   in
   Constrextern.set_extern_reference extern_ref;
   try
-- 
cgit v1.2.3