[located] Push inner locations in `reference` to a CAst.t node.

The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.

An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.

It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.

9 files changed, 100 insertions, 120 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 8bf530e7f..4ee13c961 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -10,6 +10,7 @@
 
 open Pp
 open Util
+open CAst
 open Names
 open Nameops
 open Libnames
@@ -278,7 +279,7 @@ 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 (Ident (_,id))) when not (is_constructor id) -> f id a
+  | CPatAtom (Some {v=Ident id}) when not (is_constructor id) -> f id a
   | CPatPrim _ | CPatAtom _ -> a
   | CPatCast ({CAst.loc},_) ->
     CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names"
@@ -361,7 +362,7 @@ 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 (Ident (_,id),_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l
+    | { CAst.v = CRef ({v=Ident id},_) } -> 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
 
@@ -439,8 +440,8 @@ 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 (Ident (loc_id,id),us) } as x ->
-    (try CAst.make ?loc @@ CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x)
+  | { 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
 
@@ -511,7 +512,7 @@ let split_at_annot bl na =
 
 (** Pseudo-constructors *)
 
-let mkIdentC id   = CAst.make @@ CRef (Ident (Loc.tag id),None)
+let mkIdentC id   = CAst.make @@ CRef (make @@ 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)
@@ -530,21 +531,21 @@ let mkCProdN ?loc bll c =
 let mkCLambdaN ?loc bll c =
   CAst.make ?loc @@ CLambdaN (bll,c)
 
-let coerce_reference_to_id = function
-  | Ident (_,id) -> id
-  | Qualid (loc,_) ->
+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.")
+      (str "This expression should be a simple identifier."))
 
 let coerce_to_id = function
-  | { CAst.v = CRef (Ident (loc,id),None) } -> CAst.make ?loc id
+  | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc id
   | { CAst.loc; _ } -> CErrors.user_err ?loc
                          ~hdr:"coerce_to_id"
                          (str "This expression should be a simple identifier.")
 
 let coerce_to_name = function
-  | { CAst.v = CRef (Ident (loc,id),None) } -> CAst.make ?loc @@ Name id
-  | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous
+  | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc @@ Name id
+  | { CAst.loc; v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous
   | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
                          (str "This expression should be a name.")
 
@@ -570,7 +571,7 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
      CPatAtom (Some r)
   | CHole (None,Misctypes.IntroAnonymous,None) ->
      CPatAtom None
-  | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' ->
+  | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef ({v=Ident id'},None) }) when Id.equal id id' ->
       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/constrextern.ml b/interp/constrextern.ml
index f5a6a082e..19444988b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -215,7 +215,7 @@ let is_record indsp =
 let encode_record r =
   let indsp = global_inductive r in
   if not (is_record indsp) then
-    user_err ?loc:(loc_of_reference r) ~hdr:"encode_record"
+    user_err ?loc:r.CAst.loc ~hdr:"encode_record"
       (str "This type is not a structure type.");
   indsp
 
@@ -271,14 +271,14 @@ let extern_evar n l = CEvar (n,l)
     may be inaccurate *)
 
 let default_extern_reference ?loc vars r =
-  Qualid (Loc.tag ?loc @@ shortest_qualid_of_global vars r)
+  make @@ Qualid (shortest_qualid_of_global vars r)
 
 let my_extern_reference = ref default_extern_reference
 
 let set_extern_reference f = my_extern_reference := f
 let get_extern_reference () = !my_extern_reference
 
-let extern_reference ?loc vars l = !my_extern_reference ?loc vars l
+let extern_reference ?loc vars l = !my_extern_reference vars l
 
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
@@ -389,7 +389,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 (Ident (loc,id)))
+        | PatVar (Name id) -> CPatAtom (Some (make ?loc @@ Ident id))
 	| PatVar (Anonymous) -> CPatAtom None
 	| PatCstr(cstrsp,args,na) ->
 	  let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
@@ -407,7 +407,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 		          (* we don't want to have 'x := _' in our patterns *)
                           acc
 		       | Some c, _ ->
-		          ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc)
+                          ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc)
                        | _ -> raise No_match in
                      ip q tail acc
 	          | _ -> assert false
@@ -415,7 +415,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	      CPatRecord(List.rev (ip projs args []))
 	    with
 		Not_found | No_match | Exit ->
-                  let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in
+                  let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in
                   if !asymmetric_patterns then
 		    if pattern_printable_in_both_syntax cstrsp
 		    then CPatCstr (c, None, args)
@@ -458,7 +458,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 = Qualid (Loc.tag ?loc @@ shortest_qualid_of_syndef vars kn) in
+      let qid = make ?loc @@ Qualid (shortest_qualid_of_syndef 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 (Ident (loc,id)))
+        | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (make ?loc @@ Ident id))
     with
 	No_match -> extern_notation_pattern allscopes vars t rules
 
@@ -745,9 +745,9 @@ let rec extern inctx scopes vars r =
   with No_match -> lift (fun ?loc -> function
   | GRef (ref,us) ->
       extern_global (select_stronger_impargs (implicits_of_global ref))
-        (extern_reference ?loc vars ref) (extern_universes us)
+        (extern_reference vars ref) (extern_universes us)
 
-  | GVar id -> CRef (Ident (loc,id),None)
+  | GVar id -> CRef (make ?loc @@ Ident id,None)
 
   | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None)
 
@@ -763,7 +763,6 @@ let rec extern inctx scopes vars r =
   | GApp (f,args) ->
       (match DAst.get f with
 	 | GRef (ref,us) ->
-            let rloc = f.CAst.loc in
 	     let subscopes = find_arguments_scope ref in
 	     let args = fill_arg_scopes args subscopes (snd scopes) in
 	     begin
@@ -802,7 +801,7 @@ let rec extern inctx scopes vars r =
 				     (* we give up since the constructor is not complete *)
 				 | (arg, scopes) :: tail ->
                                      let head = extern true scopes vars arg in
-				     ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc)
+                                     ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc)
 		   in
 		 CRecord (List.rev (ip projs locals args []))
 	       with
@@ -810,7 +809,7 @@ let rec extern inctx scopes vars r =
                     let args = extern_args (extern true) vars args in
 		     extern_app inctx
 		       (select_stronger_impargs (implicits_of_global ref))
-		       (Some ref,extern_reference ?loc:rloc vars ref) (extern_universes us) args
+                       (Some ref,extern_reference ?loc vars ref) (extern_universes us) args
 	     end
 
 	 | _       ->
@@ -1090,7 +1089,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 (Qualid (loc, shortest_qualid_of_syndef vars kn),None) in
+              let a = CRef (make ?loc @@ Qualid (shortest_qualid_of_syndef 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/constrintern.ml b/interp/constrintern.ml
index 55b943eac..f2cd07c94 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -96,7 +96,7 @@ let is_global id =
     false
 
 let global_reference_of_reference ref =
-  locate_reference (snd (qualid_of_reference ref))
+  locate_reference (qualid_of_reference ref).CAst.v
 
 let global_reference id =
   locate_reference (qualid_of_ident id)
@@ -403,7 +403,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
 	  let name =
 	    let id =
 	      match ty with
-	      | { CAst.v = CApp ((_, { CAst.v = CRef (Ident (loc,id),_) } ), _) } -> id
+              | { v = CApp ((_, { v = CRef ({v=Ident id},_) } ), _) } -> id
 	      | _ -> default_non_dependent_ident
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
@@ -554,8 +554,8 @@ let is_var store pat =
   | _ -> false
 
 let out_var pat =
-  match pat.CAst.v with
-  | CPatAtom (Some (Ident (_,id))) -> Name id
+  match pat.v with
+  | CPatAtom (Some ({v=Ident id})) -> Name id
   | CPatAtom None -> Anonymous
   | _ -> assert false
 
@@ -621,18 +621,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 (Ident (loc,id), None)
+    | PatVar (Name id)   -> CRef (make @@ Ident id, None)
     | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc ()
     | PatCstr (c,l,_) ->
-       let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
+       let r = make ?loc @@ Qualid (qualid_of_path (path_of_global (ConstructRef c))) in
        let hole = CAst.make ?loc @@ CHole (None,Misctypes.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
   let rec extract_variables l = match l with
     | bnd :: l ->
-      let loc = bnd.CAst.loc in
+      let loc = bnd.loc in
       begin match DAst.get bnd with
-      | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
+      | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (make ?loc @@ Ident id, None)) :: extract_variables l
       | GLocalDef (Name id,_,_,_) -> extract_variables l
       | GLocalDef (Anonymous,_,_,_)
       | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.")
@@ -720,7 +720,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
             let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
             match disjpat with
             | [pat] -> (glob_constr_of_cases_pattern pat, None)
-            | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc ()
+            | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc ()
         in
         let terms = Id.Map.map mk_env terms in
         let binders = Id.Map.map mk_env' binders in
@@ -805,7 +805,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 (Ident (loc,id)) | Anonymous -> None in
+  let atom = match na with Name id -> Some (make ?loc @@ Ident id) | Anonymous -> None in
   CAst.make ?loc (CPatAtom atom)
 
 let split_by_type ids subst =
@@ -902,7 +902,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 (Ident (loc,id),None), Some (make ?loc @@ ExplByName id)) expl_impls in
+      (fun id -> CAst.make ?loc @@ CRef (make ?loc @@ Ident 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
@@ -969,14 +969,14 @@ 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,qid) =
+let intern_extended_global_of_qualid {loc;v=qid} =
   let r = Nametab.locate_extended qid in dump_extended_global loc r; r
 
 let intern_reference ref =
   let qid = qualid_of_reference ref in
   let r =
     try intern_extended_global_of_qualid qid
-    with Not_found -> error_global_not_found ?loc:(fst qid) (snd qid)
+    with Not_found -> error_global_not_found qid
   in
   Smartlocate.global_of_extended_global r
 
@@ -993,8 +993,9 @@ let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort =
   | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info]
 
 (* Is it a global reference or a syntactic definition? *)
-let intern_qualid loc qid intern env ntnvars us args =
-  match intern_extended_global_of_qualid (loc,qid) with
+let intern_qualid qid intern env ntnvars us args =
+  let loc = qid.loc in
+  match intern_extended_global_of_qualid qid with
   | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args
   | SynDef sp ->
       let (ids,c) = Syntax_def.search_syntactic_definition sp in
@@ -1007,9 +1008,9 @@ let intern_qualid loc qid intern env ntnvars us args =
       let infos = (Id.Map.empty, env) in
       let projapp = match c with NRef _ -> true | _ -> false in
       let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
-      let loc = c.CAst.loc in
+      let loc = c.loc in
       let err () =
-        user_err ?loc  (str "Notation " ++ pr_qualid qid
+        user_err ?loc  (str "Notation " ++ pr_qualid qid.v
                   ++ str " cannot have a universe instance,"
                   ++ str " its expanded head does not start with a reference")
       in
@@ -1026,40 +1027,41 @@ let intern_qualid loc qid intern env ntnvars us args =
       | Some [s], GSort (Misctypes.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)
+        user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v)
       | Some _, _ -> err ()
       in
       c, projapp, args2
 
 (* Rule out section vars since these should have been found by intern_var *)
-let intern_non_secvar_qualid loc qid intern env ntnvars us args =
-  let c, _, _ as r = intern_qualid loc qid intern env ntnvars us args in
+let intern_non_secvar_qualid qid intern env ntnvars us args =
+  let c, _, _ as r = intern_qualid qid intern env ntnvars us args in
   match DAst.get c with
     | GRef (VarRef _, _) -> raise Not_found
     | _ -> r
 
 let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
 function
-  | Qualid (loc, qid) ->
+  | {loc; v=Qualid qid} ->
+      let qid = make ?loc qid in
       let r,projapp,args2 =
-	try intern_qualid loc qid intern env ntnvars us args
-	with Not_found -> error_global_not_found ?loc qid
+        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
-  | Ident (loc, id) ->
+  | {loc; v=Ident id} ->
       try intern_var env lvar namedctx loc id us, args
       with Not_found ->
-      let qid = qualid_of_ident id in
+      let qid = make ?loc @@ qualid_of_ident id in
       try
-	let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env ntnvars us args in
+        let r, projapp, args2 = intern_non_secvar_qualid 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
-	else error_global_not_found ?loc qid
+        else error_global_not_found qid
 
 let interp_reference vars r =
   let (r,_,_,_),_ =
@@ -1255,8 +1257,8 @@ let find_constructor loc add_params ref =
     | None -> []
 
 let find_pattern_variable = function
-  | Ident (loc,id) -> id
-  | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x))
+  | {v=Ident id} -> id
+  | {loc;v=Qualid _} as x -> raise (InternalizationError(loc,NotAConstructor x))
 
 let check_duplicate loc fields =
   let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in
@@ -1289,7 +1291,7 @@ let sort_fields ~complete loc fields completer =
             let gr = global_reference_of_reference first_field_ref in
             (gr, Recordops.find_projection gr)
           with Not_found ->
-            user_err ?loc:(loc_of_reference first_field_ref) ~hdr:"intern"
+            user_err ?loc ~hdr:"intern"
                          (pr_reference first_field_ref ++ str": Not a projection")
         in
         (* the number of parameters *)
@@ -1297,7 +1299,7 @@ let sort_fields ~complete loc fields completer =
         (* the reference constructor of the record *)
         let base_constructor =
           let global_record_id = ConstructRef record.Recordops.s_CONST in
-          try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id)
+          try make ?loc @@ Qualid (shortest_qualid_of_global Id.Set.empty global_record_id)
           with Not_found ->
             anomaly (str "Environment corruption for records.") in
         let () = check_duplicate loc fields in
@@ -1347,7 +1349,7 @@ let sort_fields ~complete loc fields completer =
             | (field_ref, field_value) :: fields ->
                let field_glob_ref = try global_reference_of_reference field_ref
                with Not_found ->
-                 user_err ?loc:(loc_of_reference field_ref) ~hdr:"intern"
+                 user_err ?loc ~hdr:"intern"
                                (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
                let remaining_projs, (field_index, _) =
                  let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in
@@ -1476,9 +1478,9 @@ let drop_notations_pattern looked_for genv =
     | _ -> 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 (loc,qid) = qualid_of_reference re in
+    let qid = qualid_of_reference re in
     try
-      match locate_extended qid with
+      match locate_extended qid.v with
       | SynDef sp ->
 	let (vars,a) = Syntax_def.search_syntactic_definition sp in
 	(match a with
@@ -1496,16 +1498,16 @@ let drop_notations_pattern looked_for genv =
               (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
 	      test_kind top g;
 	      let nvars = List.length vars in
-	      if List.length pats < nvars then error_not_enough_arguments ?loc;
+              if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc;
 	      let pats1,pats2 = List.chop nvars pats in
 	      let subst = make_subst vars pats1 in
-	      let idspl1 = List.map (in_not false loc scopes (subst, Id.Map.empty) []) args in
+              let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in
 	      let (_,argscs) = find_remaining_scopes pats1 pats2 g in
 	      Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
 	| _ -> raise Not_found)
       | TrueGlobal g ->
 	  test_kind top g;
-	  Dumpglob.add_glob ?loc g;
+          Dumpglob.add_glob ?loc:qid.loc g;
 	  let (_,argscs) = find_remaining_scopes [] pats g in
 	  Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
     with Not_found -> None
@@ -1535,7 +1537,7 @@ let drop_notations_pattern looked_for genv =
 	  | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
      | CPatCstr (r, Some expl_pl, pl) ->
-      let g = try locate (snd (qualid_of_reference r))
+      let g = try locate (qualid_of_reference r).v
 	      with Not_found ->
  	      raise (InternalizationError (loc,NotAConstructor r)) in
       if expl_pl == [] then
diff --git a/interp/declare.ml b/interp/declare.ml
index 7dd73fbb5..c55a6c69b 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -592,15 +592,10 @@ let input_constraints : constraint_decl -> Libobject.obj =
       discharge_function = discharge_constraints;
       classify_function = (fun a -> Keep a) }
 
-let loc_of_glob_level = function
-  | Misctypes.GType (Misctypes.UNamed n) -> Libnames.loc_of_reference n
-  | _ -> None
-
 let do_constraint poly l =
   let u_of_id x =
     let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
-    let loc = loc_of_glob_level x in
-    loc, Universes.is_polymorphic level, level
+    Universes.is_polymorphic level, level
   in
   let in_section = Lib.sections_are_opened () in
   let () =
@@ -608,18 +603,17 @@ let do_constraint poly l =
       user_err ~hdr:"Constraint"
                     (str"Cannot declare polymorphic constraints outside sections")
   in
-  let check_poly ?loc p loc' p' =
+  let check_poly p p' =
     if poly then ()
     else if p || p' then
-      let loc = if p then loc else loc' in
-      user_err ?loc ~hdr:"Constraint"
+      user_err ~hdr:"Constraint"
                     (str "Cannot declare a global constraint on " ++
                     str "a polymorphic universe, use "
                     ++ str "Polymorphic Constraint instead")
   in
   let constraints = List.fold_left (fun acc (l, d, r) ->
-     let ploc, p, lu = u_of_id l and rloc, p', ru = u_of_id r in
-     check_poly ?loc:ploc p rloc p';
+     let p, lu = u_of_id l and p', ru = u_of_id r in
+     check_poly p p';
      Univ.Constraint.add (lu, d, ru) acc)
     Univ.Constraint.empty l
   in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 7d919ec0c..a1a3be70f 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -94,8 +94,8 @@ 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 (Ident (loc,id),_) -> found loc id bdvars l
-    | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) ->
+    | 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
     | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
   in aux bound l c
@@ -194,7 +194,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 (Ident (Loc.tag id'),None), Id.Set.add id' avoid)
+      (CAst.make @@ CRef (CAst.make @@ Ident id',None), Id.Set.add id' avoid)
 
 let destClassApp cl =
   let open CAst in
@@ -202,7 +202,7 @@ let destClassApp cl =
   match cl.v with
     | CApp ((None, { v = CRef (ref, inst) }), l) -> CAst.make ?loc (ref, List.map fst l, inst)
     | CAppExpl ((None, ref, inst), l) -> CAst.make ?loc (ref, l, inst)
-    | CRef (ref, inst) -> CAst.make ?loc:(loc_of_reference ref) (ref, [], inst)
+    | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst)
     | _ -> raise Not_found
 
 let destClassAppExpl cl =
@@ -210,15 +210,15 @@ let destClassAppExpl cl =
   let loc = cl.loc in
   match cl.v with
     | CApp ((None, { v = CRef (ref, inst) } ), l) -> CAst.make ?loc (ref, l, inst)
-    | CRef (ref, inst) -> CAst.make ?loc:(loc_of_reference ref) (ref, [], inst)
+    | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst)
     | _ -> raise Not_found
 
 let implicit_application env ?(allow_partial=true) f ty =
   let is_class =
     try
       let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in
-      let (loc, qid) = qualid_of_reference r in
-      let gr = Nametab.locate qid in
+      let qid = qualid_of_reference r in
+      let gr = Nametab.locate qid.CAst.v in
 	if Typeclasses.is_class gr then Some (clapp, gr) else None
     with Not_found -> None
   in
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 6033d509b..1f4a93a6f 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -42,42 +42,38 @@ let global_of_extended_global = function
   | [],NApp (NRef ref,[]) -> ref
   | _ -> raise Not_found
 
-let locate_global_with_alias ?(head=false) (loc,qid) =
+let locate_global_with_alias ?(head=false) {CAst.loc; v=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 (pr_qualid qid ++
       str " is bound to a notation that does not denote a reference.")
 
-let global_inductive_with_alias r =
-  let (loc,qid as lqid) = qualid_of_reference r in
-  try match locate_global_with_alias lqid with
+let global_inductive_with_alias ({CAst.loc} as lr)  =
+  let qid = qualid_of_reference lr in
+  try match locate_global_with_alias qid with
   | IndRef ind -> ind
   | ref ->
-      user_err ?loc:(loc_of_reference r) ~hdr:"global_inductive"
-        (pr_reference r ++ spc () ++ str "is not an inductive type.")
-  with Not_found -> Nametab.error_global_not_found ?loc qid
+      user_err ?loc ~hdr:"global_inductive"
+        (pr_reference lr ++ spc () ++ str "is not an inductive type.")
+  with Not_found -> Nametab.error_global_not_found qid
 
 let global_with_alias ?head r =
-  let (loc,qid as lqid) = qualid_of_reference r in
-  try locate_global_with_alias ?head lqid
-  with Not_found -> Nametab.error_global_not_found ?loc qid
+  let qid = qualid_of_reference r in
+  try locate_global_with_alias ?head qid
+  with Not_found -> Nametab.error_global_not_found qid
 
-let smart_global ?head = function
+let smart_global ?head = CAst.with_loc_val (fun ?loc -> function
   | AN r ->
-      global_with_alias ?head r
-  | ByNotation {CAst.loc;v=(ntn,sc)} ->
-      Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc
+    global_with_alias ?head r
+  | ByNotation (ntn,sc) ->
+    Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)
 
-let smart_global_inductive = function
+let smart_global_inductive = CAst.with_loc_val (fun ?loc -> function
   | AN r ->
-      global_inductive_with_alias r
-  | ByNotation {CAst.loc;v=(ntn,sc)} ->
-      destIndRef
-        (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc)
-
-let loc_of_smart_reference = function
-  | AN r -> loc_of_reference r
-  | ByNotation {CAst.loc;v=(_,_)} -> loc
+    global_inductive_with_alias r
+  | ByNotation (ntn,sc) ->
+    destIndRef
+      (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc))
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 112301251..7ff7e899e 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Loc
 open Names
 open Libnames
 open Globnames
@@ -19,7 +18,7 @@ open Misctypes
    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 located -> global_reference
+val locate_global_with_alias : ?head:bool -> qualid CAst.t -> global_reference
 
 (** Extract a global_reference from a reference that can be an "alias" *)
 val global_of_extended_global : extended_global_reference -> global_reference
@@ -38,6 +37,3 @@ val smart_global : ?head:bool -> reference or_by_notation -> global_reference
 
 (** The same for inductive types *)
 val smart_global_inductive : reference or_by_notation -> inductive
-
-(** Return the loc of a smart reference *)
-val loc_of_smart_reference : reference or_by_notation -> Loc.t option
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 0958cc7ee..e5ed58be6 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Misctypes
 open Genarg
 open Geninterp
 
@@ -32,10 +31,6 @@ let wit_string : string uniform_genarg_type =
 let wit_pre_ident : string uniform_genarg_type =
   make0 "preident"
 
-let loc_of_or_by_notation f = function
-  | AN c -> f c
-  | ByNotation {CAst.loc;v=(s,_)} -> loc
-
 let wit_int_or_var =
   make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
 
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index b69129956..53d1a522d 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -22,9 +22,6 @@ open Misctypes
 open Tactypes
 open Genarg
 
-(** FIXME: nothing to do there. *)
-val loc_of_or_by_notation : ('a -> Loc.t option) -> 'a or_by_notation -> Loc.t option
-
 val wit_unit : unit uniform_genarg_type
 
 val wit_bool : bool uniform_genarg_type