Merge PR #6837: [located] Push inner locations in reference to a CAst.t node.

5 files changed, 13 insertions, 13 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index c0ead3a0a8..5f63d21c4d 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -312,7 +312,7 @@ let interp_entry forpat e = match e with
 
 let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with
   | Anonymous -> CPatAtom None
-  | Name id   -> CPatAtom (Some (Ident (Loc.tag ?loc id)))
+  | Name id   -> CPatAtom (Some (CAst.make ?loc @@ Ident id))
 
 type 'r env = {
   constrs : 'r list;
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index b4f09ee6a1..9c2806bead 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -200,11 +200,11 @@ GEXTEND Gram
       | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),args)
       | "@"; lid = pattern_identref; args=LIST1 identref ->
           let { CAst.loc = locid; v = id } = lid in
-          let args = List.map (fun x -> CAst.make @@ CRef (Ident Loc.(tag ?loc:x.CAst.loc x.CAst.v), None), None) args in
+          let args = List.map (fun x -> CAst.make @@ CRef (CAst.make ?loc:x.CAst.loc @@ Ident x.CAst.v, None), None) args in
           CAst.make ~loc:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ]
     | "9"
         [ ".."; c = operconstr LEVEL "0"; ".." ->
-          CAst.make ~loc:!@loc @@ CAppExpl ((None, Ident (Loc.tag ~loc:!@loc ldots_var),None),[c]) ]
+          CAst.make ~loc:!@loc @@ CAppExpl ((None, CAst.make ~loc:!@loc @@ Ident ldots_var, None),[c]) ]
     | "8" [ ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 69dc391c42..b25ea766ae 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -77,16 +77,16 @@ GEXTEND Gram
   ;
   reference:
     [ [ id = ident; (l,id') = fields ->
-        Qualid (Loc.tag ~loc:!@loc @@ local_make_qualid (l@[id]) id')
-      | id = ident -> Ident (Loc.tag ~loc:!@loc id)
+        CAst.make ~loc:!@loc @@ Qualid (local_make_qualid (l@[id]) id')
+      | id = ident -> CAst.make ~loc:!@loc @@ Ident id
       ] ]
   ;
   by_notation:
-    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> CAst.make ~loc:!@loc (s, sc) ] ]
+    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (s, sc) ] ]
   ;
   smart_global:
-    [ [ c = reference -> Misctypes.AN c
-      | ntn = by_notation -> Misctypes.ByNotation ntn ] ]
+    [ [ c = reference -> CAst.make ~loc:!@loc @@ Misctypes.AN c
+      | ntn = by_notation -> CAst.make ~loc:!@loc @@ Misctypes.ByNotation ntn ] ]
   ;
   qualid:
     [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 99eec97424..72c3cc14a1 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -624,9 +624,9 @@ GEXTEND Gram
             VernacSetStrategy l
       (* Canonical structure *)
       | IDENT "Canonical"; IDENT "Structure"; qid = global ->
-	  VernacCanonical (AN qid)
+          VernacCanonical CAst.(make ~loc:!@loc @@ AN qid)
       | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation ->
-	  VernacCanonical (ByNotation ntn)
+          VernacCanonical CAst.(make ~loc:!@loc @@ ByNotation ntn)
       | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
           let s = coerce_reference_to_id qid in
           VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d)
@@ -640,10 +640,10 @@ GEXTEND Gram
            VernacIdentityCoercion (f, s, t)
       | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
-          VernacCoercion (AN qid, s, t)
+          VernacCoercion (CAst.make ~loc:!@loc @@ AN qid, s, t)
       | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
-          VernacCoercion (ByNotation ntn, s, t)
+          VernacCoercion (CAst.make ~loc:!@loc @@ ByNotation ntn, s, t)
 
       | IDENT "Context"; c = binders ->
 	  VernacContext c
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 0f8aad1105..9f186224b9 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -210,7 +210,7 @@ module Prim :
     val qualid : qualid CAst.t Gram.entry
     val fullyqualid : Id.t list CAst.t Gram.entry
     val reference : reference Gram.entry
-    val by_notation : (string * string option) CAst.t Gram.entry
+    val by_notation : (string * string option) Gram.entry
     val smart_global : reference or_by_notation Gram.entry
     val dirpath : DirPath.t Gram.entry
     val ne_string : string Gram.entry