Merge PR #7797: Remove reference name type.

94 files changed, 656 insertions, 691 deletions

diff --git a/dev/base_include b/dev/base_include
index 574bc097e..6f54ecb24 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -229,7 +229,7 @@ let pf_e gl s =
 let _ = Flags.in_debugger := false
 let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
-  (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
+  (fun ?loc _ r -> Nametab.shortest_qualid_of_global ?loc Id.Set.empty r);;
 
 let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc))
 
diff --git a/dev/ci/user-overlays/07797-rm-reference.sh b/dev/ci/user-overlays/07797-rm-reference.sh
new file mode 100644
index 000000000..f7811cd6f
--- /dev/null
+++ b/dev/ci/user-overlays/07797-rm-reference.sh
@@ -0,0 +1,20 @@
+_OVERLAY_BRANCH=rm-reference
+
+if [ "$CI_PULL_REQUEST" = "7797" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then
+
+    Equations_CI_BRANCH="$_OVERLAY_BRANCH"
+    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations.git
+
+    ltac2_CI_BRANCH="fix-7797"
+    ltac2_CI_GITURL=https://github.com/ppedrot/Ltac2.git
+
+    quickchick_CI_BRANCH="$_OVERLAY_BRANCH"
+    quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick.git
+
+    coq_dpdgraph_CI_BRANCH="$_OVERLAY_BRANCH"
+    coq_dpdgraph_CI_GITURL=https://github.com/maximedenes/coq-dpdgraph.git
+
+    Elpi_CI_BRANCH="$_OVERLAY_BRANCH"
+    Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi.git
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index bb8189efc..f3fc126f9 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,14 @@
 
 ### ML API
 
+Names
+
+- In `Libnames`, the type `reference` and its two constructors `Qualid` and
+  `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity,
+  `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be
+  replaced by a test using `qualid_is_ident`. Extracting the ident part of a
+  qualid can be done using `qualid_basename`.
+
 Misctypes
 
 - Syntax for universe sorts and kinds has been moved from `Misctypes`
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 10a7a4158..844ad9188 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -549,8 +549,8 @@ let encode_path ?loc prefix mpdir suffix id =
     | Some (mp,dir) ->
 	(DirPath.repr (dirpath_of_string (ModPath.to_string mp))@
 	DirPath.repr dir) in
-  CAst.make ?loc @@ Qualid (make_qualid
-    (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
+  make_qualid ?loc
+    (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id
 
 let raw_string_of_ref ?loc _ = function
   | ConstRef cst ->
@@ -569,9 +569,9 @@ let raw_string_of_ref ?loc _ = function
       encode_path ?loc "SECVAR" None [] id
 
 let short_string_of_ref ?loc _ = function
-  | VarRef id -> CAst.make ?loc @@ Ident id
-  | ConstRef cst -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (Constant.repr3 cst)))
-  | IndRef (kn,0) -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (MutInd.repr3 kn)))
+  | VarRef id -> qualid_of_ident ?loc id
+  | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (pi3 (Constant.repr3 cst)))
+  | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (pi3 (MutInd.repr3 kn)))
   | IndRef (kn,i) ->
       encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))]
         (Id.of_string ("_"^string_of_int i))
diff --git a/engine/termops.ml b/engine/termops.ml
index eacc36107..2db2e07bf 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -297,7 +297,7 @@ let has_no_evar sigma =
   with Exit -> false
 
 let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
-let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l
+let reference_of_level evd l = UState.qualid_of_level (Evd.evar_universe_context evd) l
 
 let pr_evar_universe_context ctx =
   let open UState in
diff --git a/engine/termops.mli b/engine/termops.mli
index 255494031..f9aa6ba63 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -282,7 +282,7 @@ val is_Prop : Evd.evar_map -> constr -> bool
 val is_Set : Evd.evar_map -> constr -> bool
 val is_Type : Evd.evar_map -> constr -> bool
 
-val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid
 
 (** Combinators on judgments *)
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 0e3ecdbf5..81ab3dd66 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -295,15 +295,15 @@ let constrain_variables diff ctx =
   in
   { ctx with uctx_local = (univs, local); uctx_univ_variables = vars }
   
-let reference_of_level uctx =
+let qualid_of_level uctx =
   let map, map_rev = uctx.uctx_names in 
     fun l ->
-      try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname)
+      try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)
       with Not_found | Option.IsNone ->
-        UnivNames.reference_of_level l
+        UnivNames.qualid_of_level l
 
 let pr_uctx_level uctx l =
-  Libnames.pr_reference (reference_of_level uctx l)
+  Libnames.pr_qualid (qualid_of_level uctx l)
 
 type ('a, 'b) gen_universe_decl = {
   univdecl_instance : 'a; (* Declared universes *)
diff --git a/engine/uState.mli b/engine/uState.mli
index e7e5b39e0..a59e61b89 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -171,6 +171,6 @@ val update_sigma_env : t -> Environ.env -> t
 (** {5 Pretty-printing} *)
 
 val pr_uctx_level : t -> Univ.Level.t -> Pp.t
-val reference_of_level : t -> Univ.Level.t -> Libnames.reference
+val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid
 
 val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6ffb4bcf0..a68840174 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -14,18 +14,19 @@ open Globnames
 open Nametab
 
 
-let reference_of_level l = CAst.make @@
+let qualid_of_level l =
   match Level.name l with
   | Some (d, n as na)  ->
-     let qid =
-       try Nametab.shortest_qualid_of_universe na
-       with Not_found ->
-         let name = Id.of_string_soft (string_of_int n) in
-         Libnames.make_qualid d name
-     in Libnames.Qualid qid
-  | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l))
-
-let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l)
+    begin
+    try Nametab.shortest_qualid_of_universe na
+    with Not_found ->
+      let name = Id.of_string_soft (string_of_int n) in
+      Libnames.make_qualid d name
+    end
+  | None ->
+    Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l)
+
+let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
 
 (** Global universe information outside the kernel, to handle
     polymorphic universe names in sections that have to be discharged. *)
diff --git a/engine/univNames.mli b/engine/univNames.mli
index c19aa19d5..837beac26 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -11,7 +11,7 @@
 open Univ
 
 val pr_with_global_universes : Level.t -> Pp.t
-val reference_of_level : Level.t -> Libnames.reference
+val qualid_of_level : Level.t -> Libnames.qualid
 
 (** Global universe information outside the kernel, to handle
     polymorphic universes in sections that have to be discharged. *)
diff --git a/engine/universes.ml b/engine/universes.ml
index 70601987c..ee9668433 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -17,7 +17,7 @@ type universe_binders = UnivNames.universe_binders
 type univ_name_list = UnivNames.univ_name_list
 
 let pr_with_global_universes = UnivNames.pr_with_global_universes
-let reference_of_level = UnivNames.reference_of_level
+let reference_of_level = UnivNames.qualid_of_level
 
 let add_global_universe = UnivNames.add_global_universe
 
diff --git a/engine/universes.mli b/engine/universes.mli
index 46ff33a47..29673de1e 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -22,8 +22,8 @@ open Univ
 
 val pr_with_global_universes : Level.t -> Pp.t
 [@@ocaml.deprecated "Use [UnivNames.pr_with_global_universes]"]
-val reference_of_level : Level.t -> Libnames.reference
-[@@ocaml.deprecated "Use [UnivNames.reference_of_level]"]
+val reference_of_level : Level.t -> Libnames.qualid
+[@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"]
 
 val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
 [@@ocaml.deprecated "Use [UnivNames.add_global_universe]"]
diff --git a/ide/idetop.ml b/ide/idetop.ml
index ba69c4185..7abbf239b 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -290,8 +290,7 @@ let pattern_of_string ?env s =
 
 let dirpath_of_string_list s =
   let path = String.concat "." s in
-  let m = Pcoq.parse_string Pcoq.Constr.global path in
-  let {CAst.v=qid} = Libnames.qualid_of_reference m in
+  let qid = Pcoq.parse_string Pcoq.Constr.global path in
   let id =
     try Nametab.full_name_module qid
     with Not_found ->
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index d725f5afa..521eeb8e9 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -61,17 +61,17 @@ type instance_expr = Glob_term.glob_level list
 
 type cases_pattern_expr_r =
   | CPatAlias of cases_pattern_expr * lname
-  | CPatCstr  of reference
+  | CPatCstr  of qualid
     * cases_pattern_expr list option * cases_pattern_expr list
   (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
-  | CPatAtom of reference option
+  | CPatAtom of qualid option
   | CPatOr   of cases_pattern_expr list
   | CPatNotation of notation * cases_pattern_notation_substitution
     * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
 				  (notation n applied with substitution l1)
 				  applied to arguments l2 *)
   | CPatPrim   of prim_token
-  | CPatRecord of (reference * cases_pattern_expr) list
+  | CPatRecord of (qualid * cases_pattern_expr) list
   | CPatDelimiters of string * cases_pattern_expr
   | CPatCast   of cases_pattern_expr * constr_expr
 and cases_pattern_expr = cases_pattern_expr_r CAst.t
@@ -81,16 +81,16 @@ and cases_pattern_notation_substitution =
     cases_pattern_expr list list  (** for recursive notations *)
 
 and constr_expr_r =
-  | CRef     of reference * instance_expr option
+  | CRef     of qualid * instance_expr option
   | CFix     of lident * fix_expr list
   | CCoFix   of lident * cofix_expr list
   | CProdN   of local_binder_expr list * constr_expr
   | CLambdaN of local_binder_expr list * constr_expr
   | CLetIn   of lname * constr_expr * constr_expr option * constr_expr
-  | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list
+  | CAppExpl of (proj_flag * qualid * instance_expr option) * constr_expr list
   | CApp     of (proj_flag * constr_expr) *
                 (constr_expr * explicitation CAst.t option) list
-  | CRecord  of (reference * constr_expr) list
+  | CRecord  of (qualid * constr_expr) list
 
   (* representation of the "let" and "match" constructs *)
   | CCases of Constr.case_style   (* determines whether this value represents "let" or "match" construct *)
@@ -111,7 +111,7 @@ and constr_expr_r =
   | CGeneralization of binding_kind * abstraction_kind option * constr_expr
   | CPrim of prim_token
   | CDelimiters of string * constr_expr
-  | CProj of reference * constr_expr
+  | CProj of qualid * constr_expr
 and constr_expr = constr_expr_r CAst.t
 
 and case_expr = constr_expr                 (* expression that is being matched *)
@@ -150,7 +150,7 @@ type constr_pattern_expr = constr_expr
 (** Concrete syntax for modules and module types *)
 
 type with_declaration_ast =
-  | CWith_Module of Id.t list CAst.t * qualid CAst.t
+  | CWith_Module of Id.t list CAst.t * qualid
   | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr
 
 type module_ast_r =
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index d626630ef..4b1af9147 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -10,7 +10,6 @@
 
 open Pp
 open Util
-open CAst
 open Names
 open Nameops
 open Libnames
@@ -73,11 +72,11 @@ let rec cases_pattern_expr_eq p1 p2 =
   | CPatAlias(a1,i1), CPatAlias(a2,i2) ->
       eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2
   | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
-      eq_reference c1 c2 &&
+      qualid_eq c1 c2 &&
       Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
       List.equal cases_pattern_expr_eq b1 b2
   | CPatAtom(r1), CPatAtom(r2) ->
-    Option.equal eq_reference r1 r2
+    Option.equal qualid_eq r1 r2
   | CPatOr a1, CPatOr a2 ->
     List.equal cases_pattern_expr_eq a1 a2
   | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) ->
@@ -88,7 +87,7 @@ let rec cases_pattern_expr_eq p1 p2 =
     prim_token_eq i1 i2
   | CPatRecord l1, CPatRecord l2 ->
     let equal (r1, e1) (r2, e2) =
-      eq_reference r1 r2 && cases_pattern_expr_eq e1 e2
+      qualid_eq r1 r2 && cases_pattern_expr_eq e1 e2
     in
     List.equal equal l1 l2
   | CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) ->
@@ -108,7 +107,7 @@ let eq_universes u1 u2 =
 let rec constr_expr_eq e1 e2 =
   if CAst.(e1.v == e2.v) then true
   else match CAst.(e1.v, e2.v) with
-    | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2
+    | CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && eq_universes u1 u2
     | CFix(id1,fl1), CFix(id2,fl2) ->
       eq_ast Id.equal id1 id2 &&
       List.equal fix_expr_eq fl1 fl2
@@ -128,7 +127,7 @@ let rec constr_expr_eq e1 e2 =
       constr_expr_eq b1 b2
     | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) ->
       Option.equal Int.equal proj1 proj2 &&
-      eq_reference r1 r2 &&
+      qualid_eq r1 r2 &&
       List.equal constr_expr_eq al1 al2
     | CApp((proj1,e1),al1), CApp((proj2,e2),al2) ->
       Option.equal Int.equal proj1 proj2 &&
@@ -136,7 +135,7 @@ let rec constr_expr_eq e1 e2 =
       List.equal args_eq al1 al2
     | CRecord l1, CRecord l2 ->
       let field_eq (r1, e1) (r2, e2) =
-        eq_reference r1 r2 && constr_expr_eq e1 e2
+        qualid_eq r1 r2 && constr_expr_eq e1 e2
       in
       List.equal field_eq l1 l2
     | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) ->
@@ -178,7 +177,7 @@ let rec constr_expr_eq e1 e2 =
       String.equal s1 s2 &&
       constr_expr_eq e1 e2
     | CProj(p1,c1), CProj(p2,c2) ->
-      eq_reference p1 p2 && constr_expr_eq c1 c2
+      qualid_eq p1 p2 && constr_expr_eq c1 c2
   | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
      | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
      | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
@@ -280,7 +279,9 @@ let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
     List.fold_left (cases_pattern_fold_names f)
       (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
   | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat
-  | CPatAtom (Some {v=Ident id}) when not (is_constructor id) -> f id a
+  | CPatAtom (Some qid)
+      when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) ->
+      f (qualid_basename qid) a
   | CPatPrim _ | CPatAtom _ -> a
   | CPatCast ({CAst.loc},_) ->
     CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names"
@@ -363,7 +364,9 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
 
 let free_vars_of_constr_expr c =
   let rec aux bdvars l = function
-    | { CAst.v = CRef ({v=Ident id},_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l
+    | { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
+      let id = qualid_basename qid in
+      if Id.List.mem id bdvars then l else Id.Set.add id l
     | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
   in aux [] Id.Set.empty c
 
@@ -440,11 +443,13 @@ let map_constr_expr_with_binders g f e = CAst.map (function
   )
 
 (* Used in constrintern *)
-let rec replace_vars_constr_expr l = function
-  | { CAst.loc; v = CRef ({v=Ident id},us) } as x ->
-    (try CAst.make ?loc @@ CRef (make ?loc @@ Ident (Id.Map.find id l),us) with Not_found -> x)
-  | c -> map_constr_expr_with_binders Id.Map.remove
-           replace_vars_constr_expr l c
+let rec replace_vars_constr_expr l r =
+  match r with
+  | { CAst.loc; v = CRef (qid,us) } as x when qualid_is_ident qid ->
+    let id = qualid_basename qid in
+    (try CAst.make ?loc @@ CRef (qualid_of_ident ?loc (Id.Map.find id l),us)
+     with Not_found -> x)
+  | cn -> map_constr_expr_with_binders Id.Map.remove replace_vars_constr_expr l cn
 
 (* Returns the ranges of locs of the notation that are not occupied by args  *)
 (* and which are then occupied by proper symbols of the notation (or spaces) *)
@@ -513,7 +518,7 @@ let split_at_annot bl na =
 
 (** Pseudo-constructors *)
 
-let mkIdentC id   = CAst.make @@ CRef (make @@ Ident id,None)
+let mkIdentC id   = CAst.make @@ CRef (qualid_of_ident id,None)
 let mkRefC r      = CAst.make @@ CRef (r,None)
 let mkCastC (a,k) = CAst.make @@ CCast (a,k)
 let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b)
@@ -532,20 +537,22 @@ let mkCProdN ?loc bll c =
 let mkCLambdaN ?loc bll c =
   CAst.make ?loc @@ CLambdaN (bll,c)
 
-let coerce_reference_to_id = CAst.with_loc_val (fun ?loc -> function
-  | Ident id -> id
-  | Qualid _ ->
-    CErrors.user_err ?loc ~hdr:"coerce_reference_to_id"
-      (str "This expression should be a simple identifier."))
+let coerce_reference_to_id qid =
+  if qualid_is_ident qid then qualid_basename qid
+  else
+    CErrors.user_err ?loc:qid.CAst.loc ~hdr:"coerce_reference_to_id"
+      (str "This expression should be a simple identifier.")
 
 let coerce_to_id = function
-  | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc id
+  | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid ->
+    CAst.make ?loc @@ qualid_basename qid
   | { CAst.loc; _ } -> CErrors.user_err ?loc
                          ~hdr:"coerce_to_id"
                          (str "This expression should be a simple identifier.")
 
 let coerce_to_name = function
-  | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc @@ Name id
+  | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid ->
+    CAst.make ?loc @@ Name (qualid_basename qid)
   | { CAst.loc; v = CHole (None,IntroAnonymous,None) } -> CAst.make ?loc Anonymous
   | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
                          (str "This expression should be a name.")
@@ -572,7 +579,8 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
      CPatAtom (Some r)
   | CHole (None,IntroAnonymous,None) ->
      CPatAtom None
-  | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef ({v=Ident id'},None) }) when Id.equal id id' ->
+  | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (qid,None) })
+      when qualid_is_ident qid && Id.equal id (qualid_basename qid) ->
       CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id))
   | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args ->
      (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 1c2348457..46aef1c78 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -41,7 +41,7 @@ val local_binders_loc : local_binder_expr list -> Loc.t option
 (** {6 Constructors}*)
 
 val mkIdentC : Id.t -> constr_expr
-val mkRefC : reference -> constr_expr
+val mkRefC : qualid -> constr_expr
 val mkAppC : constr_expr * constr_expr list -> constr_expr
 val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr
 val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
@@ -61,7 +61,7 @@ val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -
 
 (** {6 Destructors}*)
 
-val coerce_reference_to_id : reference -> Id.t
+val coerce_reference_to_id : qualid -> Id.t
 (** FIXME: nothing to do here *)
 
 val coerce_to_id : constr_expr -> lident
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c613effcd..2538c7772 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -270,7 +270,7 @@ let extern_evar n l = CEvar (n,l)
     may be inaccurate *)
 
 let default_extern_reference ?loc vars r =
-  make @@ Qualid (shortest_qualid_of_global vars r)
+  shortest_qualid_of_global ?loc vars r
 
 let my_extern_reference = ref default_extern_reference
 
@@ -388,7 +388,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
         (uninterp_cases_pattern_notations pat)
     with No_match ->
       lift (fun ?loc -> function
-        | PatVar (Name id) -> CPatAtom (Some (make ?loc @@ Ident id))
+        | PatVar (Name id) -> CPatAtom (Some (qualid_of_ident ?loc id))
 	| PatVar (Anonymous) -> CPatAtom None
 	| PatCstr(cstrsp,args,na) ->
 	  let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
@@ -457,7 +457,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
 	      (make_pat_notation ?loc ntn (l,ll) l2') key
       end
     | SynDefRule kn ->
-      let qid = make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn) in
+      let qid = shortest_qualid_of_syndef ?loc vars kn in
       let l1 =
 	List.rev_map (fun (c,(scopt,scl)) ->
           extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
@@ -484,7 +484,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
 	    (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
 	  insert_pat_alias ?loc p na
 	| PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
-        | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (make ?loc @@ Ident id))
+        | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id))
     with
 	No_match -> extern_notation_pattern allscopes vars t rules
 
@@ -753,7 +753,7 @@ let rec extern inctx scopes vars r =
       extern_global (select_stronger_impargs (implicits_of_global ref))
         (extern_reference vars ref) (extern_universes us)
 
-  | GVar id -> CRef (make ?loc @@ Ident id,None)
+  | GVar id -> CRef (qualid_of_ident ?loc id,None)
 
   | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None)
 
@@ -1095,7 +1095,7 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
 		List.map (fun (c,(scopt,scl)) ->
 		  extern true (scopt,scl@scopes) vars c, None)
 		  terms in
-              let a = CRef (make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn),None) in
+              let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in
 	      CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in
  	if List.is_empty args then e
 	else
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 73c108319..f09b316cd 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -38,7 +38,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
 
 val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference
+val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
@@ -56,9 +56,9 @@ val print_projections : bool ref
 
 (** Customization of the global_reference printer *)
 val set_extern_reference :
-  (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) -> unit
+  (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid) -> unit
 val get_extern_reference :
-  unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference)
+  unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid)
 
 (** WARNING: The following functions are evil due to
     side-effects. Think of the following case as used in the printer:
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 47ae64d47..4e217b2cd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -96,8 +96,8 @@ let is_global id =
   with Not_found ->
     false
 
-let global_reference_of_reference ref =
-  locate_reference (qualid_of_reference ref).CAst.v
+let global_reference_of_reference qid =
+  locate_reference qid
 
 let global_reference id =
   locate_reference (qualid_of_ident id)
@@ -117,7 +117,7 @@ let global_reference_in_absolute_module dir id =
 type internalization_error =
   | VariableCapture of Id.t * Id.t
   | IllegalMetavariable
-  | NotAConstructor of reference
+  | NotAConstructor of qualid
   | UnboundFixName of bool * Id.t
   | NonLinearPattern of Id.t
   | BadPatternsNumber of int * int
@@ -131,8 +131,8 @@ let explain_variable_capture id id' =
 let explain_illegal_metavariable =
   str "Metavariables allowed only in patterns"
 
-let explain_not_a_constructor ref =
-  str "Unknown constructor: " ++ pr_reference ref
+let explain_not_a_constructor qid =
+  str "Unknown constructor: " ++ pr_qualid qid
 
 let explain_unbound_fix_name is_cofix id =
   str "The name" ++ spc () ++ Id.print id ++
@@ -404,7 +404,8 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
 	  let name =
 	    let id =
 	      match ty with
-              | { v = CApp ((_, { v = CRef ({v=Ident id},_) } ), _) } -> id
+              | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
+                qualid_basename qid
 	      | _ -> default_non_dependent_ident
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
@@ -556,7 +557,8 @@ let is_var store pat =
 
 let out_var pat =
   match pat.v with
-  | CPatAtom (Some ({v=Ident id})) -> Name id
+  | CPatAtom (Some qid) when qualid_is_ident qid ->
+    Name (qualid_basename qid)
   | CPatAtom None -> Anonymous
   | _ -> assert false
 
@@ -622,18 +624,18 @@ let error_cannot_coerce_disjunctive_pattern_term ?loc () =
 
 let terms_of_binders bl =
   let rec term_of_pat pt = dmap_with_loc (fun ?loc -> function
-    | PatVar (Name id)   -> CRef (make @@ Ident id, None)
+    | PatVar (Name id)   -> CRef (qualid_of_ident id, None)
     | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc ()
     | PatCstr (c,l,_) ->
-       let r = make ?loc @@ Qualid (qualid_of_path (path_of_global (ConstructRef c))) in
+       let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in
        let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
-       CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
+       CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables l = match l with
     | bnd :: l ->
       let loc = bnd.loc in
       begin match DAst.get bnd with
-      | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (make ?loc @@ Ident id, None)) :: extract_variables l
+      | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)) :: extract_variables l
       | GLocalDef (Name id,_,_,_) -> extract_variables l
       | GLocalDef (Anonymous,_,_,_)
       | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.")
@@ -806,7 +808,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
    distinction *)
 
 let cases_pattern_of_name {loc;v=na} =
-  let atom = match na with Name id -> Some (make ?loc @@ Ident id) | Anonymous -> None in
+  let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in
   CAst.make ?loc (CPatAtom atom)
 
 let split_by_type ids subst =
@@ -903,7 +905,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
   try
     let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in
     let expl_impls = List.map
-      (fun id -> CAst.make ?loc @@ CRef (make ?loc @@ Ident id,None), Some (make ?loc @@ ExplByName id)) expl_impls in
+      (fun id -> CAst.make ?loc @@ CRef (qualid_of_ident ?loc id,None), Some (make ?loc @@ ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
     Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys;
     gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
@@ -970,18 +972,17 @@ let dump_extended_global loc = function
   | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref
   | SynDef sp -> Dumpglob.add_glob_kn ?loc sp
 
-let intern_extended_global_of_qualid {loc;v=qid} =
-  let r = Nametab.locate_extended qid in dump_extended_global loc r; r
+let intern_extended_global_of_qualid qid =
+  let r = Nametab.locate_extended qid in dump_extended_global qid.CAst.loc r; r
 
-let intern_reference ref =
-  let qid = qualid_of_reference ref in
+let intern_reference qid =
   let r =
     try intern_extended_global_of_qualid qid
     with Not_found -> error_global_not_found qid
   in
   Smartlocate.global_of_extended_global r
 
-let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option =
+let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option =
   match info with
   | UAnonymous -> None
   | UUnknown -> None
@@ -1014,7 +1015,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
       let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
       let loc = c.loc in
       let err () =
-        user_err ?loc  (str "Notation " ++ pr_qualid qid.v
+        user_err ?loc  (str "Notation " ++ pr_qualid qid
                   ++ str " cannot have a universe instance,"
                   ++ str " its expanded head does not start with a reference")
       in
@@ -1031,34 +1032,32 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
       | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
       | Some [_old_level], GSort _new_sort ->
         (* TODO: add old_level and new_sort to the error message *)
-        user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v)
+        user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid)
       | Some _, _ -> err ()
       in
       c, projapp, args2
 
-let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
-function
-  | {loc; v=Qualid qid} ->
-      let qid = make ?loc qid in
-      let r,projapp,args2 =
-        try intern_qualid qid intern env ntnvars us args
-        with Not_found -> error_global_not_found qid
-      in
-      let x, imp, scopes, l = find_appl_head_data r in
-	(x,imp,scopes,l), args2
-  | {loc; v=Ident id} ->
-      try intern_var env lvar namedctx loc id us, args
+let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qid =
+  let loc = qid.CAst.loc in
+  if qualid_is_ident qid then
+      try intern_var env lvar namedctx loc (qualid_basename qid) us, args
       with Not_found ->
-      let qid = make ?loc @@ qualid_of_ident id in
       try
         let r, projapp, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
 	let x, imp, scopes, l = find_appl_head_data r in
 	  (x,imp,scopes,l), args2
       with Not_found ->
-	(* Extra allowance for non globalizing functions *)
-	if !interning_grammar || env.unb then
-	  (gvar (loc,id) us, [], [], []), args
+        (* Extra allowance for non globalizing functions *)
+        if !interning_grammar || env.unb then
+          (gvar (loc,qualid_basename qid) us, [], [], []), args
         else error_global_not_found qid
+  else
+    let r,projapp,args2 =
+      try intern_qualid qid intern env ntnvars us args
+      with Not_found -> error_global_not_found qid
+    in
+    let x, imp, scopes, l = find_appl_head_data r in
+    (x,imp,scopes,l), args2
 
 let interp_reference vars r =
   let (r,_,_,_),_ =
@@ -1262,18 +1261,18 @@ let find_constructor loc add_params ref =
       List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)])
     | None -> []
 
-let find_pattern_variable = function
-  | {v=Ident id} -> id
-  | {loc;v=Qualid _} as x -> raise (InternalizationError(loc,NotAConstructor x))
+let find_pattern_variable qid =
+  if qualid_is_ident qid then qualid_basename qid
+  else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid))
 
 let check_duplicate loc fields =
-  let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in
+  let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in
   let dups = List.duplicates eq fields in
   match dups with
   | [] -> ()
   | (r, _) :: _ ->
     user_err ?loc (str "This record defines several times the field " ++
-      pr_reference r ++ str ".")
+      pr_qualid r ++ str ".")
 
 (** [sort_fields ~complete loc fields completer] expects a list
     [fields] of field assignments [f = e1; g = e2; ...], where [f, g]
@@ -1298,14 +1297,14 @@ let sort_fields ~complete loc fields completer =
             (gr, Recordops.find_projection gr)
           with Not_found ->
             user_err ?loc ~hdr:"intern"
-                         (pr_reference first_field_ref ++ str": Not a projection")
+                         (pr_qualid first_field_ref ++ str": Not a projection")
         in
         (* the number of parameters *)
         let nparams = record.Recordops.s_EXPECTEDPARAM in
         (* the reference constructor of the record *)
         let base_constructor =
           let global_record_id = ConstructRef record.Recordops.s_CONST in
-          try make ?loc @@ Qualid (shortest_qualid_of_global Id.Set.empty global_record_id)
+          try shortest_qualid_of_global ?loc Id.Set.empty global_record_id
           with Not_found ->
             anomaly (str "Environment corruption for records.") in
         let () = check_duplicate loc fields in
@@ -1356,7 +1355,7 @@ let sort_fields ~complete loc fields completer =
                let field_glob_ref = try global_reference_of_reference field_ref
                with Not_found ->
                  user_err ?loc ~hdr:"intern"
-                               (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
+                               (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in
                let remaining_projs, (field_index, _) =
                  let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in
                  try CList.extract_first the_proj remaining_projs
@@ -1483,10 +1482,9 @@ let drop_notations_pattern looked_for genv =
       end
     | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x
   in
-  let rec drop_syndef top scopes re pats =
-    let qid = qualid_of_reference re in
+  let rec drop_syndef top scopes qid pats =
     try
-      match locate_extended qid.v with
+      match locate_extended qid with
       | SynDef sp ->
 	let (vars,a) = Syntax_def.search_syntactic_definition sp in
 	(match a with
@@ -1542,10 +1540,10 @@ let drop_notations_pattern looked_for genv =
 	  | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
 	  | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
-     | CPatCstr (r, Some expl_pl, pl) ->
-      let g = try locate (qualid_of_reference r).v
+     | CPatCstr (qid, Some expl_pl, pl) ->
+      let g = try locate qid
 	      with Not_found ->
- 	      raise (InternalizationError (loc,NotAConstructor r)) in
+              raise (InternalizationError (loc,NotAConstructor qid)) in
       if expl_pl == [] then
         (* Convention: (@r) deactivates all further implicit arguments and scopes *)
         DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 12f77af30..dd0944cc4 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -141,10 +141,10 @@ val intern_constr_pattern :
     constr_pattern_expr -> patvar list * constr_pattern
 
 (** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
-val intern_reference : reference -> GlobRef.t
+val intern_reference : qualid -> GlobRef.t
 
 (** Expands abbreviations (syndef); raise an error if not existing *)
-val interp_reference : ltac_sign -> reference -> glob_constr
+val interp_reference : ltac_sign -> qualid -> glob_constr
 
 (** Interpret binders *)
 
diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml
index 42c1fe429..607f2258f 100644
--- a/interp/genredexpr.ml
+++ b/interp/genredexpr.ml
@@ -60,6 +60,6 @@ open Constrexpr
 
 type r_trm = constr_expr
 type r_pat = constr_pattern_expr
-type r_cst = reference or_by_notation
+type r_cst = qualid or_by_notation
 
 type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index b54e2badd..83ad9af33 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -96,9 +96,11 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
     else l
   in
   let rec aux bdvars l c = match CAst.(c.v) with
-    | CRef ({CAst.v=Ident id},_) -> found c.CAst.loc id bdvars l
-    | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef ({CAst.v=Ident id},_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) ->
-        Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c
+    | CRef (qid,_) when qualid_is_ident qid ->
+      found c.CAst.loc (qualid_basename qid) bdvars l
+    | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
+        qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
+        Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
     | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
   in aux bound l c
 
@@ -196,7 +198,7 @@ let combine_params avoid fn applied needed =
 let combine_params_freevar =
   fun avoid (_, decl) ->
     let id' = next_name_away_from (RelDecl.get_name decl) avoid in
-      (CAst.make @@ CRef (CAst.make @@ Ident id',None), Id.Set.add id' avoid)
+      (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
 
 let destClassApp cl =
   let open CAst in
@@ -218,9 +220,8 @@ let destClassAppExpl cl =
 let implicit_application env ?(allow_partial=true) f ty =
   let is_class =
     try
-      let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in
-      let qid = qualid_of_reference r in
-      let gr = Nametab.locate qid.CAst.v in
+      let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
+      let gr = Nametab.locate qid in
 	if Typeclasses.is_class gr then Some (clapp, gr) else None
     with Not_found -> None
   in
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 25394fc0d..a8492095e 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -16,8 +16,8 @@ open Libnames
 val declare_generalizable : local:bool -> lident list option -> unit
 
 val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t
-val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t
+val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t
+val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t
 
 (** Fragile, should be used only for construction a set of identifiers to avoid *)
 
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 33c07d551..c27cc9cc0 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -45,8 +45,9 @@ let error_application_to_module_type loc =
     or both are searched. The returned kind is never ModAny, and
     it is equal to the input kind when this one isn't ModAny. *)
 
-let lookup_module_or_modtype kind {CAst.loc;v=qid} =
+let lookup_module_or_modtype kind qid =
   let open Declaremods in
+  let loc = qid.CAst.loc in
   try
     if kind == ModType then raise Not_found;
     let mp = Nametab.locate_module qid in
@@ -84,7 +85,7 @@ let loc_of_module l = l.CAst.loc
 
 let rec interp_module_ast env kind m cst = match m with
   | {CAst.loc;v=CMident qid} ->
-      let (mp,kind) = lookup_module_or_modtype kind CAst.(make ?loc qid) in
+      let (mp,kind) = lookup_module_or_modtype kind qid in
       (MEident mp, kind, cst)
   | {CAst.loc;v=CMapply (me1,me2)} ->
       let me1',kind1, cst = interp_module_ast env kind me1 cst in
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index e1fbdba87..91491bdf8 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -41,26 +41,24 @@ let global_of_extended_global = function
   | [],NApp (NRef ref,[]) -> ref
   | _ -> raise Not_found
 
-let locate_global_with_alias ?(head=false) {CAst.loc; v=qid} =
+let locate_global_with_alias ?(head=false) qid =
   let ref = Nametab.locate_extended qid in
   try
     if head then global_of_extended_global_head ref
     else global_of_extended_global ref
   with Not_found ->
-    user_err ?loc (pr_qualid qid ++
+    user_err ?loc:qid.CAst.loc (pr_qualid qid ++
       str " is bound to a notation that does not denote a reference.")
 
-let global_inductive_with_alias ({CAst.loc} as lr)  =
-  let qid = qualid_of_reference lr in
+let global_inductive_with_alias qid  =
   try match locate_global_with_alias qid with
   | IndRef ind -> ind
   | ref ->
-      user_err ?loc ~hdr:"global_inductive"
-        (pr_reference lr ++ spc () ++ str "is not an inductive type.")
+      user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+        (pr_qualid qid ++ spc () ++ str "is not an inductive type.")
   with Not_found -> Nametab.error_global_not_found qid
 
-let global_with_alias ?head r =
-  let qid = qualid_of_reference r in
+let global_with_alias ?head qid =
   try locate_global_with_alias ?head qid
   with Not_found -> Nametab.error_global_not_found qid
 
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 6b574d7b5..e41ef7891 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -17,7 +17,7 @@ open Globnames
    if not bound in the global env; raise a [UserError] if bound to a
    syntactic def that does not denote a reference *)
 
-val locate_global_with_alias : ?head:bool -> qualid CAst.t -> GlobRef.t
+val locate_global_with_alias : ?head:bool -> qualid -> GlobRef.t
 
 (** Extract a global_reference from a reference that can be an "alias" *)
 val global_of_extended_global : extended_global_reference -> GlobRef.t
@@ -26,13 +26,13 @@ val global_of_extended_global : extended_global_reference -> GlobRef.t
     May raise [Nametab.GlobalizationError _] for an unknown reference,
     or a [UserError] if bound to a syntactic def that does not denote
     a reference. *)
-val global_with_alias : ?head:bool -> reference -> GlobRef.t
+val global_with_alias : ?head:bool -> qualid -> GlobRef.t
 
 (** The same for inductive types *)
-val global_inductive_with_alias : reference -> inductive
+val global_inductive_with_alias : qualid -> inductive
 
 (** Locate a reference taking into account notations and "aliases" *)
-val smart_global : ?head:bool -> reference Constrexpr.or_by_notation -> GlobRef.t
+val smart_global : ?head:bool -> qualid Constrexpr.or_by_notation -> GlobRef.t
 
 (** The same for inductive types *)
-val smart_global_inductive : reference Constrexpr.or_by_notation -> inductive
+val smart_global_inductive : qualid Constrexpr.or_by_notation -> inductive
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 4792cda08..5e5e43ed3 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -41,7 +41,7 @@ val wit_ident : Id.t uniform_genarg_type
 
 val wit_var : (lident, lident, Id.t) genarg_type
 
-val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
+val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
 
 val wit_sort_family : (Sorts.family, unit, unit) genarg_type
 
@@ -53,7 +53,7 @@ val wit_open_constr :
   (constr_expr, glob_constr_and_expr, constr) genarg_type
 
 val wit_red_expr :
-  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+  ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
 
@@ -63,10 +63,10 @@ val wit_clause_dft_concl :  (lident Locus.clause_expr, lident Locus.clause_expr,
 
 val wit_integer : int uniform_genarg_type
 val wit_preident : string uniform_genarg_type
-val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
-val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
+val wit_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
+val wit_global : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
 val wit_clause :  (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
 val wit_redexpr :
-  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+  ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/library/goptions.ml b/library/goptions.ml
index 76071ebcc..f14ad333e 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -161,7 +161,7 @@ module type RefConvertArg =
 sig
   type t
   val compare : t -> t -> int
-  val encode : reference -> t
+  val encode : qualid -> t
   val subst : substitution -> t -> t
   val printer : t -> Pp.t
   val key : option_name
@@ -172,7 +172,7 @@ end
 module RefConvert = functor (A : RefConvertArg) ->
 struct
   type t = A.t
-  type key = reference
+  type key = qualid
   let compare = A.compare
   let table = ref_table
   let encode = A.encode
diff --git a/library/goptions.mli b/library/goptions.mli
index 6c14d19ee..3d7df18fe 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -89,7 +89,7 @@ module MakeRefTable :
     (A : sig
            type t
            val compare : t -> t -> int
-           val encode : reference -> t
+           val encode : qualid -> t
 	   val subst : substitution -> t -> t
            val printer : t -> Pp.t
            val key : option_name
@@ -147,9 +147,9 @@ val get_string_table :
 
 val get_ref_table :
   option_name ->
-    < add : reference -> unit;
-      remove : reference -> unit;
-      mem : reference -> unit;
+    < add : qualid -> unit;
+      remove : qualid -> unit;
+      mem : qualid -> unit;
       print : unit >
 
 (** The first argument is a locality flag. *)
diff --git a/library/libnames.ml b/library/libnames.ml
index 8d5a02a29..23085048a 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -134,23 +134,33 @@ let restrict_path n sp =
   make_path (DirPath.make dir') s
 
 (*s qualified names *)
-type qualid = full_path
+type qualid_r = full_path
+type qualid = qualid_r CAst.t
 
-let make_qualid = make_path
-let repr_qualid = repr_path
+let make_qualid ?loc pa id = CAst.make ?loc (make_path pa id)
+let repr_qualid {CAst.v=qid} = repr_path qid
 
-let qualid_eq = eq_full_path
+let qualid_eq qid1 qid2 = eq_full_path qid1.CAst.v qid2.CAst.v
 
-let string_of_qualid = string_of_path
-let pr_qualid = pr_path
+let string_of_qualid qid = string_of_path qid.CAst.v
+let pr_qualid qid = pr_path qid.CAst.v
 
-let qualid_of_string = path_of_string
+let qualid_of_string ?loc s = CAst.make ?loc @@ path_of_string s
 
-let qualid_of_path sp = sp
-let qualid_of_ident id = make_qualid DirPath.empty id
-let qualid_of_dirpath dir =
+let qualid_of_path ?loc sp = CAst.make ?loc sp
+let qualid_of_ident ?loc id = make_qualid ?loc DirPath.empty id
+let qualid_of_dirpath ?loc dir =
   let (l,a) = split_dirpath dir in
-  make_qualid l a
+  make_qualid ?loc l a
+
+let qualid_is_ident qid =
+  DirPath.is_empty qid.CAst.v.dirpath
+
+let qualid_basename qid =
+  qid.CAst.v.basename
+
+let qualid_path qid =
+  qid.CAst.v.dirpath
 
 type object_name = full_path * KerName.t
 
@@ -183,52 +193,6 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with
 | DirModule op1, DirModule op2 -> eq_op op1 op2
 | _ -> false
 
-type reference_r =
-  | Qualid of qualid
-  | Ident of Id.t
-type reference = reference_r CAst.t
-
-let qualid_of_reference = CAst.map (function
-  | Qualid qid -> qid
-  | Ident id -> qualid_of_ident id)
-
-let string_of_reference = CAst.with_val (function
-  | Qualid qid -> string_of_qualid qid
-  | Ident id -> Id.to_string id)
-
-let pr_reference = CAst.with_val (function
-  | Qualid qid -> pr_qualid qid
-  | Ident id -> Id.print id)
-
-let eq_reference {CAst.v=r1} {CAst.v=r2} = match r1, r2 with
-| Qualid q1, Qualid q2 -> qualid_eq q1 q2
-| Ident id1, Ident id2 -> Id.equal id1 id2
-| _ -> false
-
-let join_reference {CAst.loc=l1;v=ns} {CAst.loc=l2;v=r} =
-  CAst.make ?loc:(Loc.merge_opt l1 l2) (
-  match ns , r with
-    Qualid q1, Qualid q2 ->
-      let (dp1,id1) = repr_qualid q1 in
-      let (dp2,id2) = repr_qualid q2 in
-      Qualid (make_qualid
-		(append_dirpath (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) dp2)
-		id2)
-  | Qualid q1, Ident id2 ->
-    let (dp1,id1) = repr_qualid q1 in
-    Qualid (make_qualid
-	      (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1)))
-	      id2)
-  | Ident id1, Qualid q2 ->
-    let (dp2,id2) = repr_qualid q2 in
-    Qualid (make_qualid
-      (append_dirpath (dirpath_of_string (Names.Id.to_string id1)) dp2)
-      id2)
-  | Ident id1, Ident id2 ->
-    Qualid (make_qualid
-      (dirpath_of_string (Names.Id.to_string id1)) id2)
-  )
-
 (* Default paths *)
 let default_library = Names.DirPath.initial (* = ["Top"] *)
 
diff --git a/library/libnames.mli b/library/libnames.mli
index 5f69b1f0f..447eecbb5 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -65,23 +65,28 @@ val restrict_path : int -> full_path -> full_path
     qualifications of absolute names, including single identifiers.
     The [qualid] are used to access the name table. *)
 
-type qualid
+type qualid_r
+type qualid = qualid_r CAst.t
 
-val make_qualid : DirPath.t -> Id.t -> qualid
+val make_qualid : ?loc:Loc.t -> DirPath.t -> Id.t -> qualid
 val repr_qualid : qualid -> DirPath.t * Id.t
 
 val qualid_eq : qualid -> qualid -> bool
 
 val pr_qualid : qualid -> Pp.t
 val string_of_qualid : qualid -> string
-val qualid_of_string : string -> qualid
+val qualid_of_string : ?loc:Loc.t -> string -> qualid
 
 (** Turns an absolute name, a dirpath, or an Id.t into a
    qualified name denoting the same name *)
 
-val qualid_of_path : full_path -> qualid
-val qualid_of_dirpath : DirPath.t -> qualid
-val qualid_of_ident : Id.t -> qualid
+val qualid_of_path : ?loc:Loc.t -> full_path -> qualid
+val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid
+val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid
+
+val qualid_is_ident : qualid -> bool
+val qualid_path : qualid -> DirPath.t
+val qualid_basename : qualid -> Id.t
 
 (** Both names are passed to objects: a "semantic" [kernel_name], which
    can be substituted and a "syntactic" [full_path] which can be printed
@@ -124,20 +129,6 @@ val eq_global_dir_reference :
   global_dir_reference -> global_dir_reference -> bool
 
 (** {6 ... } *)
-(** A [reference] is the user-level notion of name. It denotes either a
-    global name (referred either by a qualified name or by a single
-    name) or a variable *)
-
-type reference_r =
-  | Qualid of qualid
-  | Ident of Id.t
-type reference = reference_r CAst.t
-
-val eq_reference : reference -> reference -> bool
-val qualid_of_reference : reference -> qualid CAst.t
-val string_of_reference : reference -> string
-val pr_reference : reference -> Pp.t
-val join_reference : reference -> reference -> reference
 
 (** some preset paths *)
 val default_library : DirPath.t
diff --git a/library/library.ml b/library/library.ml
index 56d2709d5..400f3dcf1 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -577,10 +577,10 @@ let require_library_from_dirpath modrefl export =
 
 (* the function called by Vernacentries.vernac_import *)
 
-let safe_locate_module {CAst.loc;v=qid} =
+let safe_locate_module qid =
   try Nametab.locate_module qid
   with Not_found ->
-    user_err ?loc ~hdr:"import_library"
+    user_err ?loc:qid.CAst.loc ~hdr:"import_library"
       (pr_qualid qid ++ str " is not a module")
 
 let import_module export modl =
@@ -595,18 +595,18 @@ let import_module export modl =
     | [] -> ()
     | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
   let rec aux acc = function
-    | ({CAst.loc; v=dir} as m) :: l ->
+    | qid :: l ->
         let m,acc =
-          try Nametab.locate_module dir, acc
-          with Not_found-> flush acc; safe_locate_module m, [] in
+          try Nametab.locate_module qid, acc
+          with Not_found-> flush acc; safe_locate_module qid, [] in
         (match m with
         | MPfile dir -> aux (dir::acc) l
         | mp ->
             flush acc;
             try Declaremods.import_module export mp; aux [] l
             with Not_found ->
-              user_err ?loc ~hdr:"import_library"
-                (pr_qualid dir ++ str " is not a module"))
+              user_err ?loc:qid.CAst.loc ~hdr:"import_library"
+                (pr_qualid qid ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
 
diff --git a/library/library.mli b/library/library.mli
index 0877ebb5a..d5815afc4 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -36,7 +36,7 @@ type seg_proofs = Constr.constr Future.computation array
 
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
-val import_module : bool -> qualid CAst.t list -> unit
+val import_module : bool -> qualid list -> unit
 
 (** Start the compilation of a file as a library. The first argument must be
     output file, and the 
diff --git a/library/nametab.ml b/library/nametab.ml
index 995f44706..a3b3ca6e7 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -18,8 +18,8 @@ open Globnames
 
 exception GlobalizationError of qualid
 
-let error_global_not_found {CAst.loc;v} =
-  Loc.raise ?loc (GlobalizationError v)
+let error_global_not_found qid =
+  Loc.raise ?loc:qid.CAst.loc (GlobalizationError qid)
 
 (* The visibility can be registered either
    - for all suffixes not shorter then a given int - when the object
@@ -69,7 +69,7 @@ module type NAMETREE = sig
   val find : user_name -> t -> elt
   val exists : user_name -> t -> bool
   val user_name : qualid -> t -> user_name
-  val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
+  val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
 end
 
@@ -220,7 +220,7 @@ let exists uname tab =
   with
       Not_found -> false
 
-let shortest_qualid ctx uname tab =
+let shortest_qualid ?loc ctx uname tab =
   let id,dir = U.repr uname in
   let hidden = Id.Set.mem id ctx in
   let rec find_uname pos dir tree =
@@ -235,7 +235,7 @@ let shortest_qualid ctx uname tab =
   in
   let ptab = Id.Map.find id tab in
   let found_dir = find_uname [] dir ptab in
-    make_qualid (DirPath.make found_dir) id
+    make_qualid ?loc (DirPath.make found_dir) id
 
 let push_node node l =
   match node with
@@ -458,14 +458,13 @@ let global_of_path sp =
 
 let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab
 
-let global ({CAst.loc;v=r} as lr)=
-  let {CAst.loc; v} as qid = qualid_of_reference lr in
-  try match locate_extended v with
+let global qid =
+  try match locate_extended qid with
     | TrueGlobal ref -> ref
     | SynDef _ ->
-        user_err ?loc ~hdr:"global"
+        user_err ?loc:qid.CAst.loc ~hdr:"global"
           (str "Unexpected reference to a notation: " ++
-           pr_qualid v)
+           pr_qualid qid)
   with Not_found ->
     error_global_not_found qid
 
@@ -510,40 +509,40 @@ let path_of_universe mp =
 
 (* Shortest qualid functions **********************************************)
 
-let shortest_qualid_of_global ctx ref =
+let shortest_qualid_of_global ?loc ctx ref =
   match ref with
-    | VarRef id -> make_qualid DirPath.empty id
+    | VarRef id -> make_qualid ?loc DirPath.empty id
     | _ ->
         let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
-        ExtRefTab.shortest_qualid ctx sp !the_ccitab
+        ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
 
-let shortest_qualid_of_syndef ctx kn =
+let shortest_qualid_of_syndef ?loc ctx kn =
   let sp = path_of_syndef kn in
-    ExtRefTab.shortest_qualid ctx sp !the_ccitab
+    ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
 
-let shortest_qualid_of_module mp =
+let shortest_qualid_of_module ?loc mp =
   let dir = MPmap.find mp !the_modrevtab in
-    DirTab.shortest_qualid Id.Set.empty dir !the_dirtab
+    DirTab.shortest_qualid ?loc Id.Set.empty dir !the_dirtab
 
-let shortest_qualid_of_modtype kn =
+let shortest_qualid_of_modtype ?loc kn =
   let sp = MPmap.find kn !the_modtyperevtab in
-    MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab
+    MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab
 
-let shortest_qualid_of_universe kn =
+let shortest_qualid_of_universe ?loc kn =
   let sp = UnivIdMap.find kn !the_univrevtab in
-    UnivTab.shortest_qualid Id.Set.empty sp !the_univtab
+    UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab
 
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
   with Not_found as e ->
     if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
 
-let global_inductive ({CAst.loc; v=r} as lr) =
-  match global lr with
+let global_inductive qid =
+  match global qid with
   | IndRef ind -> ind
   | ref ->
-      user_err ?loc ~hdr:"global_inductive"
-        (pr_reference lr ++ spc () ++ str "is not an inductive type")
+      user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+        (pr_qualid qid ++ spc () ++ str "is not an inductive type")
 
 (********************************************************************)
 
diff --git a/library/nametab.mli b/library/nametab.mli
index 2ec73a986..57e9141db 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -61,7 +61,7 @@ open Globnames
 exception GlobalizationError of qualid
 
 (** Raises a globalization error *)
-val error_global_not_found : qualid CAst.t -> 'a
+val error_global_not_found : qualid -> 'a
 
 (** {6 Register visibility of things } *)
 
@@ -105,8 +105,8 @@ val locate_universe : qualid -> universe_id
    references, like [locate] and co, but raise a nice error message
    in case of failure *)
 
-val global : reference -> GlobRef.t
-val global_inductive : reference -> inductive
+val global : qualid -> GlobRef.t
+val global_inductive : qualid -> inductive
 
 (** These functions locate all global references with a given suffix;
    if [qualid] is valid as such, it comes first in the list *)
@@ -168,11 +168,11 @@ val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t
    Coq.A.B.x that denotes the same object.
    @raise Not_found for unknown objects. *)
 
-val shortest_qualid_of_global : Id.Set.t -> GlobRef.t -> qualid
-val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid
-val shortest_qualid_of_modtype : ModPath.t -> qualid
-val shortest_qualid_of_module : ModPath.t -> qualid
-val shortest_qualid_of_universe : universe_id -> qualid
+val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
+val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
+val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
+val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> universe_id -> qualid
 
 (** Deprecated synonyms *)
 
@@ -207,7 +207,7 @@ module type NAMETREE = sig
   val find : user_name -> t -> elt
   val exists : user_name -> t -> bool
   val user_name : qualid -> t -> user_name
-  val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
+  val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
 end
 
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
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
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 5a54c6f05..fe49d64c7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -87,7 +87,7 @@ let encode_tuple ({CAst.loc} as r) =
 
 module PrintingInductiveMake =
   functor (Test : sig
-     val encode : reference -> inductive
+     val encode : qualid -> inductive
      val member_message : Pp.t -> bool -> Pp.t
      val field : string
      val title : string
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 5310455fe..8695d52b1 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -87,7 +87,7 @@ val subst_genarg_hook :
 
 module PrintingInductiveMake :
   functor (Test : sig
-    val encode : Libnames.reference -> Names.inductive
+    val encode : Libnames.qualid -> Names.inductive
     val member_message : Pp.t -> bool -> Pp.t
     val field : string
     val title : string
@@ -95,7 +95,7 @@ module PrintingInductiveMake :
     sig
       type t = Names.inductive
       val compare : t -> t -> int
-      val encode : Libnames.reference -> Names.inductive
+      val encode : Libnames.qualid -> Names.inductive
       val subst : substitution -> t -> t
       val printer : t -> Pp.t
       val key : Goptions.option_name
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 11cfd2040..ba193da60 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -51,7 +51,7 @@ let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
 | GType l1, GType l2 ->
-   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2
+   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2
 | _ -> false
 
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 54fa5328f..86245d479 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -33,11 +33,11 @@ type 'a universe_kind =
   | UUnknown
   | UNamed of 'a
 
-type level_info = Libnames.reference universe_kind
+type level_info = Libnames.qualid universe_kind
 type glob_level = level_info glob_sort_gen
 type glob_constraint = glob_level * Univ.constraint_type * glob_level
 
-type sort_info = (Libnames.reference * int) option list
+type sort_info = (Libnames.qualid * int) option list
 type glob_sort = sort_info glob_sort_gen
 
 (** Casts *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9e024b1c2..57c4d363b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -171,38 +171,37 @@ let _ =
 
 (** Miscellaneous interpretation functions *)
 
-let interp_known_universe_level evd r =
-  let qid = Libnames.qualid_of_reference r in
+let interp_known_universe_level evd qid =
   try
-    match r.CAst.v with
-    | Libnames.Ident id -> Evd.universe_of_name evd id
-    | Libnames.Qualid _ -> raise Not_found
+    let open Libnames in
+    if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
+    else raise Not_found
   with Not_found ->
-    let univ, k = Nametab.locate_universe qid.CAst.v in
+    let univ, k = Nametab.locate_universe qid in
     Univ.Level.make univ k
 
-let interp_universe_level_name ~anon_rigidity evd r =
-  try evd, interp_known_universe_level evd r
+let interp_universe_level_name ~anon_rigidity evd qid =
+  try evd, interp_known_universe_level evd qid
   with Not_found ->
-    match r with (* Qualified generated name *)
-    | {CAst.loc; v=Libnames.Qualid qid} ->
-       let dp, i = Libnames.repr_qualid qid in
-       let num =
-         try int_of_string (Id.to_string i)
-         with Failure _ ->
-           user_err ?loc ~hdr:"interp_universe_level_name"
-                    (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r))
-       in
-       let level = Univ.Level.make dp num in
-       let evd =
-         try Evd.add_global_univ evd level
-         with UGraph.AlreadyDeclared -> evd
-       in evd, level
-    | {CAst.loc; v=Libnames.Ident id} -> (* Undeclared *)
-        if not (is_strict_universe_declarations ()) then
-          new_univ_level_variable ?loc ~name:id univ_rigid evd
-        else user_err ?loc ~hdr:"interp_universe_level_name"
-                      (Pp.(str "Undeclared universe: " ++ Id.print id))
+    if Libnames.qualid_is_ident qid then (* Undeclared *)
+      let id = Libnames.qualid_basename qid in
+      if not (is_strict_universe_declarations ()) then
+        new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd
+      else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
+          (Pp.(str "Undeclared universe: " ++ Id.print id))
+    else
+      let dp, i = Libnames.repr_qualid qid in
+      let num =
+        try int_of_string (Id.to_string i)
+        with Failure _ ->
+          user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
+            (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
+      in
+      let level = Univ.Level.make dp num in
+      let evd =
+        try Evd.add_global_univ evd level
+        with UGraph.AlreadyDeclared -> evd
+      in evd, level
 
 let interp_universe ?loc evd = function
   | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
@@ -232,10 +231,10 @@ let interp_known_level_info ?loc evd = function
   | UUnknown | UAnonymous ->
     user_err ?loc ~hdr:"interp_known_level_info"
       (str "Anonymous universes not allowed here.")
-  | UNamed ref ->
-    try interp_known_universe_level evd ref
+  | UNamed qid ->
+    try interp_known_universe_level evd qid
     with Not_found ->
-      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref)
+      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
 
 let interp_level_info ?loc evd : level_info -> _ = function
   | UUnknown -> new_univ_level_variable ?loc univ_rigid evd
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 605781993..e38da45b9 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -159,7 +159,7 @@ let tag_var = tag Tag.variable
 
   let pr_univ_expr = function
     | Some (x,n) ->
-       pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
+       pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
     | None -> str"_"
 
   let pr_univ l =
@@ -180,7 +180,7 @@ let tag_var = tag Tag.variable
     | GSet -> tag_type (str "Set")
     | GType UUnknown -> tag_type (str "Type")
     | GType UAnonymous -> tag_type (str "_")
-    | GType (UNamed u) -> tag_type (pr_reference u)
+    | GType (UNamed u) -> tag_type (pr_qualid u)
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
@@ -205,16 +205,16 @@ let tag_var = tag Tag.variable
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | UNamed u -> pr_reference u
+        | UNamed u -> pr_qualid u
         | UAnonymous -> tag_type (str "Type")
         | UUnknown -> tag_type (str "_"))
 
   let pr_universe_instance l =
     pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l
 
-  let pr_reference = CAst.with_val (function
-  | Qualid qid -> pr_qualid qid
-  | Ident id -> tag_var (pr_id id))
+  let pr_reference qid =
+    if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid)
+    else pr_qualid qid
 
   let pr_cref ref us =
     pr_reference ref ++ pr_universe_instance us
@@ -564,9 +564,9 @@ let tag_var = tag Tag.variable
           return (p ++ prlist (pr spc (lapp,L)) l2, lapp)
         else
           return (p, lproj)
-      | CAppExpl ((None,{v=Ident var},us),[t])
-      | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None])
-          when Id.equal var Notation_ops.ldots_var ->
+      | CAppExpl ((None,qid,us),[t])
+      | CApp ((_, {v = CRef(qid,us)}),[t,None])
+          when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var ->
         return (
           hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."),
           larg
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index ce37c3614..bca419c9a 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -47,7 +47,7 @@ val pr_guard_annot : (constr_expr -> Pp.t) ->
   lident option * recursion_order_expr ->
   Pp.t
 
-val pr_record_body : (reference * constr_expr) list -> Pp.t
+val pr_record_body : (qualid * constr_expr) list -> Pp.t
 val pr_binders : local_binder_expr list -> Pp.t
 val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t
 val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fe6cf73c7..5e5d00362 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -344,8 +344,7 @@ let register_locatable name f =
 
 exception ObjFound of logical_name
 
-let locate_any_name ref =
-  let {v=qid} = qualid_of_reference ref in
+let locate_any_name qid =
   try Term (Nametab.locate qid)
   with Not_found ->
   try Syntactic (Nametab.locate_syndef qid)
@@ -452,8 +451,7 @@ type locatable_kind =
 | LocOther of string
 | LocAny
 
-let print_located_qualid name flags ref =
-  let {v=qid} = qualid_of_reference ref in
+let print_located_qualid name flags qid =
   let located = match flags with
   | LocTerm -> locate_term qid
   | LocModule -> locate_modtype qid @ locate_module qid
@@ -787,10 +785,9 @@ let print_full_pure_context env sigma =
    follows the definition of the inductive type *)
 
 (* This is designed to print the contents of an opened section *)
-let read_sec_context r =
-  let qid = qualid_of_reference r in
+let read_sec_context qid =
   let dir =
-    try Nametab.locate_section qid.v
+    try Nametab.locate_section qid
     with Not_found ->
       user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in
   let rec get_cxt in_cxt = function
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 0375cfc92..8dd729610 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -24,20 +24,20 @@ val print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node
 val print_full_context : env -> Evd.evar_map -> Pp.t
 val print_full_context_typ : env -> Evd.evar_map -> Pp.t
 val print_full_pure_context : env -> Evd.evar_map -> Pp.t
-val print_sec_context : env -> Evd.evar_map -> reference -> Pp.t
-val print_sec_context_typ : env -> Evd.evar_map -> reference -> Pp.t
+val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t
+val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t
 val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t
 val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t
 val print_eval :
   reduction_function -> env -> Evd.evar_map ->
     Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
-val print_name : env -> Evd.evar_map -> reference Constrexpr.or_by_notation ->
+val print_name : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
   UnivNames.univ_name_list option -> Pp.t
-val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
-val print_about : env -> Evd.evar_map -> reference Constrexpr.or_by_notation ->
+val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t
+val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
   UnivNames.univ_name_list option -> Pp.t
-val print_impargs : reference Constrexpr.or_by_notation -> Pp.t
+val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
 val print_graph : env -> evar_map -> Pp.t
@@ -77,10 +77,10 @@ val register_locatable : string -> 'a locatable_info -> unit
     name describing the kind of objects considered and that is added as a
     grammar command prefix for vernacular commands Locate. *)
 
-val print_located_qualid : reference -> Pp.t
-val print_located_term : reference -> Pp.t
-val print_located_module : reference -> Pp.t
-val print_located_other : string -> reference -> Pp.t
+val print_located_qualid : qualid -> Pp.t
+val print_located_term : qualid -> Pp.t
+val print_located_module : qualid -> Pp.t
+val print_located_other : string -> qualid -> Pp.t
 
 type object_pr = {
   print_inductive           : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
diff --git a/printing/printer.ml b/printing/printer.ml
index 72030dc9f..d76bd1e2b 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
diff --git a/stm/stm.ml b/stm/stm.ml
index c394be22e..0aed88a53 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2558,8 +2558,8 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
 
   let load_objs libs =
     let rq_file (dir, from, exp) =
-      let mp = CAst.make @@ Libnames.(Qualid (qualid_of_string dir)) in
-      let mfrom = Option.map (fun fr -> CAst.make @@ Libnames.(Qualid (qualid_of_string fr))) from in
+      let mp = Libnames.qualid_of_string dir in
+      let mfrom = Option.map Libnames.qualid_of_string from in
       Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
     List.(iter rq_file (rev libs))
   in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index d49c8aaa5..85ff02824 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -125,7 +125,7 @@ type 'a hints_path_gen =
   | PathEmpty
   | PathEpsilon
 
-type pre_hints_path = Libnames.reference hints_path_gen
+type pre_hints_path = Libnames.qualid hints_path_gen
 type hints_path = GlobRef.t hints_path_gen
 
 type hint_term =
@@ -157,7 +157,7 @@ type hint_entry = GlobRef.t option *
   raw_hint hint_ast with_uid with_metadata
 
 type reference_or_constr =
-  | HintsReference of reference
+  | HintsReference of qualid
   | HintsConstr of Constrexpr.constr_expr
 
 type hint_mode =
@@ -167,12 +167,12 @@ type hint_mode =
 
 type hints_expr =
   | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
-  | HintsResolveIFF of bool * reference list * int option
+  | HintsResolveIFF of bool * qualid list * int option
   | HintsImmediate of reference_or_constr list
-  | HintsUnfold of reference list
-  | HintsTransparency of reference list * bool
-  | HintsMode of reference * hint_mode list
-  | HintsConstructors of reference list
+  | HintsUnfold of qualid list
+  | HintsTransparency of qualid list * bool
+  | HintsMode of qualid * hint_mode list
+  | HintsConstructors of qualid list
   | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
 
 type import_level = [ `LAX | `WARN | `STRICT ]
@@ -1360,7 +1360,7 @@ let interp_hints poly =
       let constr_hints_of_ind qid =
         let ind = global_inductive_with_alias qid in
 	let mib,_ = Global.lookup_inductive ind in
-        Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_reference qid) "ind";
+        Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind";
           List.init (nconstructors ind) 
 	    (fun i -> let c = (ind,i+1) in
 		      let gr = ConstructRef c in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index e958f986e..ca18f835a 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -73,7 +73,7 @@ type search_entry
 type hint_entry
 
 type reference_or_constr =
-  | HintsReference of Libnames.reference
+  | HintsReference of Libnames.qualid
   | HintsConstr of Constrexpr.constr_expr
 
 type hint_mode =
@@ -83,12 +83,12 @@ type hint_mode =
 
 type hints_expr =
   | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
-  | HintsResolveIFF of bool * Libnames.reference list * int option
+  | HintsResolveIFF of bool * Libnames.qualid list * int option
   | HintsImmediate of reference_or_constr list
-  | HintsUnfold of Libnames.reference list
-  | HintsTransparency of Libnames.reference list * bool
-  | HintsMode of Libnames.reference * hint_mode list
-  | HintsConstructors of Libnames.reference list
+  | HintsUnfold of Libnames.qualid list
+  | HintsTransparency of Libnames.qualid list * bool
+  | HintsMode of Libnames.qualid * hint_mode list
+  | HintsConstructors of Libnames.qualid list
   | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
 
 type 'a hints_path_gen =
@@ -99,7 +99,7 @@ type 'a hints_path_gen =
   | PathEmpty
   | PathEpsilon
 
-type pre_hints_path = Libnames.reference hints_path_gen
+type pre_hints_path = Libnames.qualid hints_path_gen
 type hints_path = GlobRef.t hints_path_gen
     
 val normalize_path : hints_path -> hints_path
@@ -110,9 +110,9 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t
 val pp_hints_path : hints_path -> Pp.t
 val pp_hint_mode : hint_mode -> Pp.t
 val glob_hints_path_atom :
-  Libnames.reference hints_path_atom_gen -> GlobRef.t hints_path_atom_gen
+  Libnames.qualid hints_path_atom_gen -> GlobRef.t hints_path_atom_gen
 val glob_hints_path :
-  Libnames.reference hints_path_gen -> GlobRef.t hints_path_gen
+  Libnames.qualid hints_path_gen -> GlobRef.t hints_path_gen
 
 module Hint_db :
   sig
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 8cf3895fb..382d18b09 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -229,10 +229,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
             let sigma, c = interp_casted_constr_evars env' sigma term cty in
             Some (Inr (c, subst)), sigma
 	| Some (Inl props) ->
-            let get_id = CAst.map (function
-                | Ident id' -> id'
-                | Qualid id' -> snd (repr_qualid id'))
-	    in
+            let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in
 	    let props, rest =
 	      List.fold_left
 		(fun (props, rest) decl ->
diff --git a/vernac/classes.mli b/vernac/classes.mli
index eea2a211d..bd30b2d60 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,7 +22,7 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
 
 (** Instance declaration *)
 
-val existing_instance : bool -> reference -> Hints.hint_info_expr option -> unit
+val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
 val declare_instance_constant :
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index b93e8d9ac..6057c05f5 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -44,8 +44,8 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
         user_err ?loc
          (strbrk"Cannot infer the non constant arguments of the conclusion of "
           ++ Id.print cs ++ str ".");
-      let args = List.map (fun id -> CAst.(make ?loc @@ CRef(make ?loc @@ Ident id,None))) params in
-      CAppExpl ((None,CAst.make ?loc @@ Ident name,None),List.rev args)
+      let args = List.map (fun id -> CAst.(make ?loc @@ CRef(qualid_of_ident ?loc id,None))) params in
+      CAppExpl ((None,qualid_of_ident ?loc name,None),List.rev args)
   | c -> c
   )
 
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index a6d7fccf3..eef7afbfb 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -44,7 +44,7 @@ let mkSubset sigma name typ prop =
 
 let sigT = Lazy.from_fun build_sigma_type
 
-let make_qref s = CAst.make @@ Qualid (qualid_of_string s)
+let make_qref s = qualid_of_string s
 let lt_ref = make_qref "Init.Peano.lt"
 
 let rec telescope sigma l =
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 434e836d8..cc9be7b0e 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -229,7 +229,7 @@ type prod_info = production_level * production_position
 
 type (_, _) entry =
 | TTName : ('self, lname) entry
-| TTReference : ('self, reference) entry
+| TTReference : ('self, qualid) entry
 | TTBigint : ('self, Constrexpr.raw_natural_number) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
@@ -312,7 +312,7 @@ let interp_entry forpat e = match e with
 
 let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with
   | Anonymous -> CPatAtom None
-  | Name id   -> CPatAtom (Some (CAst.make ?loc @@ Ident id))
+  | Name id   -> CPatAtom (Some (qualid_of_ident ?loc id))
 
 type 'r env = {
   constrs : 'r list;
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index 3a59242de..16934fc86 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -549,7 +549,7 @@ GEXTEND Gram
       ] ]
   ;
   module_expr_atom:
-    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ]
+    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid | "("; me = module_expr; ")" -> me ] ]
   ;
   with_declaration:
     [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
@@ -559,7 +559,7 @@ GEXTEND Gram
       ] ]
   ;
   module_type:
-    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v)
+    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid
       | "("; mt = module_type; ")" -> mt
       | mty = module_type; me = module_expr_atom ->
           CAst.make ~loc:!@loc @@ CMapply (mty,me)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8f64f5519..da14358ef 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1449,7 +1449,7 @@ let add_notation_extra_printing_rule df k v =
 
 (* Infix notations *)
 
-let inject_var x = CAst.make @@ CRef (CAst.make @@ Ident (Id.of_string x),None)
+let inject_var x = CAst.make @@ CRef (qualid_of_ident (Id.of_string x),None)
 
 let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
   check_infix_modifiers modifiers;
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index d0c423650..56dfaa54a 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -16,7 +16,6 @@ open Util
 open CAst
 
 open Extend
-open Libnames
 open Decl_kinds
 open Constrexpr
 open Constrexpr_ops
@@ -79,13 +78,13 @@ open Pputils
   let pr_lname_decl (n, u) =
     pr_lname n ++ pr_universe_decl u
 
-  let pr_smart_global = Pputils.pr_or_by_notation pr_reference
+  let pr_smart_global = Pputils.pr_or_by_notation pr_qualid
 
-  let pr_ltac_ref = Libnames.pr_reference
+  let pr_ltac_ref = Libnames.pr_qualid
 
-  let pr_module = Libnames.pr_reference
+  let pr_module = Libnames.pr_qualid
 
-  let pr_import_module = Libnames.pr_reference
+  let pr_import_module = Libnames.pr_qualid
 
   let sep_end = function
     | VernacBullet _
@@ -157,7 +156,7 @@ open Pputils
   let pr_locality local = if local then keyword "Local" else keyword "Global"
 
   let pr_option_ref_value = function
-    | QualidRefValue id -> pr_reference id
+    | QualidRefValue id -> pr_qualid id
     | StringRefValue s -> qs s
 
   let pr_printoption table b =
@@ -180,7 +179,7 @@ open Pputils
     | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
 
   let pr_reference_or_constr pr_c = function
-    | HintsReference r -> pr_reference r
+    | HintsReference r -> pr_qualid r
     | HintsConstr c -> pr_c c
 
   let pr_hint_mode = function
@@ -202,24 +201,24 @@ open Pputils
             l
         | HintsResolveIFF (l2r, l, n) ->
           keyword "Resolve " ++ str (if l2r then "->" else "<-")
-          ++ prlist_with_sep sep pr_reference l
+          ++ prlist_with_sep sep pr_qualid l
         | HintsImmediate l ->
           keyword "Immediate" ++ spc() ++
             prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l
         | HintsUnfold l ->
-          keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_reference l
+          keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_qualid l
         | HintsTransparency (l, b) ->
           keyword (if b then "Transparent" else "Opaque")
           ++ spc ()
-          ++ prlist_with_sep sep pr_reference l
+          ++ prlist_with_sep sep pr_qualid l
         | HintsMode (m, l) ->
           keyword "Mode"
           ++ spc ()
-          ++ pr_reference m ++ spc() ++
+          ++ pr_qualid m ++ spc() ++
             prlist_with_sep spc pr_hint_mode l
         | HintsConstructors c ->
           keyword "Constructors"
-          ++ spc() ++ prlist_with_sep spc pr_reference c
+          ++ spc() ++ prlist_with_sep spc pr_qualid c
         | HintsExtern (n,c,tac) ->
           let pat = match c with None -> mt () | Some pat -> pr_pat pat in
           keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
@@ -233,7 +232,7 @@ open Pputils
       keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p
     | CWith_Module (id,qid) ->
       keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
-        pr_ast pr_qualid qid
+        pr_qualid qid
 
   let rec pr_module_ast leading_space pr_c = function
     | { loc ; v = CMident qid } ->
@@ -451,7 +450,7 @@ open Pputils
     | PrintFullContext ->
       keyword "Print All"
     | PrintSectionContext s ->
-      keyword "Print Section" ++ spc() ++ Libnames.pr_reference s
+      keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s
     | PrintGrammar ent ->
       keyword "Print Grammar" ++ spc() ++ str ent
     | PrintLoadPath dir ->
@@ -499,9 +498,9 @@ open Pputils
     | PrintName (qid,udecl) ->
       keyword "Print" ++ spc()  ++ pr_smart_global qid ++ pr_univ_name_list udecl
     | PrintModuleType qid ->
-      keyword "Print Module Type" ++ spc() ++ pr_reference qid
+      keyword "Print Module Type" ++ spc() ++ pr_qualid qid
     | PrintModule qid ->
-      keyword "Print Module" ++ spc() ++ pr_reference qid
+      keyword "Print Module" ++ spc() ++ pr_qualid qid
     | PrintInspect n ->
       keyword "Inspect" ++ spc() ++ int n
     | PrintScopes ->
@@ -604,7 +603,7 @@ open Pputils
           | ShowUniverses -> keyword "Show Universes"
           | ShowProofNames -> keyword "Show Conjectures"
           | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
-          | ShowMatch id -> keyword "Show Match " ++ pr_reference id
+          | ShowMatch id -> keyword "Show Match " ++ pr_qualid id
         in
         return (pr_showable s)
       | VernacCheckGuard ->
@@ -901,7 +900,7 @@ open Pputils
 
       | VernacDeclareInstances insts ->
          let pr_inst (id, info) =
-           pr_reference id ++ pr_hint_info pr_constr_pattern_expr info
+           pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info
          in
          return (
           hov 1 (keyword "Existing" ++ spc () ++
@@ -911,7 +910,7 @@ open Pputils
 
       | VernacDeclareClass id ->
         return (
-          hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id)
+          hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id)
         )
 
       (* Modules and Module Types *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 94eb45fd3..479482095 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -183,29 +183,27 @@ let print_modules () =
   pr_vertical_list DirPath.print only_loaded
 
 
-let print_module r =
-  let qid = qualid_of_reference r in
+let print_module qid =
   try
-    let globdir = Nametab.locate_dir qid.v in
+    let globdir = Nametab.locate_dir qid in
       match globdir with
           DirModule { obj_dir; obj_mp; _ } ->
           Printmod.print_module (Printmod.printable_body obj_dir) obj_mp
 	| _ -> raise Not_found
   with
-    Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid.v)
+    Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid)
 
-let print_modtype r =
-  let qid = qualid_of_reference r in
+let print_modtype qid =
   try
-    let kn = Nametab.locate_modtype qid.v in
+    let kn = Nametab.locate_modtype qid in
     Printmod.print_modtype kn
   with Not_found ->
     (* Is there a module of this name ? If yes we display its type *)
     try
-      let mp = Nametab.locate_module qid.v in
+      let mp = Nametab.locate_module qid in
       Printmod.print_module false mp
     with Not_found ->
-      user_err (str"Unknown Module Type or Module " ++ pr_qualid qid.v)
+      user_err (str"Unknown Module Type or Module " ++ pr_qualid qid)
 
 let print_namespace ns =
   let ns = List.rev (Names.DirPath.repr ns) in
@@ -367,33 +365,32 @@ let msg_found_library = function
   | Library.LibInPath, fulldir, file ->
     hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file)
 
-let err_unmapped_library ?loc ?from qid =
+let err_unmapped_library ?from qid =
   let dir = fst (repr_qualid qid) in
   let prefix = match from with
   | None -> str "."
   | Some from ->
     str " and prefix " ++ DirPath.print from ++ str "."
   in
-  user_err ?loc
+  user_err ?loc:qid.CAst.loc
     ~hdr:"locate_library"
     (strbrk "Cannot find a physical path bound to logical path matching suffix " ++
        DirPath.print dir ++ prefix)
 
-let err_notfound_library ?loc ?from qid =
+let err_notfound_library ?from qid =
   let prefix = match from with
   | None -> str "."
   | Some from ->
     str " with prefix " ++ DirPath.print from ++ str "."
   in
-  user_err ?loc ~hdr:"locate_library"
+  user_err ?loc:qid.CAst.loc ~hdr:"locate_library"
      (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
 
-let print_located_library r =
-  let {loc;v=qid} = qualid_of_reference r in
+let print_located_library qid =
   try msg_found_library (Library.locate_qualified_library ~warn:false qid)
   with
-    | Library.LibUnmappedDir -> err_unmapped_library ?loc qid
-    | Library.LibNotFound -> err_notfound_library ?loc qid
+    | Library.LibUnmappedDir -> err_unmapped_library qid
+    | Library.LibNotFound -> err_notfound_library qid
 
 let smart_global r =
   let gr = Smartlocate.smart_global r in
@@ -636,7 +633,7 @@ let vernac_scheme l =
 let vernac_combined_scheme lid l =
   if Dumpglob.dump () then
     (Dumpglob.dump_definition lid false "def";
-     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (make ?loc @@ Ident id))) l);
+     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (qualid_of_ident ?loc id))) l);
  Indschemes.do_combined_scheme lid l
 
 let vernac_universe ~atts l =
@@ -657,7 +654,7 @@ let vernac_constraint ~atts l =
 (* Modules            *)
 
 let vernac_import export refl =
-  Library.import_module export (List.map qualid_of_reference refl)
+  Library.import_module export refl
 
 let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
   (* We check the state of the system (in section, in module type)
@@ -675,7 +672,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
   in
   Dumpglob.dump_moddef ?loc mp "mod";
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
-  Option.iter (fun export -> vernac_import export [make @@ Ident id]) export
+  Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export
 
 let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
   (* We check the state of the system (in section, in module type)
@@ -700,7 +697,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
        List.iter
          (fun (export,id) ->
            Option.iter
-             (fun export -> vernac_import export [make @@ Ident id]) export
+             (fun export -> vernac_import export [qualid_of_ident id]) export
          ) argsexport
     | _::_ ->
        let binders_ast = List.map
@@ -715,14 +712,14 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
        Dumpglob.dump_moddef ?loc mp "mod";
        Flags.if_verbose Feedback.msg_info
 	 (str "Module " ++ Id.print id ++ str " is defined");
-       Option.iter (fun export -> vernac_import export [make @@ Ident id])
+       Option.iter (fun export -> vernac_import export [qualid_of_ident id])
          export
 
 let vernac_end_module export {loc;v=id} =
   let mp = Declaremods.end_module () in
   Dumpglob.dump_modref ?loc mp "mod";
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
-  Option.iter (fun export -> vernac_import export [make ?loc @@ Ident id]) export
+  Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
 
 let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
   if Lib.sections_are_opened () then
@@ -747,7 +744,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
        List.iter
          (fun (export,id) ->
            Option.iter
-             (fun export -> vernac_import export [make ?loc @@ Ident id]) export
+             (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
          ) argsexport
 
     | _ :: _ ->
@@ -809,22 +806,20 @@ let warn_require_in_section =
 
 let vernac_require from import qidl =
   if Lib.sections_are_opened () then warn_require_in_section ();
-  let qidl = List.map qualid_of_reference qidl in
   let root = match from with
   | None -> None
   | Some from ->
-    let qid = Libnames.qualid_of_reference from in
-    let (hd, tl) = Libnames.repr_qualid qid.v in
+    let (hd, tl) = Libnames.repr_qualid from in
     Some (Libnames.add_dirpath_suffix hd tl)
   in
-  let locate {loc;v=qid} =
+  let locate qid =
     try
       let warn = not !Flags.quiet in
       let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in
       (dir, f)
     with
-      | Library.LibUnmappedDir -> err_unmapped_library ?loc ?from:root qid
-      | Library.LibNotFound -> err_notfound_library ?loc ?from:root qid
+      | Library.LibUnmappedDir -> err_unmapped_library ?from:root qid
+      | Library.LibNotFound -> err_notfound_library ?from:root qid
   in
   let modrefl = List.map locate qidl in
   if Dumpglob.dump () then
@@ -1687,10 +1682,10 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
     let glnumopt = query_command_selector ?loc glopt in
     let gl,id =
       match glnumopt, ref_or_by_not.v with
-      | None,AN {v=Ident id} -> (* goal number not given, catch any failure *)
-	 (try get_nth_goal 1,id with _ -> raise NoHyp)
-      | Some n,AN {v=Ident id} ->  (* goal number given, catch if wong *)
-	 (try get_nth_goal n,id
+      | None,AN qid when qualid_is_ident qid -> (* goal number not given, catch any failure *)
+         (try get_nth_goal 1, qualid_basename qid with _ -> raise NoHyp)
+      | Some n,AN qid when qualid_is_ident qid ->  (* goal number given, catch if wong *)
+         (try get_nth_goal n, qualid_basename qid
 	  with
 	    Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs"
                           (str "No such goal: " ++ int n ++ str "."))
@@ -1771,11 +1766,10 @@ let vernac_print ~atts env sigma =
       Printer.pr_assumptionset env sigma nassums
   | PrintStrategy r -> print_strategy r
 
-let global_module r =
-  let {loc;v=qid} = qualid_of_reference r in
+let global_module qid =
   try Nametab.full_name_module qid
   with Not_found ->
-    user_err ?loc ~hdr:"global_module"
+    user_err ?loc:qid.CAst.loc ~hdr:"global_module"
      (str "Module/section " ++ pr_qualid qid ++ str " not found.")
 
 let interp_search_restriction = function
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 3c88a3443..02a3b2bd6 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -8,11 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val dump_global : Libnames.reference Constrexpr.or_by_notation -> unit
+val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit
 
 (** Vernacular entries *)
 val vernac_require :
-  Libnames.reference option -> bool option -> Libnames.reference list -> unit
+  Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
 
 (** The main interpretation function of vernacular expressions *)
 val interp :
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 5acac9e25..f74383b02 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -13,7 +13,7 @@ open Constrexpr
 open Libnames
 
 (** Vernac expressions, produced by the parser *)
-type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
+type class_rawexpr = FunClass | SortClass | RefClass of qualid or_by_notation
 
 type goal_selector = Goal_select.t =
   | SelectAlreadyFocused
@@ -37,37 +37,37 @@ type univ_name_list = UnivNames.univ_name_list
 type printable =
   | PrintTables
   | PrintFullContext
-  | PrintSectionContext of reference
+  | PrintSectionContext of qualid
   | PrintInspect of int
   | PrintGrammar of string
   | PrintLoadPath of DirPath.t option
   | PrintModules
-  | PrintModule of reference
-  | PrintModuleType of reference
+  | PrintModule of qualid
+  | PrintModuleType of qualid
   | PrintNamespace of DirPath.t
   | PrintMLLoadPath
   | PrintMLModules
   | PrintDebugGC
-  | PrintName of reference or_by_notation * UnivNames.univ_name_list option
+  | PrintName of qualid or_by_notation * UnivNames.univ_name_list option
   | PrintGraph
   | PrintClasses
   | PrintTypeClasses
-  | PrintInstances of reference or_by_notation
+  | PrintInstances of qualid or_by_notation
   | PrintCoercions
   | PrintCoercionPaths of class_rawexpr * class_rawexpr
   | PrintCanonicalConversions
   | PrintUniverses of bool * string option
-  | PrintHint of reference or_by_notation
+  | PrintHint of qualid or_by_notation
   | PrintHintGoal
   | PrintHintDbName of string
   | PrintHintDb
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
-  | PrintAbout of reference or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
-  | PrintImplicit of reference or_by_notation
-  | PrintAssumptions of bool * bool * reference or_by_notation
-  | PrintStrategy of reference or_by_notation option
+  | PrintAbout of qualid or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
+  | PrintImplicit of qualid or_by_notation
+  | PrintAssumptions of bool * bool * qualid or_by_notation
+  | PrintStrategy of qualid or_by_notation option
 
 type search_about_item =
   | SearchSubPattern of constr_pattern_expr
@@ -80,11 +80,11 @@ type searchable =
   | SearchAbout of (bool * search_about_item) list
 
 type locatable =
-  | LocateAny of reference or_by_notation
-  | LocateTerm of reference or_by_notation
-  | LocateLibrary of reference
-  | LocateModule of reference
-  | LocateOther of string * reference
+  | LocateAny of qualid or_by_notation
+  | LocateTerm of qualid or_by_notation
+  | LocateLibrary of qualid
+  | LocateModule of qualid
+  | LocateOther of string * qualid
   | LocateFile of string
 
 type showable =
@@ -95,7 +95,7 @@ type showable =
   | ShowUniverses
   | ShowProofNames
   | ShowIntros of bool
-  | ShowMatch of reference
+  | ShowMatch of qualid
 
 type comment =
   | CommentConstr of constr_expr
@@ -103,7 +103,7 @@ type comment =
   | CommentInt of int
 
 type reference_or_constr = Hints.reference_or_constr =
-  | HintsReference of reference
+  | HintsReference of qualid
   | HintsConstr of constr_expr
 [@@ocaml.deprecated "Please use [Hints.reference_or_constr]"]
 
@@ -123,18 +123,18 @@ type hint_info_expr = Hints.hint_info_expr
 
 type hints_expr = Hints.hints_expr =
   | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list
-  | HintsResolveIFF of bool * reference list * int option
+  | HintsResolveIFF of bool * qualid list * int option
   | HintsImmediate of Hints.reference_or_constr list
-  | HintsUnfold of reference list
-  | HintsTransparency of reference list * bool
-  | HintsMode of reference * Hints.hint_mode list
-  | HintsConstructors of reference list
+  | HintsUnfold of qualid list
+  | HintsTransparency of qualid list * bool
+  | HintsMode of qualid * Hints.hint_mode list
+  | HintsConstructors of qualid list
   | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
 [@@ocaml.deprecated "Please use [Hints.hints_expr]"]
 
 type search_restriction =
-  | SearchInside of reference list
-  | SearchOutside of reference list
+  | SearchInside of qualid list
+  | SearchOutside of qualid list
 
 type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
@@ -159,7 +159,7 @@ type option_value = Goptions.option_value =
 
 type option_ref_value =
   | StringRefValue of string
-  | QualidRefValue of reference
+  | QualidRefValue of qualid
 
 (** Identifier and optional list of bound universes and constraints. *)
 
@@ -222,9 +222,9 @@ type proof_end =
   | Proved of Proof_global.opacity_flag * lident option
 
 type scheme =
-  | InductionScheme of bool * reference or_by_notation * sort_expr
-  | CaseScheme of bool * reference or_by_notation * sort_expr
-  | EqualityScheme of reference or_by_notation
+  | InductionScheme of bool * qualid or_by_notation * sort_expr
+  | CaseScheme of bool * qualid or_by_notation * sort_expr
+  | EqualityScheme of qualid or_by_notation
 
 type section_subset_expr =
   | SsEmpty
@@ -348,10 +348,10 @@ type nonrec vernac_expr =
   | VernacBeginSection of lident
   | VernacEndSegment of lident
   | VernacRequire of
-      reference option * export_flag option * reference list
-  | VernacImport of export_flag * reference list
-  | VernacCanonical of reference or_by_notation
-  | VernacCoercion of reference or_by_notation *
+      qualid option * export_flag option * qualid list
+  | VernacImport of export_flag * qualid list
+  | VernacCanonical of qualid or_by_notation
+  | VernacCoercion of qualid or_by_notation *
       class_rawexpr * class_rawexpr
   | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr
   | VernacNameSectionHypSet of lident * section_subset_expr
@@ -367,9 +367,9 @@ type nonrec vernac_expr =
   | VernacContext of local_binder_expr list
 
   | VernacDeclareInstances of
-    (reference * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
+    (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
 
-  | VernacDeclareClass of reference (* inductive or definition name *)
+  | VernacDeclareClass of qualid (* inductive or definition name *)
 
   (* Modules and Module Types *)
   | VernacDeclareModule of bool option * lident *
@@ -403,11 +403,11 @@ type nonrec vernac_expr =
 
   (* Commands *)
   | VernacCreateHintDb of string * bool
-  | VernacRemoveHints of string list * reference list
+  | VernacRemoveHints of string list * qualid list
   | VernacHints of string list * Hints.hints_expr
   | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
       onlyparsing_flag
-  | VernacArguments of reference or_by_notation *
+  | VernacArguments of qualid or_by_notation *
       vernac_argument_status list (* Main arguments status list *) *
         (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
       int option (* Number of args to trigger reduction *) *
@@ -416,9 +416,9 @@ type nonrec vernac_expr =
           `DefaultImplicits ] list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of (lident list) option
-  | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list)
+  | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list)
   | VernacSetStrategy of
-      (Conv_oracle.level * reference or_by_notation list) list
+      (Conv_oracle.level * qualid or_by_notation list) list
   | VernacUnsetOption of export_flag * Goptions.option_name
   | VernacSetOption of export_flag * Goptions.option_name * option_value
   | VernacAddOption of Goptions.option_name * option_ref_value list