[parsing] Use AST node for main parsing entry.

Before #9263 this type was returned by the STM's `parse_sentence`, but
the type was lost on the generalization to entries.

3 files changed, 4 insertions, 4 deletions

diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 0e46df2320..994fad85f0 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -52,7 +52,7 @@ module Vernac_ =
 
     let () =
       let open Extend in
-      let act_vernac v loc = Some (loc, v) in
+      let act_vernac v loc = Some CAst.(make ~loc v) in
       let act_eoi _ loc = None in
       let rule = [
         Rule (Next (Stop, Atoken Tok.EOI), act_eoi);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index fa251281dc..4bf7c9f7bd 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -26,7 +26,7 @@ module Vernac_ :
     val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
     val noedit_mode : vernac_expr Entry.t
     val command_entry : vernac_expr Entry.t
-    val main_entry : (Loc.t * vernac_control) option Entry.t
+    val main_entry : vernac_control CAst.t option Entry.t
     val red_expr : raw_red_expr Entry.t
     val hint_info : Hints.hint_info_expr Entry.t
   end
@@ -40,7 +40,7 @@ module Unsafe : sig
 end
 
 (** The main entry: reads an optional vernac command *)
-val main_entry : proof_mode option -> (Loc.t * vernac_control) option Entry.t
+val main_entry : proof_mode option -> vernac_control CAst.t option Entry.t
 
 (** Grammar entry for tactics: proof mode(s).
   By default Coq's grammar has an empty entry (non-terminal) for
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7611355100..a5ef41c4db 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2167,7 +2167,7 @@ let vernac_load interp fname =
           else
             None
         in
-        interp (snd (parse_sentence proof_mode input));
+        interp (parse_sentence proof_mode input).CAst.v;
       done
     with End_of_input -> ()
   end;