[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, 13 insertions, 12 deletions

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;
        }