[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.

17 files changed, 90 insertions, 99 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index a4e8c44cd..397cb2920 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -597,8 +597,8 @@ let warns () =
 let rec locate_ref = function
   | [] -> [],[]
   | r::l ->
-      let q = snd (qualid_of_reference r) in
-      let mpo = try Some (Nametab.locate_module q) with Not_found -> None
+      let q = qualid_of_reference r in
+      let mpo = try Some (Nametab.locate_module q.CAst.v) with Not_found -> None
       and ro =
         try Some (Smartlocate.global_with_alias r)
         with Nametab.GlobalizationError _ | UserError _ -> None
@@ -608,7 +608,7 @@ let rec locate_ref = function
 	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
 	| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
 	| Some mp, Some r ->
-           warning_ambiguous_name (q,mp,r);
+           warning_ambiguous_name (q.CAst.v,mp,r);
            let refs,mps = locate_ref l in refs,mp::mps
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
@@ -646,7 +646,7 @@ let separate_extraction lr =
     is \verb!Extraction! [qualid]. *)
 
 let simple_extraction r =
-  Vernacentries.dump_global (Misctypes.AN r);
+  Vernacentries.dump_global CAst.(make (Misctypes.AN r));
   match locate_ref [r] with
   | ([], [mp]) as p -> full_extr None p
   | [r],[] ->
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 6c421491f..54c6d9d72 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -899,7 +899,7 @@ let extract_constant_inline inline r ids s =
 let extract_inductive r s l optstr =
   check_inside_section ();
   let g = Smartlocate.global_with_alias r in
-  Dumpglob.add_glob ?loc:(loc_of_reference r) g;
+  Dumpglob.add_glob ?loc:r.CAst.loc g;
   match g with
     | IndRef ((kn,i) as ip) ->
 	let mib = Global.lookup_mind kn in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 1c27b27e2..b65d9867d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -356,7 +356,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	(*i The next call to mk_rel_id is valid since we have just construct the graph
 	   Ensures by : do_built
 	i*)
-	let f_R_mut = Ident (Loc.tag @@ mk_rel_id (List.nth names 0)) in
+        let f_R_mut = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in
 	let ind_kn =
 	  fst (locate_with_msg
 		 (pr_reference f_R_mut++str ": Not an inductive type!")
@@ -364,7 +364,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 		 f_R_mut)
 	in
 	let fname_kn (((fname,_),_,_,_,_),_) =
-          let f_ref = Ident CAst.(with_loc_val (fun ?loc n -> (loc,n)) fname) in
+          let f_ref = CAst.map (fun n -> Ident n) fname in
 	  locate_with_msg
 	    (pr_reference f_ref++str ": Not an inductive type!")
 	    locate_constant
@@ -472,7 +472,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
   let unbounded_eq =
     let f_app_args =
       CAst.make @@ Constrexpr.CAppExpl(
-	 (None,(Ident (Loc.tag fname)),None) ,
+         (None,CAst.make @@ Ident fname,None) ,
 	 (List.map
 	    (function
                | {CAst.v=Anonymous} -> assert false
@@ -482,7 +482,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	 )
 	)
     in
-    CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))),
+    CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))),
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
@@ -539,7 +539,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
       | None ->
 	  let ltof =
 	    let make_dir l = DirPath.make (List.rev_map Id.of_string l) in
-	    Libnames.Qualid (Loc.tag @@ Libnames.qualid_of_path
+            CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path
 			       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")))
 	  in
 	  let fun_from_mes =
@@ -724,7 +724,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 let rec add_args id new_args = CAst.map (function
   | CRef (r,_) as b ->
       begin match r with
-	| Libnames.Ident(loc,fname) when Id.equal fname id ->
+        | {CAst.v=Libnames.Ident fname} when Id.equal fname id ->
 	    CAppExpl((None,r,None),new_args)
 	| _ -> b
       end
@@ -744,7 +744,7 @@ let rec add_args id new_args = CAst.map (function
   | CAppExpl((pf,r,us),exprl) ->
       begin
 	match r with
-	| Libnames.Ident(loc,fname) when Id.equal fname id ->
+        | {CAst.v=Libnames.Ident fname} when Id.equal fname id ->
 	    CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl))
 	| _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl)
       end
@@ -883,7 +883,7 @@ let make_graph (f_ref:global_reference) =
 				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
                                         (fun {CAst.loc;v=n} -> CAst.make ?loc @@
-					   CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None))
+                                           CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None))
 					nal
                                   | Constrexpr.CLocalPattern _ -> assert false
 			       )
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index d6fd2f2a0..a0b9217c7 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -32,7 +32,7 @@ let id_of_name = function
   | _ -> raise Not_found
 
 let locate  ref =
-    let (loc,qid) = qualid_of_reference ref in
+    let {CAst.v=qid} = qualid_of_reference ref in
     Nametab.locate qid
 
 let locate_ind ref =
@@ -100,13 +100,8 @@ let list_union_eq eq_fun l1 l2 =
 let list_add_set_eq eq_fun x l =
   if List.exists (eq_fun x) l then l else x::l
 
-
-
-
 let const_of_id id =
-  let _,princ_ref =
-    qualid_of_reference (Libnames.Ident (Loc.tag id))
-  in
+  let princ_ref = qualid_of_ident id in
   try Constrintern.locate_reference princ_ref
   with Not_found ->
     CErrors.user_err ~hdr:"IndFun.const_of_id"
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 4cbcde8e5..fb9ae64bf 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1325,7 +1325,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
     CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
   let hook _ _ =
     let opacity =
-      let na_ref = Libnames.Ident (Loc.tag na) in
+      let na_ref = CAst.make @@ Libnames.Ident na in
       let na_global = Smartlocate.global_with_alias na_ref in
       match na_global with
 	  ConstRef c -> is_opaque_constant c
@@ -1579,7 +1579,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let hook _ _ = 
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
-    let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.tag term_id)] in
+    let _ = Extraction_plugin.Table.extraction_inline true [CAst.make @@ Ident term_id] in
     (*     message "start second proof"; *)
     let stop = 
       try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 1909cd96f..0c42a8bb2 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -38,11 +38,11 @@ let genarg_of_ipattern pat = in_gen (rawwit Stdarg.wit_intro_pattern) pat
 let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
 let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
 
-let reference_to_id = function
-  | Libnames.Ident (loc, id) -> CAst.make ?loc id
-  | Libnames.Qualid (loc,_) ->
+let reference_to_id = CAst.map_with_loc (fun ?loc -> function
+  | Libnames.Ident id -> id
+  | Libnames.Qualid _ ->
     CErrors.user_err ?loc
-      (str "This expression should be a simple identifier.")
+      (str "This expression should be a simple identifier."))
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
 
@@ -473,7 +473,7 @@ END
 
 VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
 | [ "Print" "Ltac" reference(r) ] ->
-  [ Feedback.msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
+  [ Feedback.msg_notice (Tacintern.print_ltac (Libnames.qualid_of_reference r).CAst.v) ]
 END
 
 VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
@@ -508,8 +508,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
 | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [
     VtSideff (List.map (function
       | TacticDefinition ({CAst.v=r},_) -> r
-      | TacticRedefinition (Ident (_,r),_) -> r
-      | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
+      | TacticRedefinition ({CAst.v=Ident r},_) -> r
+      | TacticRedefinition ({CAst.v=Qualid q},_) -> snd(repr_qualid q)) l), VtLater
   ] -> [ fun ~atts ~st -> let open Vernacinterp in
            Tacentries.register_ltac (Locality.make_module_locality atts.locality) l;
            st
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 54e2ba960..352e92c2a 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -49,7 +49,7 @@ module Tactic = Pltac
 
 open Pcoq
 
-let sigref = mkRefC (Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Init.Specif.sig"))
+let sigref = mkRefC (CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Init.Specif.sig"))
 
 type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
 
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 7643cc97d..7534e2799 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -154,8 +154,7 @@ let mkTacCase with_evar = function
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
   | [(clear,ElimOnIdent id),(None,None),None],None ->
-    let id = CAst.(id.loc, id.v) in
-      TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings)))
+      TacCase (with_evar,(clear,(CAst.make @@ CRef (CAst.make ?loc:id.CAst.loc @@ Ident id.CAst.v,None),NoBindings)))
   | ic ->
       if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
       then
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index a42994652..5d262ffcb 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -181,9 +181,9 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let pr_and_short_name pr (c,_) = pr c
 
-  let pr_or_by_notation f = function
+  let pr_or_by_notation f = CAst.with_val (function
     | AN v -> f v
-    | ByNotation {CAst.v=(s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+    | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc)
 
   let pr_located pr (loc,x) = pr x
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e0368153e..d32a2faef 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1773,12 +1773,11 @@ let rec strategy_of_ast = function
 
 (* By default the strategy for "rewrite_db" is top-down *)
 
-let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l)
+let mkappc s l = CAst.make @@ CAppExpl ((None,CAst.make @@ Libnames.Ident (Id.of_string s),None),l)
 
 let declare_an_instance n s args =
   (((CAst.make @@ Name n),None), Explicit,
-  CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@  qualid_of_string s),None),
-	   args))
+   CAst.make @@ CAppExpl ((None, CAst.make @@ Qualid (qualid_of_string s),None), args))
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
@@ -1792,17 +1791,17 @@ let anew_instance global binders instance fields =
 let declare_instance_refl global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
   in anew_instance global binders instance
-       [(Ident (Loc.tag @@ Id.of_string "reflexivity"),lemma)]
+       [(CAst.make @@ Ident (Id.of_string "reflexivity"),lemma)]
 
 let declare_instance_sym global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
   in anew_instance global binders instance
-       [(Ident (Loc.tag @@ Id.of_string "symmetry"),lemma)]
+       [(CAst.make @@ Ident (Id.of_string "symmetry"),lemma)]
 
 let declare_instance_trans global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
   in anew_instance global binders instance
-       [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)]
+       [(CAst.make @@ Ident (Id.of_string "transitivity"),lemma)]
 
 let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
@@ -1826,16 +1825,16 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
 	in ignore(
 	    anew_instance global binders instance
-	      [(Ident (Loc.tag @@ Id.of_string "PreOrder_Reflexive"), lemma1);
-	       (Ident (Loc.tag @@ Id.of_string "PreOrder_Transitive"),lemma3)])
+              [(CAst.make @@ Ident (Id.of_string "PreOrder_Reflexive"), lemma1);
+               (CAst.make @@ Ident (Id.of_string "PreOrder_Transitive"),lemma3)])
     | (None, Some lemma2, Some lemma3) ->
 	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
 	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
 	in ignore(
 	    anew_instance global binders instance
-	      [(Ident (Loc.tag @@ Id.of_string "PER_Symmetric"), lemma2);
-	       (Ident (Loc.tag @@ Id.of_string "PER_Transitive"),lemma3)])
+              [(CAst.make @@ Ident (Id.of_string "PER_Symmetric"), lemma2);
+               (CAst.make @@ Ident (Id.of_string "PER_Transitive"),lemma3)])
      | (Some lemma1, Some lemma2, Some lemma3) ->
 	let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
 	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
@@ -1843,9 +1842,9 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
 	in ignore(
 	  anew_instance global binders instance
-	    [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), lemma1);
-	     (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), lemma2);
-	     (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), lemma3)])
+            [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), lemma1);
+             (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2);
+             (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)])
 
 let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None)
 
@@ -1951,16 +1950,16 @@ let add_setoid global binders a aeq t n =
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in ignore(
     anew_instance global binders instance
-      [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
-       (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
-       (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
+      [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+       (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+       (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
 
 
 let make_tactic name =
   let open Tacexpr in
   let tacpath = Libnames.qualid_of_string name in
-  let tacname = Qualid (Loc.tag tacpath) in
-  TacArg (Loc.tag @@ TacCall (Loc.tag (tacname, [])))
+  let tacname = CAst.make @@ Qualid tacpath in
+  TacArg (Loc.tag @@ (TacCall (Loc.tag (tacname, []))))
 
 let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
@@ -2010,7 +2009,7 @@ let add_morphism glob binders m s n =
   let instance =
     (((CAst.make @@ Name instance_id),None), Explicit,
     CAst.make @@ CAppExpl (
-	     (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
+             (None, CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 566fc2873..e510b9f59 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -450,11 +450,10 @@ let register_ltac local tacl =
         let () = if is_shadowed then warn_unusable_identifier id in
         NewTac id, body
     | Tacexpr.TacticRedefinition (ident, body) ->
-        let loc = loc_of_reference ident in
         let kn =
-          try Tacenv.locate_tactic (snd (qualid_of_reference ident))
+          try Tacenv.locate_tactic (qualid_of_reference ident).CAst.v
           with Not_found ->
-            CErrors.user_err ?loc 
+            CErrors.user_err ?loc:ident.CAst.loc
                        (str "There is no Ltac named " ++ pr_reference ident ++ str ".")
         in
         UpdateTac kn, body
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 45f4a45fc..9ad9e1520 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -92,15 +92,15 @@ let intern_int_or_var = intern_or_var (fun (n : int) -> n)
 let intern_string_or_var = intern_or_var (fun (s : string) -> s)
 
 let intern_global_reference ist = function
-  | Ident (loc,id) when find_var id ist ->
+  | {CAst.loc;v=Ident id} when find_var id ist ->
     ArgVar (make ?loc id)
   | r ->
-      let loc,_ as lqid = qualid_of_reference r in
-      try ArgArg (loc,locate_global_with_alias lqid)
-      with Not_found -> error_global_not_found (snd lqid)
+    let {CAst.loc} as lqid = qualid_of_reference r in
+    try ArgArg (loc,locate_global_with_alias lqid)
+    with Not_found -> error_global_not_found lqid
 
 let intern_ltac_variable ist = function
-  | Ident (loc,id) ->
+  | {loc;v=Ident id} ->
       if find_var id ist then
 	(* A local variable of any type *)
         ArgVar (make ?loc id)
@@ -109,19 +109,19 @@ let intern_ltac_variable ist = function
       raise Not_found
 
 let intern_constr_reference strict ist = function
-  | Ident (_,id) as r when not strict && find_hyp id ist ->
+  | {v=Ident id} as r when not strict && find_hyp id ist ->
       (DAst.make @@ GVar id), Some (make @@ CRef (r,None))
-  | Ident (_,id) as r when find_var id ist ->
+  | {v=Ident id} as r when find_var id ist ->
       (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (r,None))
   | r ->
-      let loc,_ as lqid = qualid_of_reference r in
+      let {loc} as lqid = qualid_of_reference r in
       DAst.make @@ GRef (locate_global_with_alias lqid,None), 
         if strict then None else Some (make @@ CRef (r,None))
 
 (* Internalize an isolated reference in position of tactic *)
 
 let intern_isolated_global_tactic_reference r =
-  let (loc,qid) = qualid_of_reference r in
+  let {loc;v=qid} = qualid_of_reference r in
   TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[]))
 
 let intern_isolated_tactic_reference strict ist r =
@@ -135,12 +135,12 @@ let intern_isolated_tactic_reference strict ist r =
   try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
   with Not_found ->
   (* Reference not found *)
-  error_global_not_found (snd (qualid_of_reference r))
+  error_global_not_found (qualid_of_reference r)
 
 (* Internalize an applied tactic reference *)
 
 let intern_applied_global_tactic_reference r =
-  let (loc,qid) = qualid_of_reference r in
+  let {loc;v=qid} = qualid_of_reference r in
   ArgArg (loc,Tacenv.locate_tactic qid)
 
 let intern_applied_tactic_reference ist r =
@@ -151,7 +151,7 @@ let intern_applied_tactic_reference ist r =
   try intern_applied_global_tactic_reference r
   with Not_found ->
   (* Reference not found *)
-  error_global_not_found (snd (qualid_of_reference r))
+  error_global_not_found (qualid_of_reference r)
 
 (* Intern a reference parsed in a non-tactic entry *)
 
@@ -167,12 +167,12 @@ let intern_non_tactic_reference strict ist r =
   with Not_found ->
   (* By convention, use IntroIdentifier for unbound ident, when not in a def *)
   match r with
-  | Ident (loc,id) when not strict ->
+  | {loc;v=Ident id} when not strict ->
     let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in
     TacGeneric ipat
   | _ ->
   (* Reference not found *)
-  error_global_not_found (snd (qualid_of_reference r))
+  error_global_not_found (qualid_of_reference r)
 
 let intern_message_token ist = function
   | (MsgString _ | MsgInt _ as x) -> x
@@ -268,7 +268,7 @@ let intern_destruction_arg ist = function
   | clear,ElimOnIdent {loc;v=id} ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
-        let c, p = intern_constr ist (make @@ CRef (Ident (Loc.tag id), None)) in
+        let c, p = intern_constr ist (make @@ CRef (make @@ Ident id, None)) in
 	match DAst.get c with
         | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id)
 	| _ -> clear,ElimOnConstr ((c, p), NoBindings)
@@ -276,7 +276,7 @@ let intern_destruction_arg ist = function
         clear,ElimOnIdent (make ?loc id)
 
 let short_name = function
-  | AN (Ident (loc,id)) when not !strict_check -> Some (make ?loc id)
+  | {v=AN {loc;v=Ident id}} when not !strict_check -> Some (make ?loc id)
   | _ -> None
 
 let intern_evaluable_global_reference ist r =
@@ -284,20 +284,20 @@ let intern_evaluable_global_reference ist r =
   try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true lqid)
   with Not_found ->
   match r with
-  | Ident (loc,id) when not !strict_check -> EvalVarRef id
-  | _ -> error_global_not_found (snd lqid)
+  | {loc;v=Ident id} when not !strict_check -> EvalVarRef id
+  | _ -> error_global_not_found lqid
 
 let intern_evaluable_reference_or_by_notation ist = function
-  | AN r -> intern_evaluable_global_reference ist r
-  | ByNotation {loc;v=(ntn,sc)} ->
+  | {v=AN r} -> intern_evaluable_global_reference ist r
+  | {v=ByNotation (ntn,sc);loc} ->
       evaluable_of_global_reference ist.genv
       (Notation.interp_notation_as_global_reference ?loc
         (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
 
 (* Globalize a reduction expression *)
 let intern_evaluable ist = function
-  | AN (Ident (loc,id)) when find_var id ist -> ArgVar (make ?loc id)
-  | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist ->
+  | {loc;v=AN {v=Ident id}} when find_var id ist -> ArgVar (make ?loc id)
+  | {loc;v=AN {v=Ident id}} when not !strict_check && find_hyp id ist ->
       ArgArg (EvalVarRef id, Some (make ?loc id))
   | r ->
       let e = intern_evaluable_reference_or_by_notation ist r in
@@ -353,10 +353,9 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
          ref or a pattern seems interesting, with "head" reduction
          in case of an evaluable ref, and "strong" reduction in the
          subterm matched when a pattern *)
-      let loc = loc_of_smart_reference r in
       let r = match r with
-      | AN r -> r
-      | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in
+      | {v=AN r} -> r
+      | {loc} -> make ?loc @@ Qualid (qualid_of_path (path_of_global (smart_global r))) in
       let sign = {
         Constrintern.ltac_vars = ist.ltacvars;
         ltac_bound = Id.Set.empty;
@@ -376,7 +375,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
   | Inl r -> interp_ref r
   | Inr { v = CAppExpl((None,r,None),[]) } ->
       (* We interpret similarly @ref and ref *)
-      interp_ref (AN r)
+      interp_ref (make @@ AN r)
   | Inr c ->
       Inr (snd (intern_typed_pattern ist ~as_type:false ~ltacvars:ist.ltacvars c)))
 
@@ -385,13 +384,13 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
 let dump_glob_red_expr = function
   | Unfold occs -> List.iter (fun (_, r) ->
     try
-      Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r)
+      Dumpglob.add_glob ?loc:r.loc
 	(Smartlocate.smart_global r)
     with e when CErrors.noncritical e -> ()) occs
   | Cbv grf | Lazy grf ->
     List.iter (fun r ->
       try
-        Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r)
+        Dumpglob.add_glob ?loc:r.loc
 	  (Smartlocate.smart_global r)
       with e when CErrors.noncritical e -> ()) grf.rConst
   | _ -> ()
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a287b13b9..6a4bf577b 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -360,7 +360,7 @@ let interp_reference ist env sigma = function
     with Not_found ->
       try
         VarRef (get_id (Environ.lookup_named id env))
-      with Not_found -> error_global_not_found ?loc (qualid_of_ident id)
+      with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id)
 
 let try_interp_evaluable env (loc, id) =
   let v = Environ.lookup_named id env in
@@ -376,14 +376,14 @@ let interp_evaluable ist env sigma = function
       with Not_found ->
         match r with
         | EvalConstRef _ -> r
-        | _ -> error_global_not_found ?loc (qualid_of_ident id)
+        | _ -> error_global_not_found (make ?loc @@ qualid_of_ident id)
     end
   | ArgArg (r,None) -> r
   | ArgVar {loc;v=id} ->
     try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id)
     with Not_found ->
       try try_interp_evaluable env (loc, id)
-      with Not_found -> error_global_not_found ?loc (qualid_of_ident id)
+      with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id)
 
 (* Interprets an hypothesis name *)
 let interp_occurrences ist occs =
@@ -642,7 +642,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
         Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
     (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id)
      with Not_found ->
-       error_global_not_found ?loc (qualid_of_ident id))
+       error_global_not_found (make ?loc @@ qualid_of_ident id))
   | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
   | Inr c -> Inr (interp_typed_pattern ist env sigma c) in
   interp_occurrences ist occs, p
@@ -926,7 +926,7 @@ let interp_destruction_arg ist gl arg =
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (make ?loc id)
 	else
-          let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (Ident (loc,id),None))) in
+          let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (make ?loc @@ Ident id,None))) in
           let f env sigma =
             let (sigma,c) = interp_open_constr ist env sigma c in
             (sigma, (c,NoBindings))
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index f049963f1..19abf6780 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -853,7 +853,7 @@ open Util
 (** Constructors for constr_expr *)
 let mkCProp loc = CAst.make ?loc @@ CSort GProp
 let mkCType loc = CAst.make ?loc @@ CSort (GType [])
-let mkCVar ?loc id = CAst.make ?loc @@ CRef (Ident (Loc.tag ?loc id), None)
+let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None)
 let rec mkCHoles ?loc n =
   if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
 let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 2f8b8cb02..0d82a9f09 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1165,7 +1165,7 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar
 END
 
 let bvar_lname = let open CAst in function
-  | { v = CRef (Ident (loc, id), _) } -> CAst.make ?loc @@ Name id
+  | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id
   | { loc = loc } -> CAst.make ?loc Anonymous
 
 let pr_ssrbinder prc _ _ (_, c) = prc c
@@ -1257,7 +1257,7 @@ END
 let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd
 
 let bvar_locid = function
-  | { CAst.v = CRef (Ident (loc, id), _) } -> CAst.make ?loc id
+  | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id
   | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"")
 
 
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index c3b6a7c59..05dbf0a86 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -432,7 +432,7 @@ END
 
 let interp_modloc mr =
   let interp_mod (_, mr) =
-    let (loc, qid) = qualid_of_reference mr in
+    let {CAst.loc=loc; v=qid} = qualid_of_reference mr in
     try Nametab.full_name_module qid with Not_found ->
     CErrors.user_err ?loc (str "No Module " ++ pr_qualid qid) in
   let mr_out, mr_in = List.partition fst mr in
@@ -565,9 +565,9 @@ GEXTEND Gram
   gallina_ext:
       (* Canonical structure *)
      [[ IDENT "Canonical"; qid = Constr.global ->
-	  Vernacexpr.VernacCanonical (AN qid)
+          Vernacexpr.VernacCanonical (CAst.make @@ AN qid)
       | IDENT "Canonical"; ntn = Prim.by_notation ->
-	  Vernacexpr.VernacCanonical (ByNotation ntn)
+          Vernacexpr.VernacCanonical (CAst.make @@ ByNotation ntn)
       | IDENT "Canonical"; qid = Constr.global;
           d = G_vernac.def_body ->
           let s = coerce_reference_to_id qid in
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 33b18001c..6a1be9db0 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -131,8 +131,8 @@ let add_genarg tag pr =
 (** Constructors for cast type *)
 let dC t = CastConv t
 (** Constructors for constr_expr *)
-let isCVar   = function { CAst.v = CRef (Ident _, _) } -> true | _ -> false
-let destCVar = function { CAst.v = CRef (Ident (_, id), _) } -> id | _ ->
+let isCVar   = function { CAst.v = CRef ({CAst.v=Ident _},_) } -> true | _ -> false
+let destCVar = function { CAst.v = CRef ({CAst.v=Ident id},_) } -> id | _ ->
   CErrors.anomaly (str"not a CRef.")
 let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false
 let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c)
@@ -1012,8 +1012,8 @@ type pattern = Evd.evar_map * (constr, constr) ssrpattern
 let id_of_cpattern (_, (c1, c2), _) =
   let open CAst in
   match DAst.get c1, c2 with
-  | _, Some { v = CRef (Ident (_, x), _) } -> Some x
-  | _, Some { v = CAppExpl ((_, Ident (_, x), _), []) } -> Some x
+  | _, Some { v = CRef ({CAst.v=Ident x}, _) } -> Some x
+  | _, Some { v = CAppExpl ((_, {CAst.v=Ident x}, _), []) } -> Some x
   | GRef (VarRef x, _), None -> Some x
   | _ -> None
 let id_of_Cterm t = match id_of_cpattern t with