Remove reference name type.

reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.

We remove the reference type and replace its uses by qualid.

14 files changed, 131 insertions, 125 deletions

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