Merge PR #9003: [vernacextend] Consolidate extension points API

7 files changed, 20 insertions, 19 deletions

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 04a8ae1746..603dd60cf2 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 9730fc7fd8..bd8a097154 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