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

2 files changed, 10 insertions, 12 deletions

diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 7f1cca277e..f2025858d7 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -41,7 +41,7 @@ GRAMMAR EXTEND Gram
       | cmd = Pvernac.Vernac_.main_entry ->
               { match cmd with
               | None -> None
-              | Some (loc,c) -> Some (CAst.make ~loc (VernacControl c)) }
+              | Some {CAst.loc; v} -> Some (CAst.make ?loc (VernacControl v)) }
       ]
     ]
   ;
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 45ca658857..ef1dc6993b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -101,20 +101,18 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
         ~doc:state.doc ~entry:Pvernac.main_entry state.sid in_pa
     with
     | None ->
-        input_cleanup ();
-        state, ids, Pcoq.Parsable.comment_state in_pa
-    | Some (loc, ast) ->
-        let ast = CAst.make ~loc ast in
+      input_cleanup ();
+      state, ids, Pcoq.Parsable.comment_state in_pa
+    | Some ast ->
+      (* Printing of AST for -compile-verbose *)
+      Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo;
 
-        (* Printing of AST for -compile-verbose *)
-        Option.iter (vernac_echo ~loc) in_echo;
+      checknav_simple ast;
 
-        checknav_simple ast;
+      let state =
+        Flags.silently (interp_vernac ~check ~interactive ~state) ast in
 
-        let state =
-          Flags.silently (interp_vernac ~check ~interactive ~state) ast in
-
-        loop state (state.sid :: ids)
+      loop state (state.sid :: ids)
   in
   try loop state []
   with any ->   (* whatever the exception *)