[vernacextend] Consolidate extension points API

We group the extension API and datatypes under `Vernacextend`.

This means that the base plugin dependency is now `coq.vernac` from
`coq.stm`.

This is quite important as for example the LSP server won't like to
link the STM in.

LTAC still depends on the STM by means of the ltac_profile part tho.

The next step could be to move the extension point below `Vernacexpr`.

22 files changed, 187 insertions, 133 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index ba3b9bcbbf..8da4c6db13 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -374,9 +374,9 @@ let print_rules fmt rules =
 let print_classifier fmt = function
 | ClassifDefault -> fprintf fmt ""
 | ClassifName "QUERY" ->
-  fprintf fmt "~classifier:(fun _ -> Vernac_classifier.classify_as_query)"
+  fprintf fmt "~classifier:(fun _ -> Vernacextend.classify_as_query)"
 | ClassifName "SIDEFF" ->
-  fprintf fmt "~classifier:(fun _ -> Vernac_classifier.classify_as_sideeff)"
+  fprintf fmt "~classifier:(fun _ -> Vernacextend.classify_as_sideeff)"
 | ClassifName s -> fatal (Printf.sprintf "Unknown classifier %s" s)
 | ClassifCode c -> fprintf fmt "~classifier:(%s)" c.code
 
diff --git a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh
new file mode 100644
index 0000000000..61ffa4a197
--- /dev/null
+++ b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9003" ] || [ "$CI_BRANCH" = "vernac+move_extend_ast" ]; then
+
+    ltac2_CI_REF=vernac+move_extend_ast
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f94e9acb72..4287702b3a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -514,18 +514,18 @@ let _ =
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in
   let cmd_fn c ~atts ~st = in_current_context econstr_display c; st in
-  let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in
+  let cmd_class _ = VtQuery,VtNow in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
-  Vernacextend.vernac_extend ~command:"PrintConstr" [cmd]
+  vernac_extend ~command:"PrintConstr" [cmd]
 
 let _ =
   let open Vernacextend in
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in
   let cmd_fn c ~atts ~st = in_current_context print_pure_econstr c; st in
-  let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in
+  let cmd_class _ = VtQuery,VtNow in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
-  Vernacextend.vernac_extend ~command:"PrintPureConstr" [cmd]
+  vernac_extend ~command:"PrintPureConstr" [cmd]
 
 (* Setting printer of unbound global reference *)
 open Names
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index 18316bf2cd..df4b647642 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -18,7 +18,7 @@ DECLARE PLUGIN "derive_plugin"
 
 {
 
-let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
+let classify_derive_command _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
 
 }
 
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 155df1c1e0..7e707b423a 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -186,8 +186,8 @@ VERNAC COMMAND EXTEND Function
            Vernac_classifier.classify_vernac
              (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
          with
-         | Vernacexpr.VtSideff ids, _ when hard ->
-             Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
+         | Vernacextend.VtSideff ids, _ when hard ->
+             Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
          | x -> x }
     -> { do_generate_principle false (List.map snd recsl) }
 END
@@ -225,7 +225,7 @@ let warning_error names e =
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
 | ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
-   => { Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater }
+   => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
    ->
     {
       begin
@@ -261,7 +261,7 @@ END
 
 VERNAC COMMAND EXTEND NewFunctionalCase
 | ["Functional" "Case" fun_scheme_arg(fas) ]
-  => { Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater }
+  => { Vernacextend.(VtSideff[pi1 fas], VtLater) }
   -> { Functional_principles_types.build_case_scheme fas }
 END
 
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 70e5ab38bc..24d9406f08 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -31,6 +31,7 @@ open Tactypes
 open Tactics
 open Proofview.Notations
 open Attributes
+open Vernacextend
 
 let wit_hyp = wit_var
 
@@ -315,7 +316,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
   let add_hints base = add_rew_rules base eqs in
   List.iter add_hints bases
 
-let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater
+let classify_hint _ = VtSideff [], VtLater
 
 }
 
@@ -398,7 +399,7 @@ END
 open Inv
 open Leminv
 
-let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
+let seff id = VtSideff [id], VtLater
 
 }
 
@@ -910,7 +911,7 @@ END
    mode. *)
 VERNAC COMMAND EXTEND GrabEvars
 | [ "Grab" "Existential" "Variables" ]
-  => { Vernac_classifier.classify_as_proofstep }
+  => { classify_as_proofstep }
   -> { Proof_global.simple_with_current_proof (fun _ p  -> Proof.V82.grab_evars p) }
 END
 
@@ -942,7 +943,7 @@ END
 (* Command to add every unshelved variables to the focus *)
 VERNAC COMMAND EXTEND Unshelve
 | [ "Unshelve" ]
-  => { Vernac_classifier.classify_as_proofstep }
+  => { classify_as_proofstep }
   -> { Proof_global.simple_with_current_proof (fun _ p  -> Proof.unshelve p) }
 END
 
@@ -1094,9 +1095,9 @@ END
 
 
 VERNAC COMMAND EXTEND OptimizeProof
-| [ "Optimize" "Proof" ] => { Vernac_classifier.classify_as_proofstep } ->
+| [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
   { Proof_global.compact_the_proof () }
-| [ "Optimize" "Heap" ] => { Vernac_classifier.classify_as_proofstep } ->
+| [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
   { Gc.compact () }
 END
 
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index c58c8556c5..31bfd41a1f 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -367,8 +367,7 @@ GRAMMAR EXTEND Gram
 
 open Stdarg
 open Tacarg
-open Vernacexpr
-open Vernac_classifier
+open Vernacextend
 open Goptions
 open Libnames
 
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index aa78fb5d1e..e29f78af5b 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -84,7 +84,7 @@ open Obligations
 let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
 let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
 
-let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
+let classify_obbl _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
 
 }
 
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 1c7220ddc0..2596bc22f2 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -26,6 +26,7 @@ open Pcoq.Prim
 open Pcoq.Constr
 open Pvernac.Vernac_
 open Pltac
+open Vernacextend
 
 let wit_hyp = wit_var
 
@@ -280,18 +281,18 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
      }
   | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
-    => { Vernacexpr.VtUnknown, Vernacexpr.VtNow }
+    => { VtUnknown, VtNow }
     -> {
            add_morphism_infer atts m n;
        }
   | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
-    => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
+    => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater }
     -> {
            add_morphism atts [] m s n;
        }
   | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
-    => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
+    => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater }
     -> {
            add_morphism atts binders m s n;
        }
diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg
index 3ddea7eb30..f59ca4cef4 100644
--- a/plugins/setoid_ring/g_newring.mlg
+++ b/plugins/setoid_ring/g_newring.mlg
@@ -86,7 +86,7 @@ END
 VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
   | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] ->
     { let l = match l with None -> [] | Some l -> l in add_theory id t l }
-  | [ "Print" "Rings" ] => {Vernac_classifier.classify_as_query} -> {
+  | [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> {
     Feedback.msg_notice (strbrk "The following ring structures have been declared:");
     Spmap.iter (fun fn fi ->
       let sigma, env = Pfedit.get_current_context () in
@@ -130,7 +130,7 @@ END
 VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
 | [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] ->
   { let l = match l with None -> [] | Some l -> l in add_field_theory id t l }
-| [ "Print" "Fields" ] => {Vernac_classifier.classify_as_query} -> {
+| [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> {
     Feedback.msg_notice (strbrk "The following field structures have been declared:");
     Spmap.iter (fun fn fi ->
       let sigma, env = Pfedit.get_current_context () in
diff --git a/stm/stm.ml b/stm/stm.ml
index b474bd502a..9359ab15e2 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -25,6 +25,7 @@ open CErrors
 open Names
 open Feedback
 open Vernacexpr
+open Vernacextend
 
 module AsyncOpts = struct
 
@@ -162,7 +163,7 @@ type branch_type =
   [ `Master
   | `Proof of proof_mode * depth
   | `Edit of
-      proof_mode * Stateid.t * Stateid.t  * vernac_qed_type * Vcs_.Branch.t ]
+      proof_mode * Stateid.t * Stateid.t  * Vernacextend.vernac_qed_type * Vcs_.Branch.t ]
 (* TODO 8.7 : split commands and tactics, since this type is too messy now *)
 type cmd_t = {
   ctac : bool; (* is a tactic *)
@@ -174,7 +175,7 @@ type cmd_t = {
            | `TacQueue of solving_tac * anon_abstracting_tac * AsyncTaskQueue.cancel_switch
            | `QueryQueue of AsyncTaskQueue.cancel_switch
            | `SkipQueue ] }
-type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Names.Id.t list
+type fork_t = aast * Vcs_.Branch.t * opacity_guarantee * Names.Id.t list
 type qed_t = {
   qast : aast;
   keep : vernac_qed_type;
diff --git a/stm/stm.mli b/stm/stm.mli
index 95117f04f4..0c0e19ce5c 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -258,7 +258,7 @@ type dynamic_block_error_recovery =
   doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
 
 val register_proof_block_delimiter :
-  Vernacexpr.proof_block_name ->
+  Vernacextend.proof_block_name ->
   static_block_detection ->
   dynamic_block_error_recovery ->
     unit
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 4db86817c9..526858bd73 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -12,6 +12,7 @@ open CErrors
 open Util
 open Pp
 open CAst
+open Vernacextend
 open Vernacexpr
 
 let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
@@ -209,7 +210,3 @@ let classify_vernac e =
         | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
   in
   static_control_classifier e
-
-let classify_as_query = VtQuery, VtLater
-let classify_as_sideeff = VtSideff [], VtLater
-let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index e82b191418..9d93ad1f39 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -8,16 +8,12 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Vernacexpr
+open Vernacextend
 
 val string_of_vernac_classification : vernac_classification -> string
 
 (** What does a vernacular do *)
-val classify_vernac : vernac_control -> vernac_classification
-
-(** Standard constant classifiers *)
-val classify_as_query : vernac_classification
-val classify_as_sideeff : vernac_classification
-val classify_as_proofstep : vernac_classification
+val classify_vernac : Vernacexpr.vernac_control -> vernac_classification
 
+(**  *)
 val stm_allow_nested_proofs_option_name : string list
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 88638b295b..bc0b0310b3 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -9,7 +9,14 @@
 (************************************************************************)
 
 open CErrors
-open Vernacexpr
+
+(** The type of parsing attribute data *)
+type vernac_flags = vernac_flag list
+and vernac_flag = string * vernac_flag_value
+and vernac_flag_value =
+  | VernacFlagEmpty
+  | VernacFlagLeaf of string
+  | VernacFlagList of vernac_flags
 
 let unsupported_attributes = function
   | [] -> ()
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index c81082d5ad..c2dde4cbcc 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -8,7 +8,13 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Vernacexpr
+(** The type of parsing attribute data *)
+type vernac_flags = vernac_flag list
+and vernac_flag = string * vernac_flag_value
+and vernac_flag_value =
+  | VernacFlagEmpty
+  | VernacFlagLeaf of string
+  | VernacFlagList of vernac_flags
 
 type +'a attribute
 (** The type of attributes. When parsing attributes if an ['a
@@ -80,7 +86,7 @@ val parse_with_extra : 'a attribute -> vernac_flags -> vernac_flags * 'a
 
 (** * Defining attributes. *)
 
-type 'a key_parser = 'a option -> Vernacexpr.vernac_flag_value -> 'a
+type 'a key_parser = 'a option -> vernac_flag_value -> 'a
 (** A parser for some key in an attribute. It is given a nonempty ['a
     option] when the attribute is multiply set for some command.
 
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index a90ef97e7d..3689f60383 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -21,10 +21,10 @@ type 's grammar_prod_item =
       ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
-  Vernacexpr.extend_name -> vernac_expr Pcoq.Entry.t option ->
+  extend_name -> vernac_expr Pcoq.Entry.t option ->
     vernac_expr grammar_prod_item list -> unit
 
-val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
+val get_extend_vernac_rule : extend_name -> vernac_expr grammar_prod_item list
 
 val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type
 
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1d0a5ab0a3..fbead06adb 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -30,6 +30,7 @@ open Pcoq.Prim
 open Pcoq.Constr
 open Pcoq.Module
 open Pvernac.Vernac_
+open Attributes
 
 let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
 let _ = List.iter CLexer.add_keyword vernac_kw
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 1c1faca599..e56261a78d 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1213,6 +1213,7 @@ open Pputils
 
 let rec pr_vernac_flag (k, v) =
   let k = keyword k in
+  let open Attributes in
   match v with
   | VernacFlagEmpty -> k
   | VernacFlagLeaf v -> k ++ str " = " ++ qs v
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 594e9eca48..5bcab29a3a 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -219,13 +219,6 @@ type section_subset_expr =
 
     {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command.
  *)
-type extend_name =
-  (** Name of the vernac entry where the tactic is defined, typically found
-      after the VERNAC EXTEND statement in the source. *)
-  string *
-  (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch
-      is given an offset, starting from zero. *)
-  int
 
 (* This type allows registering the inlining of constants in native compiler.
    It will be extended with primitive inductive types and operators *)
@@ -253,6 +246,14 @@ type vernac_argument_status = {
   implicit_status : vernac_implicit_status;
 }
 
+type extend_name =
+  (** Name of the vernac entry where the tactic is defined, typically found
+      after the VERNAC EXTEND statement in the source. *)
+  string *
+  (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch
+      is given an offset, starting from zero. *)
+  int
+
 type nonrec vernac_expr =
 
   | VernacLoad of verbose_flag * string
@@ -395,71 +396,11 @@ type nonrec vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-type vernac_flags = vernac_flag list
-and vernac_flag = string * vernac_flag_value
-and vernac_flag_value =
-  | VernacFlagEmpty
-  | VernacFlagLeaf of string
-  | VernacFlagList of vernac_flags
-
 type vernac_control =
-  | VernacExpr of vernac_flags * vernac_expr
+  | VernacExpr of Attributes.vernac_flags * vernac_expr
   (* boolean is true when the `-time` batch-mode command line flag was set.
      the flag is used to print differently in `-time` vs `Time foo` *)
   | VernacTime of bool * vernac_control CAst.t
   | VernacRedirect of string * vernac_control CAst.t
   | VernacTimeout of int * vernac_control
   | VernacFail of vernac_control
-
-(* A vernac classifier provides information about the exectuion of a
-   command:
-
-   - vernac_when: encodes if the vernac may alter the parser [thus
-     forcing immediate execution], or if indeed it is pure and parsing
-     can continue without its execution.
-
-   - vernac_type: if it is starts, ends, continues a proof or
-     alters the global state or is a control command like BackTo or is
-     a query like Check.
-
-   The classification works on the assumption that we have 3 states:
-   parsing, execution (global enviroment, etc...), and proof
-   state. For example, commands that only alter the proof state are
-   considered safe to delegate to a worker.
-
-*)
-type vernac_type =
-  (* Start of a proof *)
-  | VtStartProof of vernac_start
-  (* Command altering the global state, bad for parallel
-     processing. *)
-  | VtSideff of vernac_sideff_type
-  (* End of a proof *)
-  | VtQed of vernac_qed_type
-  (* A proof step *)
-  | VtProofStep of proof_step
-  (* To be removed *)
-  | VtProofMode of string
-  (* Queries are commands assumed to be "pure", that is to say, they
-     don't modify the interpretation state. *)
-  | VtQuery
-  (* To be removed *)
-  | VtMeta
-  | VtUnknown
-and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
-and vernac_start = string * opacity_guarantee * Id.t list
-and vernac_sideff_type = Id.t list
-and opacity_guarantee =
-  | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
-  | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
-and proof_step = { (* TODO: inline with OCaml 4.03 *)
-  parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
-  proof_block_detection : proof_block_name option
-}
-and solving_tac = bool (* a terminator *)
-and anon_abstracting_tac = bool (* abstracting anonymously its result *)
-and proof_block_name = string (* open type of delimiters *)
-type vernac_when =
-  | VtNow
-  | VtLater
-type vernac_classification = vernac_type * vernac_when
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 5fba586298..3a321ecdb4 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -12,7 +12,43 @@ open Util
 open Pp
 open CErrors
 
-type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+type vernac_type =
+  (* Start of a proof *)
+  | VtStartProof of vernac_start
+  (* Command altering the global state, bad for parallel
+     processing. *)
+  | VtSideff of vernac_sideff_type
+  (* End of a proof *)
+  | VtQed of vernac_qed_type
+  (* A proof step *)
+  | VtProofStep of {
+      parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
+      proof_block_detection : proof_block_name option
+    }
+  (* To be removed *)
+  | VtProofMode of string
+  (* Queries are commands assumed to be "pure", that is to say, they
+     don't modify the interpretation state. *)
+  | VtQuery
+  (* To be removed *)
+  | VtMeta
+  | VtUnknown
+and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
+and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_sideff_type = Names.Id.t list
+and opacity_guarantee =
+  | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
+  | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
+and solving_tac = bool (** a terminator *)
+and anon_abstracting_tac = bool (** abstracting anonymously its result *)
+and proof_block_name = string (** open type of delimiters *)
+
+type vernac_when =
+  | VtNow
+  | VtLater
+type vernac_classification = vernac_type * vernac_when
+
+type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
@@ -68,10 +104,23 @@ let call opn converted_args ~atts ~st =
 
 (** VERNAC EXTEND registering *)
 
-type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
+type classifier = Genarg.raw_generic_argument list -> vernac_classification
+
+(** Classifiers  *)
+let classifiers : classifier array String.Map.t ref = ref String.Map.empty
+
+let get_vernac_classifier (name, i) args =
+  (String.Map.find name !classifiers).(i) args
+
+let declare_vernac_classifier name f =
+  classifiers := String.Map.add name f !classifiers
+
+let classify_as_query = VtQuery, VtLater
+let classify_as_sideeff = VtSideff [], VtLater
+let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
 
 type (_, _) ty_sig =
-| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
 
@@ -124,7 +173,7 @@ let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s
 | TUentry a -> Aentry (Pcoq.genarg_grammar (Genarg.ExtraArg a))
 | TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (Genarg.ExtraArg a), string_of_int i)
 
-let rec untype_grammar : type r s. (r, s) ty_sig -> Vernacexpr.vernac_expr Egramml.grammar_prod_item list = function
+let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function
 | TyNil -> []
 | TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty
 | TyNonTerminal (tu, ty) ->
@@ -132,16 +181,6 @@ let rec untype_grammar : type r s. (r, s) ty_sig -> Vernacexpr.vernac_expr Egram
   let symb = untype_user_symbol tu in
   Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty
 
-let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol
-
-let classifiers : classifier array String.Map.t ref = ref String.Map.empty
-
-let get_vernac_classifier (name, i) args =
-  (String.Map.find name !classifiers).(i) args
-
-let declare_vernac_classifier name f =
-  classifiers := String.Map.add name f !classifiers
-
 let vernac_extend ~command ?classifier ?entry ext =
   let get_classifier (TyML (_, ty, _, cl)) = match cl with
   | Some cl -> untype_classifier ty cl
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index bb94f3a6a9..7feaccd9a3 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -8,20 +8,75 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(** Vernacular Extension data *)
+
+(* A vernac classifier provides information about the exectuion of a
+   command:
+
+   - vernac_when: encodes if the vernac may alter the parser [thus
+     forcing immediate execution], or if indeed it is pure and parsing
+     can continue without its execution.
+
+   - vernac_type: if it is starts, ends, continues a proof or
+     alters the global state or is a control command like BackTo or is
+     a query like Check.
+
+   The classification works on the assumption that we have 3 states:
+   parsing, execution (global enviroment, etc...), and proof
+   state. For example, commands that only alter the proof state are
+   considered safe to delegate to a worker.
+
+*)
+type vernac_type =
+  (* Start of a proof *)
+  | VtStartProof of vernac_start
+  (* Command altering the global state, bad for parallel
+     processing. *)
+  | VtSideff of vernac_sideff_type
+  (* End of a proof *)
+  | VtQed of vernac_qed_type
+  (* A proof step *)
+  | VtProofStep of {
+      parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
+      proof_block_detection : proof_block_name option
+    }
+  (* To be removed *)
+  | VtProofMode of string
+  (* Queries are commands assumed to be "pure", that is to say, they
+     don't modify the interpretation state. *)
+  | VtQuery
+  (* To be removed *)
+  | VtMeta
+  | VtUnknown
+and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
+and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_sideff_type = Names.Id.t list
+and opacity_guarantee =
+  | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
+  | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
+and solving_tac = bool (** a terminator *)
+and anon_abstracting_tac = bool (** abstracting anonymously its result *)
+and proof_block_name = string (** open type of delimiters *)
+
+type vernac_when =
+  | VtNow
+  | VtLater
+type vernac_classification = vernac_type * vernac_when
+
 (** Interpretation of extended vernac phrases. *)
 
-type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
-val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
+val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
 
 (** {5 VERNAC EXTEND} *)
 
-type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
+type classifier = Genarg.raw_generic_argument list -> vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal :
   ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
@@ -32,7 +87,7 @@ type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option ->
 (** Wrapper to dynamically extend vernacular commands. *)
 val vernac_extend :
   command:string ->
-  ?classifier:(string -> Vernacexpr.vernac_classification) ->
+  ?classifier:(string -> vernac_classification) ->
   ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
   ty_ml list -> unit
 
@@ -55,6 +110,9 @@ val vernac_argument_extend : name:string -> 'a vernac_argument ->
   ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t
 
 (** {5 STM classifiers} *)
+val get_vernac_classifier : Vernacexpr.extend_name -> classifier
 
-val get_vernac_classifier :
-  Vernacexpr.extend_name -> classifier
+(** Standard constant classifiers *)
+val classify_as_query : vernac_classification
+val classify_as_sideeff : vernac_classification
+val classify_as_proofstep : vernac_classification