STM: encode in static types that vernac_when is only used when VtSideff

The stm.ml changes show that for the other classifications either the
vernac_when was ignored, or there was an assert on it forcing it to be
Now or Later depending on the vernac_type.

One may also note that the classification used in top_printers
`VtQuery,VtNow` would have failed those asserts...

6 files changed, 16 insertions, 17 deletions

diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index 6c9cd66f96..de3fb9f11f 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 _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater)
+let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
 
 }
 
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 833ff9f1ed..c217ed8b1d 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -186,14 +186,14 @@ let classify_as_Fixpoint recsl =
 
 let classify_funind recsl =
   match classify_as_Fixpoint recsl with
-  | Vernacextend.VtSideff ids, _
+  | Vernacextend.VtSideff (ids, _)
     when is_proof_termination_interactively_checked recsl ->
-      Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
+      Vernacextend.(VtStartProof (GuaranteesOpacity, ids))
   | x -> x
 
 let is_interactive recsl =
   match classify_funind recsl with
-  | Vernacextend.VtStartProof _, _ -> true
+  | Vernacextend.VtStartProof _ -> true
   | _ -> false
 
 }
@@ -243,7 +243,7 @@ let warning_error names e =
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
 | ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
-   => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
+   => { Vernacextend.(VtSideff(List.map pi1 fas, VtLater)) }
    ->
     { begin
         try
@@ -275,7 +275,7 @@ END
 
 VERNAC COMMAND EXTEND NewFunctionalCase
 | ["Functional" "Case" fun_scheme_arg(fas) ]
-  => { Vernacextend.(VtSideff[pi1 fas], 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 7691ca225e..7ba63f1830 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -336,7 +336,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 _ = VtSideff [], VtLater
+let classify_hint _ = VtSideff ([], VtLater)
 
 }
 
@@ -422,7 +422,7 @@ END
 open Inv
 open Leminv
 
-let seff id = VtSideff [id], VtLater
+let seff id = VtSideff ([id], VtLater)
 
 }
 
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index d10d10a664..afdea98ef5 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -446,8 +446,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
       let solving_tac = is_explicit_terminator t in
       let parallel = `Yes (solving_tac,anon_abstracting_tac) in
       let pbr = if solving_tac then Some "par" else None in
-      VtProofStep{ parallel = parallel; proof_block_detection = pbr },
-      VtLater
+      VtProofStep{ parallel = parallel; proof_block_detection = pbr }
     } -> {
       let t = rm_abstract t in
       vernac_solve Goal_select.SelectAll n t def
@@ -494,7 +493,7 @@ END
 VERNAC COMMAND EXTEND VernacTacticNotation
 | #[ deprecation; locality; ]
   [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
-  { VtSideff [], VtNow } ->
+  { VtSideff ([], VtNow) } ->
   {
     let n = Option.default 0 n in
     Tacentries.add_tactic_notation (Locality.make_module_locality locality) n ?deprecation r e;
@@ -542,7 +541,7 @@ VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
 | #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => {
     VtSideff (List.map (function
       | TacticDefinition ({CAst.v=r},_) -> r
-      | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
+      | TacticRedefinition (qid,_) -> qualid_basename qid) l, VtLater)
   } -> {
          Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l;
   }
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 58c8dabd79..62bc2a9259 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -83,7 +83,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 _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
+let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
 
 }
 
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 1a84158df7..1cc333945d 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -277,19 +277,19 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
          add_setoid atts binders a aeq t n
      }
   | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
-    => { VtStartProof(GuaranteesOpacity, [n]), VtLater }
+    => { VtStartProof(GuaranteesOpacity, [n]) }
     -> { if Lib.is_modtype () then
            CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead.");
          add_morphism_interactive atts m n }
   | #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" ident(n) ]
-    => { VtSideff([n]), VtLater }
+    => { VtSideff([n], VtLater) }
     -> { add_morphism_as_parameter atts m n }
   | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
-    => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
+    => { VtStartProof(GuaranteesOpacity,[n]) }
     -> { add_morphism atts [] m s n }
   | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
-    => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
+    => { VtStartProof(GuaranteesOpacity,[n]) }
     -> { add_morphism atts binders m s n }
 END