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

Ack-by: ejgallego
Reviewed-by: gares

13 files changed, 106 insertions, 108 deletions

diff --git a/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh b/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh
new file mode 100644
index 0000000000..c5f1510357
--- /dev/null
+++ b/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10319" ] || [ "$CI_BRANCH" = "vernac-when-sideff" ]; then
+
+    mtac2_CI_REF=vernac-when-sideff
+    mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
+
+    equations_CI_REF=vernac-when-sideff
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4ce87faaa1..87b4d31054 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -533,7 +533,7 @@ let _ =
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in
   let cmd_fn c ~atts = VtDefault (fun () -> in_current_context econstr_display c) in
-  let cmd_class _ = VtQuery,VtNow in
+  let cmd_class _ = VtQuery in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   vernac_extend ~command:"PrintConstr" [cmd]
 
@@ -542,7 +542,7 @@ let _ =
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in
   let cmd_fn c ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) in
-  let cmd_class _ = VtQuery,VtNow in
+  let cmd_class _ = VtQuery in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   vernac_extend ~command:"PrintPureConstr" [cmd]
 
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
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 1e89d6937c..d77e37c910 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1563,7 +1563,7 @@ end = struct (* {{{ *)
   let perform_states query =
     if query = [] then [] else
     let is_tac e = match Vernac_classifier.classify_vernac e with
-    | VtProofStep _, _ -> true
+    | VtProofStep _ -> true
     | _ -> false
     in
     let initial =
@@ -2860,12 +2860,12 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
         "  classified as: " ^ Vernac_classifier.string_of_vernac_classification c);
       match c with
       (* Meta *)
-      | VtMeta, _ ->
+      | VtMeta ->
         let id = Backtrack.undo_vernac_classifier expr ~doc in
         process_back_meta_command ~newtip ~head id x
 
       (* Query *)
-      | VtQuery, w ->
+      | VtQuery ->
           let id = VCS.new_node ~id:newtip proof_mode () in
           let queue =
             if VCS.is_vio_doc () &&
@@ -2875,10 +2875,10 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
             else `MainQueue in
           VCS.commit id (mkTransCmd x [] false queue);
           VCS.set_parsing_state id head_parsing;
-          Backtrack.record (); assert (w == VtLater); `Ok
+          Backtrack.record (); `Ok
 
       (* Proof *)
-      | VtStartProof (guarantee, names), w ->
+      | VtStartProof (guarantee, names) ->
 
          if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then
            "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
@@ -2900,9 +2900,9 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
             VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
           end;
           VCS.set_parsing_state id head_parsing;
-          Backtrack.record (); assert (w == VtLater); `Ok
+          Backtrack.record (); `Ok
 
-      | VtProofStep { parallel; proof_block_detection = cblock }, w ->
+      | VtProofStep { parallel; proof_block_detection = cblock } ->
           let id = VCS.new_node ~id:newtip proof_mode () in
           let queue =
             match parallel with
@@ -2914,18 +2914,18 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
              detection should occur here.
           detect_proof_block id cblock; *)
           VCS.set_parsing_state id head_parsing;
-          Backtrack.record (); assert (w == VtLater); `Ok
+          Backtrack.record (); `Ok
 
-      | VtQed keep, w ->
+      | VtQed keep ->
           let valid = VCS.get_branch_pos head in
           let rc =
             merge_proof_branch ~valid ~id:newtip x keep head in
           VCS.checkout_shallowest_proof_branch ();
-          Backtrack.record (); assert (w == VtLater);
+          Backtrack.record ();
           rc
 
       (* Side effect in a (still open) proof is replayed on all branches*)
-      | VtSideff l, w ->
+      | VtSideff (l, w) ->
           let id = VCS.new_node ~id:newtip proof_mode () in
           let new_ids =
             match (VCS.get_branch head).VCS.kind with
@@ -2961,15 +2961,13 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
               VCS.set_parsing_state id parsing_state) new_ids;
           `Ok
 
-      | VtProofMode pm, VtNow ->
+      | VtProofMode pm ->
         let proof_mode = Pvernac.lookup_proof_mode pm in
         let id = VCS.new_node ~id:newtip proof_mode () in
         VCS.commit id (mkTransCmd x [] false `MainQueue);
         VCS.set_parsing_state id head_parsing;
         Backtrack.record (); `Ok
 
-      | VtProofMode _, VtLater ->
-          anomaly(str"classifier: VtProofMode must imply VtNow.")
     end in
     let pr_rc rc = match rc with
       | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index aa16f9535d..cfeca1fa62 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -20,9 +20,13 @@ let string_of_parallel = function
        "par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
   | `No -> ""
 
-let string_of_vernac_type = function
+let string_of_vernac_when = function
+  | VtLater -> "Later"
+  | VtNow -> "Now"
+
+let string_of_vernac_classification = function
   | VtStartProof _ -> "StartProof"
-  | VtSideff _ -> "Sideff"
+  | VtSideff (_,w) -> "Sideff"^" "^(string_of_vernac_when w)
   | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
   | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)"
   | VtQed VtDrop -> "Qed(drop)"
@@ -33,13 +37,6 @@ let string_of_vernac_type = function
   | VtMeta -> "Meta "
   | VtProofMode _ -> "Proof Mode"
 
-let string_of_vernac_when = function
-  | VtLater -> "Later"
-  | VtNow -> "Now"
-
-let string_of_vernac_classification (t,w) =
-  string_of_vernac_type t ^ " " ^ string_of_vernac_when w
-
 let vtkeep_of_opaque = let open Proof_global in function
   | Opaque -> VtKeepOpaque
   | Transparent -> VtKeepDefined
@@ -67,15 +64,15 @@ let classify_vernac e =
     | VernacSetOption (_, l,_)
       when CList.exists (CList.equal String.equal l)
         options_affecting_stm_scheduling ->
-       VtSideff [], VtNow
+       VtSideff ([], VtNow)
     (* Qed *)
-    | VernacAbort _ -> VtQed VtDrop, VtLater
-    | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom), VtLater
-    | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque)), VtLater
-    | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque), VtLater
+    | VernacAbort _ -> VtQed VtDrop
+    | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom)
+    | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque))
+    | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque)
     (* Query *)
     | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
-    | VernacCheckMayEval _ -> VtQuery, VtLater
+    | VernacCheckMayEval _ -> VtQuery
     (* ProofStep *)
     | VernacProof _ 
     | VernacFocus _ | VernacUnfocus
@@ -83,27 +80,25 @@ let classify_vernac e =
     | VernacCheckGuard
     | VernacUnfocused
     | VernacSolveExistential _ ->
-        VtProofStep { parallel = `No; proof_block_detection = None }, VtLater
+        VtProofStep { parallel = `No; proof_block_detection = None }
     | VernacBullet _ ->
-        VtProofStep { parallel = `No; proof_block_detection = Some "bullet" },
-        VtLater
+        VtProofStep { parallel = `No; proof_block_detection = Some "bullet" }
     | VernacEndSubproof -> 
         VtProofStep { parallel = `No;
-                      proof_block_detection = Some "curly" },
-        VtLater
+                      proof_block_detection = Some "curly" }
     (* StartProof *)
     | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
-      VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
+      VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i)
 
     | VernacDefinition (_,({v=i},_),ProveBody _) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
       let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-      VtStartProof(guarantee, idents_of_name i), VtLater
+      VtStartProof(guarantee, idents_of_name i)
     | VernacStartTheoremProof (_,l) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
       let ids = List.map (fun (({v=i}, _), _) -> i) l in
       let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-      VtStartProof (guarantee,ids), VtLater
+      VtStartProof (guarantee,ids)
     | VernacFixpoint (discharge,l) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
@@ -114,8 +109,8 @@ let classify_vernac e =
           List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
-        then VtStartProof (guarantee,ids), VtLater
-        else VtSideff ids, VtLater
+        then VtStartProof (guarantee,ids)
+        else VtSideff (ids, VtLater)
     | VernacCoFixpoint (discharge,l) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
@@ -126,15 +121,15 @@ let classify_vernac e =
           List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
-        then VtStartProof (guarantee,ids), VtLater
-        else VtSideff ids, VtLater
+        then VtStartProof (guarantee,ids)
+        else VtSideff (ids, VtLater)
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->
         let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in
-        VtSideff ids, VtLater
+        VtSideff (ids, VtLater)
     | VernacPrimitive (id,_,_) ->
-        VtSideff [id.CAst.v], VtLater
-    | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id), VtLater
+        VtSideff ([id.CAst.v], VtLater)
+    | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
     | VernacInductive (_, _,_,l) ->
         let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with
         | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
@@ -142,12 +137,12 @@ let classify_vernac e =
            CList.map_filter (function
             | AssumExpr({v=Names.Name n},_), _ -> Some n
             | _ -> None) l) l in
-        VtSideff (List.flatten ids), VtLater
+        VtSideff (List.flatten ids, VtLater)
     | VernacScheme l ->
         let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in
-        VtSideff ids, VtLater
-    | VernacCombinedScheme ({v=id},_) -> VtSideff [id], VtLater
-    | VernacBeginSection {v=id} -> VtSideff [id], VtLater
+        VtSideff (ids, VtLater)
+    | VernacCombinedScheme ({v=id},_) -> VtSideff ([id], VtLater)
+    | VernacBeginSection {v=id} -> VtSideff ([id], VtLater)
     | VernacUniverse _ | VernacConstraint _
     | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
     | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
@@ -166,17 +161,17 @@ let classify_vernac e =
     | VernacRegister _
     | VernacNameSectionHypSet _
     | VernacComments _
-    | VernacDeclareInstance _ -> VtSideff [], VtLater
+    | VernacDeclareInstance _ -> VtSideff ([], VtLater)
     (* Who knows *)
-    | VernacLoad _ -> VtSideff [], VtNow
+    | VernacLoad _ -> VtSideff ([], VtNow)
     (* (Local) Notations have to disappear *)
-    | VernacEndSegment _ -> VtSideff [], VtNow
+    | VernacEndSegment _ -> VtSideff ([], VtNow)
     (* Modules with parameters have to be executed: can import notations *)
     | VernacDeclareModule (exp,{v=id},bl,_)
     | VernacDefineModule (exp,{v=id},bl,_,_) ->
-        VtSideff [id], if bl = [] && exp = None then VtLater else VtNow
+        VtSideff ([id], if bl = [] && exp = None then VtLater else VtNow)
     | VernacDeclareModuleType ({v=id},bl,_,_) ->
-        VtSideff [id], if bl = [] then VtLater else VtNow
+        VtSideff ([id], if bl = [] then VtLater else VtNow)
     (* These commands alter the parser *)
     | VernacDeclareCustomEntry _
     | VernacOpenCloseScope _ | VernacDeclareScope _
@@ -186,40 +181,39 @@ let classify_vernac e =
     | VernacSyntacticDefinition _
     | VernacRequire _ | VernacImport _ | VernacInclude _
     | VernacDeclareMLModule _
-    | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow
-    | VernacProofMode pm -> VtProofMode pm, VtNow
+    | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow)
+    | VernacProofMode pm -> VtProofMode pm
     | VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
       let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-      VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater
+      VtStartProof (guarantee, idents_of_name name.CAst.v)
     | VernacInstance ((name,_),_,_,_,_) ->
-      VtSideff (idents_of_name name.CAst.v), VtLater
+      VtSideff (idents_of_name name.CAst.v, VtLater)
     (* Stm will install a new classifier to handle these *)
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
     | VernacResetName _ | VernacResetInitial
-    | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
+    | VernacBackTo _ | VernacRestart -> VtMeta
     (* What are these? *)
     | VernacRestoreState _
-    | VernacWriteState _ -> VtSideff [], VtNow
+    | VernacWriteState _ -> VtSideff ([], VtNow)
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
         try Vernacextend.get_vernac_classifier s l
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
   let rec static_control_classifier v = v |> CAst.with_val (function
-    | VernacExpr (atts, e) ->
-      static_classifier ~atts e
-    | VernacTimeout (_,e) -> static_control_classifier e
-    | VernacTime (_,e) | VernacRedirect (_, e) ->
-       static_control_classifier e
-    | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+      | VernacExpr (atts, e) ->
+        static_classifier ~atts e
+      | VernacTimeout (_,e) -> static_control_classifier e
+      | VernacTime (_,e) | VernacRedirect (_, e) ->
+        static_control_classifier e
+      | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+        (* XXX why is Fail not always Query? *)
         (match static_control_classifier e with
-        | ( VtQuery | VtProofStep _ | VtSideff _
-          | VtMeta), _ as x -> x
-        | VtQed _, _ ->
-            VtProofStep { parallel = `No; proof_block_detection = None },
-            VtLater
-        | (VtStartProof _ | VtProofMode _), _ -> VtQuery, VtLater))
+         | VtQuery | VtProofStep _ | VtSideff _
+         | VtMeta as x -> x
+         | VtQed _ -> VtProofStep { parallel = `No; proof_block_detection = None }
+         | VtStartProof _ | VtProofMode _ -> VtQuery))
   in
   static_control_classifier e
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index bd1f925486..930be257e3 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -884,7 +884,7 @@ END
 {
 
 let classify_ltac2 = function
-| StrSyn _ -> Vernacextend.(VtSideff [], VtNow)
+| StrSyn _ -> Vernacextend.(VtSideff ([], VtNow))
 | StrMut _ | StrVal _ | StrPrm _  | StrTyp _ -> Vernacextend.classify_as_sideeff
 
 }
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 6a52177dd5..c7008c2a84 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -16,7 +16,11 @@ type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque
 
 type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop
 
-type vernac_type =
+type vernac_when =
+  | VtNow
+  | VtLater
+
+type vernac_classification =
   (* Start of a proof *)
   | VtStartProof of vernac_start
   (* Command altering the global state, bad for parallel
@@ -37,7 +41,7 @@ type vernac_type =
   (* To be removed *)
   | VtMeta
 and vernac_start = opacity_guarantee * Names.Id.t list
-and vernac_sideff_type = Names.Id.t list
+and vernac_sideff_type = Names.Id.t list * vernac_when
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
@@ -48,11 +52,6 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *)
 
 and proof_block_name = string (** open type of delimiters *)
 
-type vernac_when =
-  | VtNow
-  | VtLater
-type vernac_classification = vernac_type * vernac_when
-
 type typed_vernac =
   | VtDefault of (unit -> unit)
 
@@ -130,9 +129,9 @@ let get_vernac_classifier (name, i) args =
 let declare_vernac_classifier name f =
   classifiers := String.Map.add name f !classifiers
 
-let classify_as_query = VtQuery, VtLater
-let classify_as_sideeff = VtSideff [], VtLater
-let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
+let classify_as_query = VtQuery
+let classify_as_sideeff = VtSideff ([], VtLater)
+let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}
 
 type (_, _) ty_sig =
 | TyNil : (vernac_command, vernac_classification) ty_sig
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 78b7f21b0d..fd59d77237 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -32,7 +32,11 @@ type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque
 
 type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop
 
-type vernac_type =
+type vernac_when =
+  | VtNow
+  | VtLater
+
+type vernac_classification =
   (* Start of a proof *)
   | VtStartProof of vernac_start
   (* Command altering the global state, bad for parallel
@@ -53,7 +57,7 @@ type vernac_type =
   (* To be removed *)
   | VtMeta
 and vernac_start = opacity_guarantee * Names.Id.t list
-and vernac_sideff_type = Names.Id.t list
+and vernac_sideff_type = Names.Id.t list * vernac_when
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
@@ -64,11 +68,6 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *)
 
 and proof_block_name = string (** open type of delimiters *)
 
-type vernac_when =
-  | VtNow
-  | VtLater
-type vernac_classification = vernac_type * vernac_when
-
 (** Interpretation of extended vernac phrases. *)
 
 type typed_vernac =