[located] More work towards using CAst.t

We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:

- module declarations
- intro patterns
- top-level sentences

Now, parsed documents should be full annotated by `CAst` nodes.

3 files changed, 9 insertions, 10 deletions

diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index a1d36b822..69dc391c4 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -62,8 +62,8 @@ GEXTEND Gram
       ] ]
   ;
   fullyqualid:
-    [ [ id = ident; (l,id')=fields -> Loc.tag ~loc:!@loc @@ id::List.rev (id'::l)
-      | id = ident -> Loc.tag ~loc:!@loc [id]
+    [ [ id = ident; (l,id')=fields -> CAst.make ~loc:!@loc @@ id::List.rev (id'::l)
+      | id = ident -> CAst.make ~loc:!@loc [id]
       ] ]
   ;
   basequalid:
@@ -82,14 +82,14 @@ GEXTEND Gram
       ] ]
   ;
   by_notation:
-    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> Loc.tag ~loc:!@loc (s, sc) ] ]
+    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> CAst.make ~loc:!@loc (s, sc) ] ]
   ;
   smart_global:
     [ [ c = reference -> Misctypes.AN c
       | ntn = by_notation -> Misctypes.ByNotation ntn ] ]
   ;
   qualid:
-    [ [ qid = basequalid -> Loc.tag ~loc:!@loc qid ] ]
+    [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ]
   ;
   ne_string:
     [ [ s = STRING ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f1ec49623..99eec9742 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -554,7 +554,7 @@ GEXTEND Gram
       ] ]
   ;
   module_expr_atom:
-    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ]
+    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ]
   ;
   with_declaration:
     [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
@@ -564,7 +564,7 @@ GEXTEND Gram
       ] ]
   ;
   module_type:
-    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid)
+    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v)
       | "("; mt = module_type; ")" -> mt
       | mty = module_type; me = module_expr_atom ->
           CAst.make ~loc:!@loc @@ CMapply (mty,me)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e66aa4ade..0f8aad110 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Loc
 open Names
 open Extend
 open Vernacexpr
@@ -208,10 +207,10 @@ module Prim :
     val integer : int Gram.entry
     val string : string Gram.entry
     val lstring : lstring Gram.entry
-    val qualid : qualid located Gram.entry
-    val fullyqualid : Id.t list located Gram.entry
+    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) Loc.located Gram.entry
+    val by_notation : (string * string option) CAst.t Gram.entry
     val smart_global : reference or_by_notation Gram.entry
     val dirpath : DirPath.t Gram.entry
     val ne_string : string Gram.entry