Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLater

Ack-by: ejgallego
Reviewed-by: gares

4 files changed, 10 insertions, 11 deletions

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