From 84accdaea3ce094cc5d0232107d3e2ea654a76c2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 18 Sep 2017 13:27:20 +0200
Subject: Remove STM vernaculars.

---
 API/API.mli | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 901ed3528b..50fbee5298 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3676,7 +3676,7 @@ sig
                    | VtProofStep of proof_step
                    | VtProofMode of string
                    | VtQuery of vernac_part_of_script * Feedback.route_id
-                   | VtStm of vernac_control * vernac_part_of_script
+                   | VtBack of vernac_part_of_script * Stateid.t
                    | VtUnknown
    and vernac_qed_type =
      | VtKeep
@@ -3685,10 +3685,6 @@ sig
    and vernac_start = string * opacity_guarantee * Names.Id.t list
    and vernac_sideff_type = Names.Id.t list
    and vernac_part_of_script = bool
-   and vernac_control =
-     | VtWait
-     | VtJoinDocument
-     | VtBack of Stateid.t
    and opacity_guarantee =
      | GuaranteesOpacity
      | Doesn'tGuaranteeOpacity
@@ -3770,7 +3766,6 @@ sig
   type option_value
   type showable
   type bullet
-  type stm_vernac
   type comment
   type register_kind
   type locatable
@@ -3922,7 +3917,6 @@ sig
   | VernacLocate of locatable
   | VernacRegister of lident * register_kind
   | VernacComments of comment list
-  | VernacStm of stm_vernac
   | VernacGoal of Constrexpr.constr_expr
   | VernacAbort of lident option
   | VernacAbortAll
-- 
cgit v1.2.3