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

4 files changed, 20 insertions, 19 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 8854ff898..412a1cbb4 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -213,9 +213,9 @@ let tag_var = tag Tag.variable
   let pr_universe_instance l =
     pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l
 
-  let pr_reference = function
-  | Qualid (_, qid) -> pr_qualid qid
-  | Ident (_, id) -> tag_var (pr_id id)
+  let pr_reference = CAst.with_val (function
+  | Qualid qid -> pr_qualid qid
+  | Ident id -> tag_var (pr_id id))
 
   let pr_cref ref us =
     pr_reference ref ++ pr_universe_instance us
@@ -565,8 +565,8 @@ let tag_var = tag Tag.variable
           return (p ++ prlist (pr spc (lapp,L)) l2, lapp)
         else
           return (p, lproj)
-      | CAppExpl ((None,Ident (_,var),us),[t])
-      | CApp ((_, {CAst.v = CRef(Ident(_,var),us)}),[t,None])
+      | CAppExpl ((None,{v=Ident var},us),[t])
+      | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None])
           when Id.equal var Notation_ops.ldots_var ->
         return (
           hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."),
diff --git a/printing/pputils.ml b/printing/pputils.ml
index c2846c4cd..c14aa318e 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -123,8 +123,8 @@ let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
   pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma)
 
 let pr_or_by_notation f = function
-  | AN v -> f v
-  | ByNotation {CAst.v=(s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+  | {CAst.loc; v=AN v} -> f v
+  | {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
 let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index cfc5e6b4e..1f17d844f 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -15,6 +15,7 @@
 open Pp
 open CErrors
 open Util
+open CAst
 open Names
 open Nameops
 open Termops
@@ -343,7 +344,7 @@ let register_locatable name f =
 exception ObjFound of logical_name
 
 let locate_any_name ref =
-  let (loc,qid) = qualid_of_reference ref in
+  let {v=qid} = qualid_of_reference ref in
   try Term (Nametab.locate qid)
   with Not_found ->
   try Syntactic (Nametab.locate_syndef qid)
@@ -452,7 +453,7 @@ type locatable_kind =
 | LocAny
 
 let print_located_qualid name flags ref =
-  let (loc,qid) = qualid_of_reference ref in
+  let {v=qid} = qualid_of_reference ref in
   let located = match flags with
   | LocTerm -> locate_term qid
   | LocModule -> locate_modtype qid @ locate_module qid
@@ -784,11 +785,11 @@ let print_full_pure_context env sigma =
 
 (* This is designed to print the contents of an opened section *)
 let read_sec_context r =
-  let loc,qid = qualid_of_reference r in
+  let qid = qualid_of_reference r in
   let dir =
-    try Nametab.locate_section qid
+    try Nametab.locate_section qid.v
     with Not_found ->
-      user_err ?loc ~hdr:"read_sec_context" (str "Unknown section.") in
+      user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in
   let rec get_cxt in_cxt = function
     | (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest ->
         if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
@@ -838,12 +839,12 @@ let print_any_name env sigma na udecl =
 
 let print_name env sigma na udecl =
   match na with
-  | ByNotation {CAst.loc;v=(ntn,sc)} ->
+  | {loc; v=ByNotation (ntn,sc)} ->
       print_any_name env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc))
         udecl
-  | AN ref ->
+  | {loc; v=AN ref} ->
       print_any_name env sigma (locate_any_name ref) udecl
 
 let print_opaque_name env sigma qid =
@@ -891,12 +892,12 @@ let print_about_any ?loc env sigma k udecl =
 
 let print_about env sigma na udecl =
   match na with
-  | ByNotation {CAst.loc;v=(ntn,sc)} ->
+  | {loc;v=ByNotation (ntn,sc)} ->
       print_about_any ?loc env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc)) udecl
-  | AN ref ->
-      print_about_any ?loc:(loc_of_reference ref) env sigma (locate_any_name ref) udecl
+  | {loc;v=AN ref} ->
+      print_about_any ?loc env sigma (locate_any_name ref) udecl
 
 (* for debug *)
 let inspect env sigma depth =
diff --git a/printing/printer.ml b/printing/printer.ml
index e50d302b3..199aa79c6 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -235,9 +235,9 @@ let qualid_of_global env r =
 let safe_gen f env sigma c =
   let orig_extern_ref = Constrextern.get_extern_reference () in
   let extern_ref ?loc vars r =
-    try orig_extern_ref ?loc vars r
+    try orig_extern_ref vars r
     with e when CErrors.noncritical e ->
-      Libnames.Qualid (Loc.tag ?loc @@ qualid_of_global env r)
+      CAst.make ?loc @@ Libnames.Qualid (qualid_of_global env r)
   in
   Constrextern.set_extern_reference extern_ref;
   try