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

1 files changed, 20 insertions, 24 deletions

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))