Merge PR #7797: Remove reference name type.

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