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

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 94149a085..1fa26b455 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -202,11 +202,11 @@ GEXTEND Gram
       | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),args)
       | "@"; lid = pattern_identref; args=LIST1 identref ->
           let { CAst.loc = locid; v = id } = lid in
-          let args = List.map (fun x -> CAst.make @@ CRef (CAst.make ?loc:x.CAst.loc @@ Ident x.CAst.v, None), None) args in
+          let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in
           CAst.make ~loc:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ]
     | "9"
         [ ".."; c = operconstr LEVEL "0"; ".." ->
-          CAst.make ~loc:!@loc @@ CAppExpl ((None, CAst.make ~loc:!@loc @@ Ident ldots_var, None),[c]) ]
+          CAst.make ~loc:!@loc @@ CAppExpl ((None, (qualid_of_ident ~loc:!@loc ldots_var), None),[c]) ]
     | "8" [ ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 08bcd0f8c..91dce27fe 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -18,7 +18,7 @@ let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
 let _ = List.iter CLexer.add_keyword prim_kw
 
 
-let local_make_qualid l id = make_qualid (DirPath.make l) id
+let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id
 
 let my_int_of_string loc s =
   try
@@ -67,8 +67,8 @@ GEXTEND Gram
       ] ]
   ;
   basequalid:
-    [ [ id = ident; (l,id')=fields -> local_make_qualid (l@[id]) id'
-      | id = ident -> qualid_of_ident id
+    [ [ id = ident; (l,id')=fields -> local_make_qualid !@loc (l@[id]) id'
+      | id = ident -> qualid_of_ident ~loc:!@loc id
       ] ]
   ;
   name:
@@ -77,8 +77,8 @@ GEXTEND Gram
   ;
   reference:
     [ [ id = ident; (l,id') = fields ->
-        CAst.make ~loc:!@loc @@ Qualid (local_make_qualid (l@[id]) id')
-      | id = ident -> CAst.make ~loc:!@loc @@ Ident id
+        local_make_qualid !@loc (l@[id]) id'
+      | id = ident -> local_make_qualid !@loc [] id
       ] ]
   ;
   by_notation:
@@ -89,7 +89,7 @@ GEXTEND Gram
       | ntn = by_notation -> CAst.make ~loc:!@loc @@ Constrexpr.ByNotation ntn ] ]
   ;
   qualid:
-    [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ]
+    [ [ qid = basequalid -> qid ] ]
   ;
   ne_string:
     [ [ s = STRING ->
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 9a45bc973..f959bd80c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -213,11 +213,11 @@ module Prim :
     val integer : int Gram.entry
     val string : string Gram.entry
     val lstring : lstring Gram.entry
-    val qualid : qualid CAst.t Gram.entry
+    val reference : qualid Gram.entry
+    val qualid : qualid Gram.entry
     val fullyqualid : Id.t list CAst.t Gram.entry
-    val reference : reference Gram.entry
     val by_notation : (string * string option) Gram.entry
-    val smart_global : reference or_by_notation Gram.entry
+    val smart_global : qualid or_by_notation Gram.entry
     val dirpath : DirPath.t Gram.entry
     val ne_string : string Gram.entry
     val ne_lstring : lstring Gram.entry
@@ -232,7 +232,7 @@ module Constr :
     val binder_constr : constr_expr Gram.entry
     val operconstr : constr_expr Gram.entry
     val ident : Id.t Gram.entry
-    val global : reference Gram.entry
+    val global : qualid Gram.entry
     val universe_level : Glob_term.glob_level Gram.entry
     val sort : Glob_term.glob_sort Gram.entry
     val sort_family : Sorts.family Gram.entry