[STM] Nested Proofs Allowed has to be executed immediately

since it affects scheduling (actually the error the option lets one
silence)

stm/stm.ml

@@ -2768,7 +2768,7 @@ let allow_nested_proofs = ref false
 let _ = Goptions.declare_bool_option
     { Goptions.optdepr  = false;
       Goptions.optname  = "Nested Proofs Allowed";
-      Goptions.optkey   = ["Nested";"Proofs";"Allowed"];
+      Goptions.optkey   = Vernac_classifier.stm_allow_nested_proofs_option_name;
       Goptions.optread  = (fun () -> !allow_nested_proofs);
       Goptions.optwrite = (fun b -> allow_nested_proofs := b) }
 

stm/vernac_classifier.ml

@@ -54,13 +54,20 @@ let idents_of_name : Names.Name.t -> Names.Id.t list =
   | Names.Anonymous -> []
   | Names.Name n -> [n]
 
+let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
+
+let options_affecting_stm_scheduling =
+  [ Vernacentries.universe_polymorphism_option_name;
+    stm_allow_nested_proofs_option_name ]
+
 let classify_vernac e =
   let static_classifier ~poly e = match e with
     (* Univ poly compatibility: we run it now, so that we can just
      * look at Flags in stm.ml.  Would be nicer to have the stm
      * look at the entire dag to detect this option. *)
     | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l))
-      when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
+      when CList.exists (CList.equal String.equal l)
+        options_affecting_stm_scheduling ->
        VtSideff [], VtNow
     (* Qed *)
     | VernacAbort _ -> VtQed VtDrop, VtLater

stm/vernac_classifier.mli

@@ -25,3 +25,4 @@ val classify_as_query : vernac_classification
 val classify_as_sideeff : vernac_classification
 val classify_as_proofstep : vernac_classification
 
+val stm_allow_nested_proofs_option_name : string list