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

2 files changed, 6 insertions, 6 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index b3da97c6e..b1cecc6d1 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1084,7 +1084,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
       | VernacShow ShowScript -> ShowScript.show_script (); st (** XX we are ignoring control here *)
       | _ ->
         stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
-        try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr)
+        try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (CAst.make ?loc expr)
         with e ->
           let e = CErrors.push e in
           Exninfo.iraise Hooks.(call_process_error_once e)
@@ -2992,7 +2992,7 @@ let parse_sentence ~doc sid pa =
       try
         match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
         | None            -> raise End_of_input
-        | Some (loc, cmd) -> Loc.tag ~loc cmd
+        | Some (loc, cmd) -> CAst.make ~loc cmd
       with e when CErrors.noncritical e ->
         let (e, info) = CErrors.push e in
         Exninfo.iraise (e, info))
@@ -3033,7 +3033,7 @@ let compute_indentation ?loc sid = Option.cata (fun loc ->
     eff_indent, len
   ) (0, 0) loc
 
-let add ~doc ~ontop ?newtip verb (loc, ast) =
+let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } =
   let cur_tip = VCS.cur_tip () in
   if not (Stateid.equal ontop cur_tip) then
     user_err ?loc ~hdr:"Stm.add"
@@ -3063,7 +3063,7 @@ let query ~doc ~at ~route s =
     else Reach.known_state ~cache:`Yes at;
     try
       while true do
-        let loc, ast            = parse_sentence ~doc at s in
+        let { CAst.loc; v=ast } = parse_sentence ~doc at s in
         let indentation, strlen = compute_indentation ?loc at in
         CWarnings.set_current_loc loc;
         let clas = Vernac_classifier.classify_vernac ast in
diff --git a/stm/stm.mli b/stm/stm.mli
index f967c9815..a8eb10fb3 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -80,7 +80,7 @@ val new_doc  : stm_init_options -> doc * Stateid.t
 (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
    state [sid] Returns [End_of_input] if the stream ends *)
 val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable ->
-  Vernacexpr.vernac_control Loc.located
+  Vernacexpr.vernac_control CAst.t
 
 (* Reminder: A parsable [pa] is constructed using
    [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *)
@@ -94,7 +94,7 @@ exception End_of_input
    If [newtip] is provided, then the returned state id is guaranteed
    to be [newtip] *)
 val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
-  bool -> Vernacexpr.vernac_control Loc.located ->
+  bool -> Vernacexpr.vernac_control CAst.t ->
   doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
 (* [query at ?report_with cmd] Executes [cmd] at a given state [at],