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