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

1 files changed, 2 insertions, 2 deletions

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