From 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
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.
---
 plugins/ssr/ssrcommon.ml  |  2 +-
 plugins/ssr/ssrparser.ml4 |  6 ++++--
 plugins/ssr/ssrvernac.ml4 | 16 +++++++---------
 3 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 2a31157be..54f3f9c71 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -858,7 +858,7 @@ open Util
 (** Constructors for constr_expr *)
 let mkCProp loc = CAst.make ?loc @@ CSort GProp
 let mkCType loc = CAst.make ?loc @@ CSort (GType [])
-let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None)
+let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)
 let rec mkCHoles ?loc n =
   if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
 let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 352f88bb3..7a1d06fdc 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1154,7 +1154,8 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar
 END
 
 let bvar_lname = let open CAst in function
-  | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id
+  | { v = CRef (qid, _) } when qualid_is_ident qid ->
+    CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid)
   | { loc = loc } -> CAst.make ?loc Anonymous
 
 let pr_ssrbinder prc _ _ (_, c) = prc c
@@ -1246,7 +1247,8 @@ END
 let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd
 
 let bvar_locid = function
-  | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id
+  | { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
+    CAst.make ?loc:qid.CAst.loc (qualid_basename qid)
   | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"")
 
 
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 939e97866..7ce2dd64a 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -28,7 +28,6 @@ open Globnames
 open Stdarg
 open Genarg
 open Decl_kinds
-open Libnames
 open Pp
 open Ppconstr
 open Printer
@@ -143,21 +142,21 @@ END
 let declare_one_prenex_implicit locality f =
   let fref =
     try Smartlocate.global_with_alias f 
-    with _ -> errorstrm (pr_reference f ++ str " is not declared") in
+    with _ -> errorstrm (pr_qualid f ++ str " is not declared") in
   let rec loop = function
   | a :: args' when Impargs.is_status_implicit a ->
     (ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args'
   | args' when List.exists Impargs.is_status_implicit args' ->
-      errorstrm (str "Expected prenex implicits for " ++ pr_reference f)
+      errorstrm (str "Expected prenex implicits for " ++ pr_qualid f)
   | _ -> [] in
   let impls =
     match Impargs.implicits_of_global fref  with
     | [cond,impls] -> impls
-    | [] -> errorstrm (str "Expected some implicits for " ++ pr_reference f)
+    | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f)
     | _ -> errorstrm (str "Multiple implicits not supported") in
   match loop impls  with
   | [] ->
-    errorstrm (str "Expected some implicits for " ++ pr_reference f)
+    errorstrm (str "Expected some implicits for " ++ pr_qualid f)
   | impls ->
     Impargs.declare_manual_implicits locality fref ~enriching:false [impls]
 
@@ -415,7 +414,7 @@ let interp_search_arg arg =
 
 (* Module path postfilter *)
 
-let pr_modloc (b, m) = if b then str "-" ++ pr_reference m else pr_reference m
+let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m
 
 let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc
 
@@ -433,10 +432,9 @@ GEXTEND Gram
 END
 
 let interp_modloc mr =
-  let interp_mod (_, mr) =
-    let {CAst.loc=loc; v=qid} = qualid_of_reference mr in
+  let interp_mod (_, qid) =
     try Nametab.full_name_module qid with Not_found ->
-    CErrors.user_err ?loc (str "No Module " ++ pr_qualid qid) in
+    CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in
   let mr_out, mr_in = List.partition fst mr in
   let interp_bmod b = function
   | [] -> fun _ _ _ -> true
-- 
cgit v1.2.3