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

4 files changed, 8 insertions, 14 deletions

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