Merge remote-tracking branch 'github/pr/360' into v8.6

Was PR#360: [stm] Remove STM-related vernaculars

1 files changed, 1 insertions, 22 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 92e4dd618e..f77a940a7e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -283,16 +283,6 @@ type bullet =
     | Star of int
     | Plus of int
 
-(** {6 Types concerning Stm} *)
-type 'a stm_vernac =
-  | JoinDocument
-  | Finish
-  | Wait
-  | PrintDag
-  | Observe of Stateid.t
-  | Command of 'a (* An out of flow command not to be recorded by Stm *)
-  | PGLast of 'a (* To ease the life of PG *)
-
 (** {6 Types concerning the module layer} *)
 
 (** Rigid / flexible module signature *)
@@ -451,9 +441,6 @@ type vernac_expr =
   | VernacRegister of lident * register_kind
   | VernacComments of comment list
 
-  (* Stm backdoor *)
-  | VernacStm of vernac_expr stm_vernac
-
   (* Proof management *)
   | VernacGoal of constr_expr
   | VernacAbort of lident option
@@ -508,7 +495,7 @@ type vernac_type =
   | VtProofStep of proof_step
   | VtProofMode of string
   | VtQuery of vernac_part_of_script * report_with
-  | VtStm of vernac_control * vernac_part_of_script
+  | VtBack of Stateid.t * vernac_part_of_script
   | VtUnknown
 and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *)
 and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
@@ -516,14 +503,6 @@ and vernac_start = string * opacity_guarantee * Id.t list
 and vernac_sideff_type = Id.t list
 and vernac_is_alias = bool
 and vernac_part_of_script = bool
-and vernac_control =
-  | VtFinish
-  | VtWait
-  | VtJoinDocument
-  | VtPrintDag
-  | VtObserve of Stateid.t
-  | VtBack of Stateid.t
-  | VtPG
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)