[stm] Remove STM-related vernaculars

I think these commands never make a lot of sense on scripts other than
debugging and we have better methods now.

The last remaining command, used for the tty emulation has been renamed
to VtBack, but it should go away at some point too once the legacy
interfaces are removed.

1 files changed, 4 insertions, 18 deletions

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index dc5be08a3..f9bf9653f 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -33,10 +33,7 @@ let string_of_vernac_type = function
   | VtQuery (b,(id,route)) ->
       "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
       " route " ^ string_of_int route
-  | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) ->
-      "Stm " ^ string_of_in_script b
-  | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b
-  | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
+  | VtBack(_, b) -> "Stm Back " ^ string_of_in_script b
 
 let string_of_vernac_when = function
   | VtLater -> "Later"
@@ -55,7 +52,7 @@ let declare_vernac_classifier
 let elide_part_of_script_and_now (a, _) =
   match a with
   | VtQuery (_,id) -> VtQuery (false,id), VtNow
-  | VtStm (x, _) -> VtStm (x, false), VtNow
+  | VtBack (x, _) -> VtBack (x, false), VtNow
   | x -> x, VtNow
 
 let make_polymorphic (a, b as x) =
@@ -69,23 +66,12 @@ let set_undo_classifier f = undo_classifier := f
 
 let rec classify_vernac e =
   let static_classifier e = match e with
-    (* PG compatibility *)
-    | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
-    | VernacSetOption   ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
-      when !Flags.print_emacs -> VtStm(VtPG,false), VtNow
     (* 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 (["Universe"; "Polymorphism"],_)
     | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
-    (* Stm *)
-    | VernacStm Finish -> VtStm (VtFinish, true), VtNow
-    | VernacStm Wait -> VtStm (VtWait, true), VtNow
-    | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
-    | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow
-    | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow
-    | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x)
-    | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow
+
     (* Nested vernac exprs *)
     | VernacProgram e -> classify_vernac e
     | VernacLocal (_,e) -> classify_vernac e
@@ -98,7 +84,7 @@ let rec classify_vernac e =
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match classify_vernac e with
         | ( VtQuery _ | VtProofStep _ | VtSideff _
-          | VtStm _ | VtProofMode _ ), _ as x -> x
+          | VtBack _ | VtProofMode _ ), _ as x -> x
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
             VtNow