Merge PR #7797: Remove reference name type.

32 files changed, 196 insertions, 205 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 1e0589fac..4ede11b5c 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -596,19 +596,18 @@ let warns () =
 
 let rec locate_ref = function
   | [] -> [],[]
-  | r::l ->
-      let q = qualid_of_reference r in
-      let mpo = try Some (Nametab.locate_module q.CAst.v) with Not_found -> None
+  | qid::l ->
+      let mpo = try Some (Nametab.locate_module qid) with Not_found -> None
       and ro =
-        try Some (Smartlocate.global_with_alias r)
+        try Some (Smartlocate.global_with_alias qid)
         with Nametab.GlobalizationError _ | UserError _ -> None
       in
       match mpo, ro with
-	| None, None -> Nametab.error_global_not_found q
+        | None, None -> Nametab.error_global_not_found qid
 	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
 	| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
 	| Some mp, Some r ->
-           warning_ambiguous_name (q.CAst.v,mp,r);
+           warning_ambiguous_name (qid,mp,r);
            let refs,mps = locate_ref l in refs,mp::mps
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 77f1fb5ef..54fde2ca4 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -13,14 +13,14 @@
 open Names
 open Libnames
 
-val simple_extraction : reference -> unit
-val full_extraction : string option -> reference list -> unit
-val separate_extraction : reference list -> unit
+val simple_extraction : qualid -> unit
+val full_extraction : string option -> qualid list -> unit
+val separate_extraction : qualid list -> unit
 val extraction_library : bool -> Id.t -> unit
 
 (* For the test-suite : extraction to a temporary file + ocamlc on it *)
 
-val extract_and_compile : reference list -> unit
+val extract_and_compile : qualid list -> unit
 
 (* For debug / external output via coqtop.byte + Drop : *)
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 5bf944434..a8baeaf1b 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -194,17 +194,17 @@ val find_custom_match : ml_branch array -> string
 (*s Extraction commands. *)
 
 val extraction_language : lang -> unit
-val extraction_inline : bool -> reference list -> unit
+val extraction_inline : bool -> qualid list -> unit
 val print_extraction_inline : unit -> Pp.t
 val reset_extraction_inline : unit -> unit
 val extract_constant_inline :
-  bool -> reference -> string list -> string -> unit
+  bool -> qualid -> string list -> string -> unit
 val extract_inductive :
-  reference -> string -> string list -> string option -> unit
+  qualid -> string -> string list -> string option -> unit
 
 
 type int_or_id = ArgInt of int | ArgId of Id.t
-val extraction_implicit : reference -> int_or_id list -> unit
+val extraction_implicit : qualid -> int_or_id list -> unit
 
 (*s Table of blacklisted filenames *)
 
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 30deb6f49..7e54bc8ad 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -17,7 +17,6 @@ open Goptions
 open Tacmach.New
 open Tacticals.New
 open Tacinterp
-open Libnames
 open Stdarg
 open Tacarg
 open Pcoq.Prim
@@ -127,7 +126,7 @@ let normalize_evaluables=
 open Genarg
 open Ppconstr
 open Printer
-let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference
+let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid
 let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x)))
 let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index a158fc8ff..31496513a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -627,7 +627,7 @@ let build_scheme fas =
 		Smartlocate.global_with_alias f
 	      with Not_found ->
                 user_err ~hdr:"FunInd.build_scheme"
-                  (str "Cannot find " ++ Libnames.pr_reference f)
+                  (str "Cannot find " ++ Libnames.pr_qualid f)
 	    in
             let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
             let _ = evd := evd' in 
@@ -668,7 +668,7 @@ let build_case_scheme fa =
     try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
     with Not_found ->
       user_err ~hdr:"FunInd.build_case_scheme"
-        (str "Cannot find " ++ Libnames.pr_reference f) in
+        (str "Cannot find " ++ Libnames.pr_qualid f) in
   let first_fun,u = destConst  funs in
   let funs_mp,funs_dp,_ = Constant.repr3 first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 33aeafef8..97f9acdb3 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -36,5 +36,5 @@ exception No_graph_found
 val make_scheme :   Evd.evar_map ref ->
  (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list
 
-val build_scheme : (Id.t*Libnames.reference*Sorts.family) list ->  unit
-val build_case_scheme : (Id.t*Libnames.reference*Sorts.family)  ->  unit
+val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list ->  unit
+val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family)  ->  unit
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 9899b7b21..a2d31780d 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -168,7 +168,7 @@ END
 
 let pr_fun_scheme_arg (princ_name,fun_name,s) =
   Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
-  Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++
+  Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++
   Termops.pr_sort_family s
 
 VERNAC ARGUMENT EXTEND fun_scheme_arg
@@ -181,11 +181,11 @@ let warning_error names e =
   let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
-       let names = pr_enum Libnames.pr_reference names in
+       let names = pr_enum Libnames.pr_qualid names in
        let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in
        warn_cannot_define_graph (names,error)
     | Defining_principle e ->
-       let names = pr_enum Libnames.pr_reference names in
+       let names = pr_enum Libnames.pr_qualid names in
        let error = if do_observe () then CErrors.print e else mt () in
        warn_cannot_define_principle (names,error)
     | _ -> raise e
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index cd640eebd..489a40ed0 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -362,17 +362,17 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	(*i The next call to mk_rel_id is valid since we have just construct the graph
 	   Ensures by : do_built
 	i*)
-        let f_R_mut = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in
+        let f_R_mut = qualid_of_ident @@ mk_rel_id (List.nth names 0) in
 	let ind_kn =
 	  fst (locate_with_msg
-		 (pr_reference f_R_mut++str ": Not an inductive type!")
+                 (pr_qualid f_R_mut++str ": Not an inductive type!")
 		 locate_ind
 		 f_R_mut)
 	in
 	let fname_kn (((fname,_),_,_,_,_),_) =
-          let f_ref = CAst.map (fun n -> Ident n) fname in
-	  locate_with_msg
-	    (pr_reference f_ref++str ": Not an inductive type!")
+   let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in
+          locate_with_msg
+            (pr_qualid f_ref++str ": Not an inductive type!")
 	    locate_constant
 	    f_ref
 	in
@@ -477,7 +477,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
   let unbounded_eq =
     let f_app_args =
       CAst.make @@ Constrexpr.CAppExpl(
-         (None,CAst.make @@ Ident fname,None) ,
+         (None,qualid_of_ident fname,None) ,
 	 (List.map
 	    (function
                | {CAst.v=Anonymous} -> assert false
@@ -487,7 +487,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	 )
 	)
     in
-    CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))),
+    CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (qualid_of_string "Logic.eq")),
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
@@ -544,9 +544,9 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
       | None ->
 	  let ltof =
 	    let make_dir l = DirPath.make (List.rev_map Id.of_string l) in
-            CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path
-			       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")))
-	  in
+            Libnames.qualid_of_path
+              (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))
+          in
 	  let fun_from_mes =
 	    let applied_mes =
 	      Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg])    in
@@ -727,12 +727,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof
   ()
 
 let rec add_args id new_args = CAst.map (function
-  | CRef (r,_) as b ->
-      begin match r with
-        | {CAst.v=Libnames.Ident fname} when Id.equal fname id ->
-	    CAppExpl((None,r,None),new_args)
-	| _ -> b
-      end
+  | CRef (qid,_) as b ->
+    if qualid_is_ident qid && Id.equal (qualid_basename qid) id then
+      CAppExpl((None,qid,None),new_args)
+    else b
   | CFix  _  | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.")
   | CProdN(nal,b1) ->
         CProdN(List.map (function  CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2)
@@ -746,13 +744,10 @@ let rec add_args id new_args = CAst.map (function
 	       add_args id new_args  b1)
   | CLetIn(na,b1,t,b2) ->
       CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2)
-  | CAppExpl((pf,r,us),exprl) ->
-      begin
-	match r with
-        | {CAst.v=Libnames.Ident fname} when Id.equal fname id ->
-	    CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl))
-	| _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl)
-      end
+  | CAppExpl((pf,qid,us),exprl) ->
+    if qualid_is_ident qid && Id.equal (qualid_basename qid) id then
+      CAppExpl((pf,qid,us),new_args@(List.map (add_args id new_args) exprl))
+    else CAppExpl((pf,qid,us),List.map (add_args id new_args) exprl)
   | CApp((pf,b),bl) ->
       CApp((pf,add_args id new_args b),
 	   List.map (fun (e,o) -> add_args id new_args e,o) bl)
@@ -888,7 +883,7 @@ let make_graph (f_ref : GlobRef.t) =
 				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
                                         (fun {CAst.loc;v=n} -> CAst.make ?loc @@
-                                           CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None))
+                                           CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None))
 					nal
                                   | Constrexpr.CLocalPattern _ -> assert false
 			       )
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index c6faa142a..4eee2c7a4 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -31,9 +31,7 @@ let id_of_name = function
     Name id -> id
   | _ -> raise Not_found
 
-let locate  ref =
-    let {CAst.v=qid} = qualid_of_reference ref in
-    Nametab.locate qid
+let locate qid = Nametab.locate qid
 
 let locate_ind ref =
   match locate ref with
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 346b21ef2..7e52ee224 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -20,11 +20,11 @@ val array_get_start : 'a array -> 'a array
 
 val id_of_name : Name.t -> Id.t
 
-val locate_ind : Libnames.reference -> inductive
-val locate_constant : Libnames.reference -> Constant.t
+val locate_ind : Libnames.qualid -> inductive
+val locate_constant : Libnames.qualid -> Constant.t
 val locate_with_msg :
-  Pp.t -> (Libnames.reference -> 'a) ->
-  Libnames.reference -> 'a
+  Pp.t -> (Libnames.qualid -> 'a) ->
+  Libnames.qualid -> 'a
 
 val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list
 val list_union_eq :
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index aa49148fc..7298342e1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1325,7 +1325,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
     CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
   let hook _ _ =
     let opacity =
-      let na_ref = CAst.make @@ Libnames.Ident na in
+      let na_ref = qualid_of_ident na in
       let na_global = Smartlocate.global_with_alias na_ref in
       match na_global with
 	  ConstRef c -> is_opaque_constant c
@@ -1577,7 +1577,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let hook _ _ = 
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
-    let _ = Extraction_plugin.Table.extraction_inline true [CAst.make @@ Ident term_id] in
+    let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in
     (*     message "start second proof"; *)
     let stop = 
       try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 642e52155..35ed14fc1 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -173,7 +173,7 @@ TACTIC EXTEND convert_concl_no_check
 | ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ]
 END
 
-let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference
+let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid
 let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global
 let glob_hints_path_atom ist = Hints.glob_hints_path_atom
 
@@ -189,7 +189,7 @@ ARGUMENT EXTEND hints_path_atom
 END
 
 let pr_hints_path prc prx pry c = Hints.pp_hints_path c
-let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c
+let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c
 let glob_hints_path ist = Hints.glob_hints_path
 
 ARGUMENT EXTEND hints_path
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index d7d642e50..620f14707 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -39,11 +39,12 @@ let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat
 let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
 let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
 
-let reference_to_id = CAst.map_with_loc (fun ?loc -> function
-  | Libnames.Ident id -> id
-  | Libnames.Qualid _ ->
-    CErrors.user_err ?loc
-      (str "This expression should be a simple identifier."))
+let reference_to_id qid =
+  if Libnames.qualid_is_ident qid then
+    CAst.make ?loc:qid.CAst.loc @@ Libnames.qualid_basename qid
+  else
+    CErrors.user_err ?loc:qid.CAst.loc
+      (str "This expression should be a simple identifier.")
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
 
@@ -199,8 +200,7 @@ GEXTEND Gram
      verbose most of the time. *)
   fresh_id:
     [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*)
-        | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in
-                          Locus.ArgVar (CAst.make ~loc:!@loc id) ] ]
+        | qid = qualid -> Locus.ArgVar (CAst.make ~loc:!@loc @@ Libnames.qualid_basename qid) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
@@ -475,7 +475,7 @@ END
 
 VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
 | [ "Print" "Ltac" reference(r) ] ->
-  [ Feedback.msg_notice (Tacintern.print_ltac (Libnames.qualid_of_reference r).CAst.v) ]
+  [ Feedback.msg_notice (Tacintern.print_ltac r) ]
 END
 
 VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
@@ -483,7 +483,7 @@ VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
   [ Tacentries.print_located_tactic r ]
 END
 
-let pr_ltac_ref = Libnames.pr_reference
+let pr_ltac_ref = Libnames.pr_qualid
 
 let pr_tacdef_body tacdef_body =
   let id, redef, body =
@@ -510,8 +510,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
 | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [
     VtSideff (List.map (function
       | TacticDefinition ({CAst.v=r},_) -> r
-      | TacticRedefinition ({CAst.v=Ident r},_) -> r
-      | TacticRedefinition ({CAst.v=Qualid q},_) -> snd(repr_qualid q)) l), VtLater
+      | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
   ] -> [ fun ~atts ~st -> let open Vernacinterp in
            Tacentries.register_ltac (Locality.make_module_locality atts.locality) l;
            st
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 352e92c2a..1f56244c7 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -12,7 +12,6 @@
   Syntax for the subtac terms and types.
   Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
 
-open Libnames
 open Constrexpr
 open Constrexpr_ops
 open Stdarg
@@ -49,7 +48,7 @@ module Tactic = Pltac
 
 open Pcoq
 
-let sigref = mkRefC (CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Init.Specif.sig"))
+let sigref loc = mkRefC (Libnames.qualid_of_string ~loc "Coq.Init.Specif.sig")
 
 type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
 
@@ -68,7 +67,7 @@ GEXTEND Gram
 
   Constr.closed_binder:
     [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
-	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
+          let typ = mkAppC (sigref !@loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in
           [CLocalAssum ([id], default_binder_kind, typ)]
     ] ];
 
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 2189e224f..f1634f156 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -67,13 +67,13 @@ let subst_strategy s str = str
 
 let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
 let pr_raw_strategy prc prlc _ (s : raw_strategy) =
-  let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_reference, prc) in
+  let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in
   Rewrite.pr_strategy prc prr s
 let pr_glob_strategy prc prlc _ (s : glob_strategy) =
   let prr = Pptactic.pr_red_expr
     (Ppconstr.pr_constr_expr,
     Ppconstr.pr_lconstr_expr,
-    Pputils.pr_or_by_notation Libnames.pr_reference,
+    Pputils.pr_or_by_notation Libnames.pr_qualid,
     Ppconstr.pr_constr_expr)
   in
   Rewrite.pr_strategy prc prr s
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 05005c733..31bc34a32 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -156,7 +156,7 @@ let mkTacCase with_evar = function
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
   | [(clear,ElimOnIdent id),(None,None),None],None ->
-      TacCase (with_evar,(clear,(CAst.make @@ CRef (CAst.make ?loc:id.CAst.loc @@ Ident id.CAst.v,None),NoBindings)))
+      TacCase (with_evar,(clear,(CAst.make @@ CRef (qualid_of_ident ?loc:id.CAst.loc id.CAst.v,None),NoBindings)))
   | ic ->
       if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
       then
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 4c075d413..c5aa542fd 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -21,8 +21,8 @@ val open_constr : constr_expr Gram.entry
 val constr_with_bindings : constr_expr with_bindings Gram.entry
 val bindings : constr_expr bindings Gram.entry
 val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry
-val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
-val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
+val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry
+val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry
 val uconstr : constr_expr Gram.entry
 val quantified_hypothesis : quantified_hypothesis Gram.entry
 val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index e19a95e84..09179dad3 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -17,7 +17,6 @@ open Constrexpr
 open Genarg
 open Geninterp
 open Stdarg
-open Libnames
 open Notation_gram
 open Tactypes
 open Locus
@@ -1109,8 +1108,8 @@ let pr_goal_selector ~toplevel s =
       pr_lconstr = pr_lconstr_expr;
       pr_pattern = pr_constr_pattern_expr;
       pr_lpattern = pr_lconstr_pattern_expr;
-      pr_constant = pr_or_by_notation pr_reference;
-      pr_reference = pr_reference;
+      pr_constant = pr_or_by_notation pr_qualid;
+      pr_reference = pr_qualid;
       pr_name = pr_lident;
       pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg);
       pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
@@ -1323,7 +1322,7 @@ let () =
   let open Genprint in
   register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int;
   register_basic_print0 wit_ref
-    pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+    pr_qualid (pr_or_var (pr_located pr_global)) pr_global;
   register_basic_print0 wit_ident pr_id pr_id pr_id;
   register_basic_print0 wit_var pr_lident pr_lident pr_id;
   register_print0
@@ -1357,7 +1356,7 @@ let () =
   ;
   Genprint.register_print0
     wit_red_expr
-    (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)))
+    (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr)))
     (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)))
     pr_red_expr_env
   ;
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index cd04f4ae9..01c52c413 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1773,11 +1773,11 @@ let rec strategy_of_ast = function
 
 (* By default the strategy for "rewrite_db" is top-down *)
 
-let mkappc s l = CAst.make @@ CAppExpl ((None,CAst.make @@ Libnames.Ident (Id.of_string s),None),l)
+let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l)
 
 let declare_an_instance n s args =
   (((CAst.make @@ Name n),None), Explicit,
-   CAst.make @@ CAppExpl ((None, CAst.make @@ Qualid (qualid_of_string s),None), args))
+   CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args))
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
@@ -1791,17 +1791,17 @@ let anew_instance global binders instance fields =
 let declare_instance_refl global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
   in anew_instance global binders instance
-       [(CAst.make @@ Ident (Id.of_string "reflexivity"),lemma)]
+       [(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
 
 let declare_instance_sym global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
   in anew_instance global binders instance
-       [(CAst.make @@ Ident (Id.of_string "symmetry"),lemma)]
+       [(qualid_of_ident (Id.of_string "symmetry"),lemma)]
 
 let declare_instance_trans global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
   in anew_instance global binders instance
-       [(CAst.make @@ Ident (Id.of_string "transitivity"),lemma)]
+       [(qualid_of_ident (Id.of_string "transitivity"),lemma)]
 
 let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
@@ -1825,16 +1825,16 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
 	in ignore(
 	    anew_instance global binders instance
-              [(CAst.make @@ Ident (Id.of_string "PreOrder_Reflexive"), lemma1);
-               (CAst.make @@ Ident (Id.of_string "PreOrder_Transitive"),lemma3)])
+              [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
+               (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)])
     | (None, Some lemma2, Some lemma3) ->
 	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
 	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
 	in ignore(
 	    anew_instance global binders instance
-              [(CAst.make @@ Ident (Id.of_string "PER_Symmetric"), lemma2);
-               (CAst.make @@ Ident (Id.of_string "PER_Transitive"),lemma3)])
+              [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
+               (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)])
      | (Some lemma1, Some lemma2, Some lemma3) ->
 	let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
 	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
@@ -1842,9 +1842,9 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
 	in ignore(
 	  anew_instance global binders instance
-            [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), lemma1);
-             (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2);
-             (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)])
+            [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
+             (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
+             (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)])
 
 let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
 
@@ -1949,16 +1949,15 @@ let add_setoid global binders a aeq t n =
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in ignore(
     anew_instance global binders instance
-      [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
-       (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
-       (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
+      [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+       (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+       (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
 
 
 let make_tactic name =
   let open Tacexpr in
-  let tacpath = Libnames.qualid_of_string name in
-  let tacname = CAst.make @@ Qualid tacpath in
-  TacArg (Loc.tag @@ (TacCall (Loc.tag (tacname, []))))
+  let tacqid = Libnames.qualid_of_string name in
+  TacArg (Loc.tag @@ (TacCall (Loc.tag (tacqid, []))))
 
 let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
@@ -2008,7 +2007,7 @@ let add_morphism glob binders m s n =
   let instance =
     (((CAst.make @@ Name instance_id),None), Explicit,
     CAst.make @@ CAppExpl (
-             (None, CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
+             (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None),
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index fada7424c..98d451536 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -449,12 +449,12 @@ let register_ltac local tacl =
         in
         let () = if is_shadowed then warn_unusable_identifier id in
         NewTac id, body
-    | Tacexpr.TacticRedefinition (ident, body) ->
+    | Tacexpr.TacticRedefinition (qid, body) ->
         let kn =
-          try Tacenv.locate_tactic (qualid_of_reference ident).CAst.v
+          try Tacenv.locate_tactic qid
           with Not_found ->
-            CErrors.user_err ?loc:ident.CAst.loc
-                       (str "There is no Ltac named " ++ pr_reference ident ++ str ".")
+            CErrors.user_err ?loc:qid.CAst.loc
+                       (str "There is no Ltac named " ++ pr_qualid qid ++ str ".")
         in
         UpdateTac kn, body
   in
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 3f804ee8d..2bfbbe2e1 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -65,7 +65,7 @@ val create_ltac_quotation : string ->
 val print_ltacs : unit -> unit
 (** Display the list of ltac definitions currently available. *)
 
-val print_located_tactic : Libnames.reference -> unit
+val print_located_tactic : Libnames.qualid -> unit
 (** Display the absolute name of a tactic. *)
 
 type _ ty_sig =
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index d51de8c65..06d2711ad 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -333,8 +333,8 @@ type glob_tactic_arg =
 
 type r_trm = constr_expr
 type r_pat = constr_pattern_expr
-type r_cst = reference or_by_notation
-type r_ref = reference
+type r_cst = qualid or_by_notation
+type r_ref = qualid
 type r_nam = lident
 type r_lev = rlevel
 
@@ -399,4 +399,4 @@ type ltac_trace = ltac_call_kind Loc.located list
 
 type tacdef_body =
   | TacticDefinition of lident * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
-  | TacticRedefinition of reference * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
+  | TacticRedefinition of qualid * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 01eead164..71e1edfd7 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -333,8 +333,8 @@ type glob_tactic_arg =
 
 type r_trm = constr_expr
 type r_pat = constr_pattern_expr
-type r_cst = reference or_by_notation
-type r_ref = reference
+type r_cst = qualid or_by_notation
+type r_ref = qualid
 type r_nam = lident
 type r_lev = rlevel
 
@@ -399,4 +399,4 @@ type ltac_trace = ltac_call_kind Loc.located list
 
 type tacdef_body =
   | TacticDefinition of lident * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
-  | TacticRedefinition of reference * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
+  | TacticRedefinition of qualid * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index cef5bb1b8..481fc30df 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -92,88 +92,83 @@ let intern_or_var f ist = function
 let intern_int_or_var = intern_or_var (fun (n : int) -> n)
 let intern_string_or_var = intern_or_var (fun (s : string) -> s)
 
-let intern_global_reference ist = function
-  | {CAst.loc;v=Ident id} when find_var id ist ->
-    ArgVar (make ?loc id)
-  | r ->
-    let {CAst.loc} as lqid = qualid_of_reference r in
-    try ArgArg (loc,locate_global_with_alias lqid)
-    with Not_found -> error_global_not_found lqid
-
-let intern_ltac_variable ist = function
-  | {loc;v=Ident id} ->
-      if find_var id ist then
-	(* A local variable of any type *)
-        ArgVar (make ?loc id)
-      else raise Not_found
-  | _ ->
-      raise Not_found
-
-let intern_constr_reference strict ist = function
-  | {v=Ident id} as r when not strict && find_hyp id ist ->
-      (DAst.make @@ GVar id), Some (make @@ CRef (r,None))
-  | {v=Ident id} as r when find_var id ist ->
-      (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (r,None))
-  | r ->
-      let {loc} as lqid = qualid_of_reference r in
-      DAst.make @@ GRef (locate_global_with_alias lqid,None), 
-        if strict then None else Some (make @@ CRef (r,None))
+let intern_global_reference ist qid =
+  if qualid_is_ident qid && find_var (qualid_basename qid) ist then
+    ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
+  else
+    try ArgArg (qid.CAst.loc,locate_global_with_alias qid)
+    with Not_found -> error_global_not_found qid
+
+let intern_ltac_variable ist qid =
+  if qualid_is_ident qid && find_var (qualid_basename qid) ist then
+    (* A local variable of any type *)
+    ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
+  else raise Not_found
+
+let intern_constr_reference strict ist qid =
+  let id = qualid_basename qid in
+  if qualid_is_ident qid && not strict && find_hyp (qualid_basename qid) ist then
+    (DAst.make @@ GVar id), Some (make @@ CRef (qid,None))
+  else if qualid_is_ident qid && find_var (qualid_basename qid) ist then
+    (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (qid,None))
+  else
+    DAst.make @@ GRef (locate_global_with_alias qid,None),
+    if strict then None else Some (make @@ CRef (qid,None))
 
 (* Internalize an isolated reference in position of tactic *)
 
-let intern_isolated_global_tactic_reference r =
-  let {loc;v=qid} = qualid_of_reference r in
+let intern_isolated_global_tactic_reference qid =
+  let loc = qid.CAst.loc in
   TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[]))
 
-let intern_isolated_tactic_reference strict ist r =
+let intern_isolated_tactic_reference strict ist qid =
   (* An ltac reference *)
-  try Reference (intern_ltac_variable ist r)
+  try Reference (intern_ltac_variable ist qid)
   with Not_found ->
   (* A global tactic *)
-  try intern_isolated_global_tactic_reference r
+  try intern_isolated_global_tactic_reference qid
   with Not_found ->
   (* Tolerance for compatibility, allow not to use "constr:" *)
-  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
+  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid))
   with Not_found ->
   (* Reference not found *)
-  error_global_not_found (qualid_of_reference r)
+  error_global_not_found qid
 
 (* Internalize an applied tactic reference *)
 
-let intern_applied_global_tactic_reference r =
-  let {loc;v=qid} = qualid_of_reference r in
-  ArgArg (loc,Tacenv.locate_tactic qid)
+let intern_applied_global_tactic_reference qid =
+  ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid)
 
-let intern_applied_tactic_reference ist r =
+let intern_applied_tactic_reference ist qid =
   (* An ltac reference *)
-  try intern_ltac_variable ist r
+  try intern_ltac_variable ist qid
   with Not_found ->
   (* A global tactic *)
-  try intern_applied_global_tactic_reference r
+  try intern_applied_global_tactic_reference qid
   with Not_found ->
   (* Reference not found *)
-  error_global_not_found (qualid_of_reference r)
+  error_global_not_found qid
 
 (* Intern a reference parsed in a non-tactic entry *)
 
-let intern_non_tactic_reference strict ist r =
+let intern_non_tactic_reference strict ist qid =
   (* An ltac reference *)
-  try Reference (intern_ltac_variable ist r)
+  try Reference (intern_ltac_variable ist qid)
   with Not_found ->
   (* A constr reference *)
-  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
+  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid))
   with Not_found ->
   (* Tolerance for compatibility, allow not to use "ltac:" *)
-  try intern_isolated_global_tactic_reference r
+  try intern_isolated_global_tactic_reference qid
   with Not_found ->
   (* By convention, use IntroIdentifier for unbound ident, when not in a def *)
-  match r with
-  | {loc;v=Ident id} when not strict ->
-    let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in
+  if qualid_is_ident qid && not strict then
+    let id = qualid_basename qid in
+    let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc:qid.CAst.loc @@ IntroNaming (IntroIdentifier id)) in
     TacGeneric ipat
-  | _ ->
-  (* Reference not found *)
-  error_global_not_found (qualid_of_reference r)
+  else
+    (* Reference not found *)
+    error_global_not_found qid
 
 let intern_message_token ist = function
   | (MsgString _ | MsgInt _ as x) -> x
@@ -269,7 +264,7 @@ let intern_destruction_arg ist = function
   | clear,ElimOnIdent {loc;v=id} ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
-        let c, p = intern_constr ist (make @@ CRef (make @@ Ident id, None)) in
+        let c, p = intern_constr ist (make @@ CRef (qualid_of_ident id, None)) in
 	match DAst.get c with
         | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id)
 	| _ -> clear,ElimOnConstr ((c, p), NoBindings)
@@ -277,16 +272,15 @@ let intern_destruction_arg ist = function
         clear,ElimOnIdent (make ?loc id)
 
 let short_name = function
-  | {v=AN {loc;v=Ident id}} when not !strict_check -> Some (make ?loc id)
+  | {v=AN qid} when qualid_is_ident qid && not !strict_check ->
+    Some (make ?loc:qid.CAst.loc @@ qualid_basename qid)
   | _ -> None
 
-let intern_evaluable_global_reference ist r =
-  let lqid = qualid_of_reference r in
-  try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true lqid)
+let intern_evaluable_global_reference ist qid =
+  try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid)
   with Not_found ->
-  match r with
-  | {loc;v=Ident id} when not !strict_check -> EvalVarRef id
-  | _ -> error_global_not_found lqid
+  if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid)
+  else error_global_not_found qid
 
 let intern_evaluable_reference_or_by_notation ist = function
   | {v=AN r} -> intern_evaluable_global_reference ist r
@@ -296,14 +290,19 @@ let intern_evaluable_reference_or_by_notation ist = function
         (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
 
 (* Globalize a reduction expression *)
-let intern_evaluable ist = function
-  | {loc;v=AN {v=Ident id}} when find_var id ist -> ArgVar (make ?loc id)
-  | {loc;v=AN {v=Ident id}} when not !strict_check && find_hyp id ist ->
-      ArgArg (EvalVarRef id, Some (make ?loc id))
-  | r ->
-      let e = intern_evaluable_reference_or_by_notation ist r in
-      let na = short_name r in
-      ArgArg (e,na)
+let intern_evaluable ist r =
+  let f ist r =
+    let e = intern_evaluable_reference_or_by_notation ist r in
+    let na = short_name r in
+    ArgArg (e,na)
+  in
+  match r with
+  | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist ->
+    ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
+  | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist ->
+    let id = qualid_basename qid in
+      ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id))
+  | _ -> f ist r
 
 let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
 
@@ -356,7 +355,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
          subterm matched when a pattern *)
       let r = match r with
       | {v=AN r} -> r
-      | {loc} -> make ?loc @@ Qualid (qualid_of_path (path_of_global (smart_global r))) in
+      | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in
       let sign = {
         Constrintern.ltac_vars = ist.ltacvars;
         ltac_bound = Id.Set.empty;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 04dd7d6e9..9d1cc1643 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -361,7 +361,7 @@ let interp_reference ist env sigma = function
     with Not_found ->
       try
         VarRef (get_id (Environ.lookup_named id env))
-      with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id)
+      with Not_found -> error_global_not_found (qualid_of_ident ?loc id)
 
 let try_interp_evaluable env (loc, id) =
   let v = Environ.lookup_named id env in
@@ -377,14 +377,14 @@ let interp_evaluable ist env sigma = function
       with Not_found ->
         match r with
         | EvalConstRef _ -> r
-        | _ -> error_global_not_found (make ?loc @@ qualid_of_ident id)
+        | _ -> error_global_not_found (qualid_of_ident ?loc id)
     end
   | ArgArg (r,None) -> r
   | ArgVar {loc;v=id} ->
     try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id)
     with Not_found ->
       try try_interp_evaluable env (loc, id)
-      with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id)
+      with Not_found -> error_global_not_found (qualid_of_ident ?loc id)
 
 (* Interprets an hypothesis name *)
 let interp_occurrences ist occs =
@@ -643,7 +643,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
         Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
     (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id)
      with Not_found ->
-       error_global_not_found (make ?loc @@ qualid_of_ident id))
+       error_global_not_found (qualid_of_ident ?loc id))
   | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
   | Inr c -> Inr (interp_typed_pattern ist env sigma c) in
   interp_occurrences ist occs, p
@@ -925,7 +925,7 @@ let interp_destruction_arg ist gl arg =
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (make ?loc id)
 	else
-          let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (make ?loc @@ Ident id,None))) in
+          let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (qualid_of_ident ?loc id,None))) in
           let f env sigma =
             let (sigma,c) = interp_open_constr ist env sigma c in
             (sigma, (c,NoBindings))
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 5e4c9214a..e9ce306e8 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -42,11 +42,11 @@ let pr_ring_mod = function
   | Ring_kind Abstract ->  str "abstract"
   | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph
   | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]"
-  | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]"
+  | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
   | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]"
   | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]"
   | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext
-  | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]"
+  | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]"
   | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]"
   | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t
   | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t
diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml
index 3eb68b518..a83c79d11 100644
--- a/plugins/setoid_ring/newring_ast.ml
+++ b/plugins/setoid_ring/newring_ast.ml
@@ -22,7 +22,7 @@ type 'constr coeff_spec =
 
 type cst_tac_spec =
     CstTac of raw_tactic_expr
-  | Closed of reference list
+  | Closed of qualid list
 
 type 'constr ring_mod =
     Ring_kind of 'constr coeff_spec
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
index 3eb68b518..a83c79d11 100644
--- a/plugins/setoid_ring/newring_ast.mli
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -22,7 +22,7 @@ type 'constr coeff_spec =
 
 type cst_tac_spec =
     CstTac of raw_tactic_expr
-  | Closed of reference list
+  | Closed of qualid list
 
 type 'constr ring_mod =
     Ring_kind of 'constr coeff_spec
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
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 69d944fa1..c20e415b4 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -131,9 +131,12 @@ let add_genarg tag pr =
 (** Constructors for cast type *)
 let dC t = CastConv t
 (** Constructors for constr_expr *)
-let isCVar   = function { CAst.v = CRef ({CAst.v=Ident _},_) } -> true | _ -> false
-let destCVar = function { CAst.v = CRef ({CAst.v=Ident id},_) } -> id | _ ->
-  CErrors.anomaly (str"not a CRef.")
+let isCVar   = function { CAst.v = CRef (qid,_) } -> qualid_is_ident qid | _ -> false
+let destCVar = function
+  | { CAst.v = CRef (qid,_) } when qualid_is_ident qid ->
+    qualid_basename qid
+  | _ ->
+    CErrors.anomaly (str"not a CRef.")
 let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false
 let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c)
   | _ -> CErrors.anomaly (str "not a GLambda")
@@ -1019,8 +1022,10 @@ type pattern = Evd.evar_map * (constr, constr) ssrpattern
 let id_of_cpattern (_, (c1, c2), _) =
   let open CAst in
   match DAst.get c1, c2 with
-  | _, Some { v = CRef ({CAst.v=Ident x}, _) } -> Some x
-  | _, Some { v = CAppExpl ((_, {CAst.v=Ident x}, _), []) } -> Some x
+  | _, Some { v = CRef (qid, _) } when qualid_is_ident qid ->
+    Some (qualid_basename qid)
+  | _, Some { v = CAppExpl ((_, qid, _), []) } when qualid_is_ident qid ->
+    Some (qualid_basename qid)
   | GRef (VarRef x, _), None -> Some x
   | _ -> None
 let id_of_Cterm t = match id_of_cpattern t with