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

8 files changed, 20 insertions, 112 deletions

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 680da7f54..dbcd8630b 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -724,9 +724,6 @@ let rec tmpp v loc =
   | VernacComments (cl) ->
       xmlComment loc (List.flatten (List.map pp_comment cl))
 
-  (* Stm backdoor *)
-  | VernacStm _ as x -> xmlTODO loc x
-
   (* Proof management *)
   | VernacGoal _ as x -> xmlTODO loc x
   | VernacAbort _ as x -> xmlTODO loc x
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 92e4dd618..f77a940a7 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].*)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 9b52d1bf3..4ba9eeefa 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -64,16 +64,6 @@ GEXTEND Gram
       | IDENT "Local"; v = vernac_poly -> VernacLocal (true, v)
       | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v)
 
-      (* Stm backdoor *)
-      | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument
-      | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish
-      | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait
-      | IDENT "Stm"; IDENT "PrintDag"; "." -> VernacStm PrintDag
-      | IDENT "Stm"; IDENT "Observe"; id = INT; "." ->
-          VernacStm (Observe (Stateid.of_int (int_of_string id)))
-      | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v)
-      | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v)
-
       | v = vernac_poly -> v ]
     ]
   ;
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 3494ad006..a6b1c97f5 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -538,22 +538,6 @@ module Make
       | VernacLocal (local, v) ->
         return (pr_locality local ++ spc() ++ pr_vernac_body v)
 
-      (* Stm *)
-      | VernacStm JoinDocument ->
-        return (keyword "Stm JoinDocument")
-      | VernacStm PrintDag ->
-        return (keyword "Stm PrintDag")
-      | VernacStm Finish ->
-        return (keyword "Stm Finish")
-      | VernacStm Wait ->
-        return (keyword "Stm Wait")
-      | VernacStm (Observe id) ->
-        return (keyword "Stm Observe " ++ str(Stateid.to_string id))
-      | VernacStm (Command v) ->
-        return (keyword "Stm Command " ++ pr_vernac_body v)
-      | VernacStm (PGLast v) ->
-        return (keyword "Stm PGLast " ++ pr_vernac_body v)
-
       (* Proof management *)
       | VernacAbortAll ->
         return (keyword "Abort All")
diff --git a/stm/stm.ml b/stm/stm.ml
index e387e6322..0ddaf604a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -989,7 +989,7 @@ end = struct (* {{{ *)
     try
       match v with
       | VernacResetInitial ->
-          VtStm (VtBack Stateid.initial, true), VtNow
+          VtBack (Stateid.initial, true), VtNow
       | VernacResetName (_,name) ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           (try
@@ -997,20 +997,20 @@ end = struct (* {{{ *)
               fold_until (fun b (id,_,label,_,_) ->
                 if b then `Stop id else `Cont (List.mem name label))
               false id in
-            VtStm (VtBack oid, true), VtNow
+            VtBack (oid, true), VtNow
           with Not_found ->
-            VtStm (VtBack id, true), VtNow)
+            VtBack (id, true), VtNow)
       | VernacBack n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
-          VtStm (VtBack oid, true), VtNow
+          VtBack (oid, true), VtNow
       | VernacUndo n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun n (id,_,_,tactic,undo) ->
             let value = (if tactic then 1 else 0) - undo in
             if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
-          VtStm (VtBack oid, true), VtLater
+          VtBack (oid, true), VtLater
       | VernacUndoTo _
       | VernacRestart as e ->
           let m = match e with VernacUndoTo m -> m | _ -> 0 in
@@ -1027,16 +1027,16 @@ end = struct (* {{{ *)
             0 id in
           let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
-          VtStm (VtBack oid, true), VtLater
+          VtBack (oid, true), VtLater
       | VernacAbortAll ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun () (id,vcs,_,_,_) ->
             match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
             () id in
-          VtStm (VtBack oid, true), VtLater
+          VtBack (oid, true), VtLater
       | VernacBacktrack (id,_,_)
       | VernacBackTo id ->
-          VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow
+          VtBack (Stateid.of_int id, not !Flags.print_emacs), VtNow
       | _ -> VtUnknown, VtNow
     with
     | Not_found ->
@@ -2428,22 +2428,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
       prerr_endline (fun () ->
         "  classified as: " ^ string_of_vernac_classification c);
       match c with
-      (* PG stuff *)    
-      | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
-      | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater")
-      (* Joining various parts of the document *)
-      | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
-      | VtStm (VtFinish, b),       VtNow -> finish (); `Ok
-      | VtStm (VtWait, b),     VtNow -> finish (); wait (); `Ok
-      | VtStm (VtPrintDag, b), VtNow ->
-          VCS.print ~now:true (); `Ok
-      | VtStm (VtObserve id, b),   VtNow -> observe id; `Ok
-      | VtStm ((VtObserve _ | VtFinish | VtJoinDocument
-                |VtPrintDag |VtWait),_), VtLater ->
-          anomaly(str"classifier: join actions cannot be classified as VtLater")
-      
       (* Back *)
-      | VtStm (VtBack oid, true), w ->
+      | VtBack(oid, true), w ->
           let id = VCS.new_node ~id:newtip () in
           let { mine; others } = Backtrack.branches_of oid in
           let valid = VCS.get_branch_pos head in
@@ -2462,12 +2448,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
           VCS.checkout_shallowest_proof_branch ();
           VCS.commit id (Alias (oid,x));
           Backtrack.record (); if w == VtNow then finish (); `Ok
-      | VtStm (VtBack id, false), VtNow ->
+      | VtBack (id, false), VtNow ->
           prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
           Backtrack.backto id;
           VCS.checkout_shallowest_proof_branch ();
           Reach.known_state ~cache:(interactive ()) id; `Ok
-      | VtStm (VtBack id, false), VtLater ->
+      | VtBack (id, false), VtLater ->
           anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
 
       (* Query *)
@@ -2604,15 +2590,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
       | VtUnknown, VtLater ->
           anomaly(str"classifier: VtUnknown must imply VtNow")
     end in
-    (* Proof General *)
-    begin match expr with 
-      | VernacStm (PGLast _) ->
-        if not (VCS.Branch.equal head VCS.Branch.master) then
-          vernac_interp Stateid.dummy
-            { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0;
-              expr = VernacShow (ShowGoal OpenSubgoals) }
-      | _ -> ()
-    end;
     prerr_endline (fun () -> "processed }}}");
     VCS.print ();
     rc
@@ -2674,8 +2651,8 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
     let clas = classify_vernac ast in
     let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
     match clas with
-    | VtStm (w,_), _ ->
-       ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow))
+    | VtBack (w,_), _ ->
+       ignore(process_transaction ~tty:false aast (VtBack (w,false), VtNow))
     | _ ->
        ignore(process_transaction
          ~tty:false aast (VtQuery (false,report_with), VtNow)))
@@ -2822,7 +2799,7 @@ let interp verb (loc,e) =
     let print_goals =
       verb && match clas with
        | VtQuery _, _ -> false
-       | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
+       | (VtProofStep _ | VtBack (_, _) | VtStartProof _), _ -> true
        | _ -> not !Flags.coqtop_ui in
     try finish ~print_goals ()
     with e ->
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
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index bfdae85d5..ba5bc5506 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -27,8 +27,7 @@ let rec is_navigation_vernac = function
   | VernacResetName _
   | VernacBacktrack _
   | VernacBackTo _
-  | VernacBack _
-  | VernacStm _ -> true
+  | VernacBack _ -> true
   | VernacRedirect (_, (_,c))
   | VernacTime (_,c) ->
       is_navigation_vernac c (* Time Back* is harmless *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 230e62607..f0e63aa7c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1941,7 +1941,6 @@ let interp ?proof ~loc locality poly c =
   | VernacTime _ -> assert false
   | VernacRedirect _ -> assert false
   | VernacTimeout _ -> assert false
-  | VernacStm _ -> assert false
 
   | VernacError e -> raise e
 
@@ -2209,9 +2208,6 @@ let interp ?(verbosely=true) ?proof (loc,c) =
       aux ?locality ~polymorphism:b isprogcmd c
     | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice"
     | VernacLocal _ -> CErrors.error "Locality specified twice"
-    | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c
-    | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c
-    | VernacStm _ -> assert false (* Done by Stm *)
     | VernacFail v ->
         with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v)
     | VernacTimeout (n,v) ->