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...

2 files changed, 15 insertions, 17 deletions

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 =