Remove deprecated `Backtrack` command

It has been deprecated since 8.4. The documentation was incorrect since
at least 8.5 (the last two arguments were ignored).

`Backtrack m n p` was a synonym for `BackTo m`

We also move `BackTo` handling to coqtop, since it is not meant to be
part of the document.

10 files changed, 6 insertions, 35 deletions

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 5f3e82938d..774732825a 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -870,26 +870,6 @@ interactively, they cannot be part of a vernacular file loaded via
    have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if
    necessary.
 
-   .. cmdv:: Backtrack @num @num @num
-      :name: Backtrack
-
-      .. deprecated:: 8.4
-
-      :cmd:`Backtrack` is a *deprecated* form of
-      :cmd:`BackTo` which allows explicitly manipulating the proof environment. The
-      three numbers represent the following:
-
-      + *first number* : State label to reach, as for :cmd:`BackTo`.
-      + *second number* : *Proof state number* to unbury once aborts have been done.
-        |Coq| will compute the number of :cmd:`Undo` to perform (see Chapter :ref:`proofhandling`).
-      + *third number* : Number of :cmd:`Abort` to perform, i.e. the number of currently
-        opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`).
-
-   .. exn:: Invalid backtrack.
-
-      The destination state label is unknown.
-
-
 .. _quitting-and-debugging:
 
 Quitting and debugging
diff --git a/stm/stm.ml b/stm/stm.ml
index d5e6e6fd8b..69dbebbc57 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1073,7 +1073,7 @@ let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t =
   *)
   let is_filtered_command = function
     | VernacResetName _ | VernacResetInitial | VernacBack _
-    | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
+    | VernacRestart | VernacUndo _ | VernacUndoTo _
     | VernacAbortAll | VernacAbort _ -> true
     | _ -> false
   in
@@ -1216,8 +1216,6 @@ end = struct (* {{{ *)
             match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
             () id in
           oid
-      | VernacBackTo id ->
-          Stateid.of_int id
       | _ -> anomaly Pp.(str "incorrect VtMeta classification")
     with
     | Not_found ->
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 8750a64ccc..5af576dad2 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -193,7 +193,7 @@ let classify_vernac e =
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
     | VernacResetName _ | VernacResetInitial
-    | VernacBackTo _ | VernacRestart -> VtMeta
+    | VernacRestart -> VtMeta
     (* What are these? *)
     | VernacRestoreState _
     | VernacWriteState _ -> VtSideff ([], VtNow)
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index e49b1c0c07..2673995a86 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -383,7 +383,7 @@ let rec vernac_loop ~state =
   try
     let input = top_buffer.tokens in
     match read_sentence ~state input with
-    | Some (VernacBacktrack(bid,_,_)) ->
+    | Some (VernacBackTo bid) ->
       let bid = Stateid.of_int bid in
       let doc, res = Stm.edit_at ~doc:state.doc bid in
       assert (res = `NewTip);
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index fed337ab03..1a1537113e 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -17,7 +17,7 @@ open Vernacexpr
 
 (* Vernaculars specific to the toplevel *)
 type vernac_toplevel =
-  | VernacBacktrack of int * int * int
+  | VernacBackTo of int
   | VernacDrop
   | VernacQuit
   | VernacControl of vernac_control
@@ -54,8 +54,8 @@ GRAMMAR EXTEND Gram
   vernac_toplevel: FIRST
     [ [ IDENT "Drop"; "." -> { Some VernacDrop }
       | IDENT "Quit"; "." -> { Some VernacQuit }
-      | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
-        { Some (VernacBacktrack (n,m,p)) }
+      | IDENT "BackTo"; n = natural; "." ->
+        { Some (VernacBackTo n) }
       (* show a goal for the specified proof state *)
       | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." ->
           { Some (VernacShowGoal {gid; sid}) }
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 15f9e0328c..ad5d98669d 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1141,7 +1141,6 @@ GRAMMAR EXTEND Gram
       | IDENT "Reset"; id = identref -> { VernacResetName id }
       | IDENT "Back" -> { VernacBack 1 }
       | IDENT "Back"; n = natural -> { VernacBack n }
-      | IDENT "BackTo"; n = natural -> { VernacBackTo n }
 
 (* Tactic Debugger *)
       |	IDENT "Debug"; IDENT "On" ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e25118e0a8..0eb0b1b6f6 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -669,8 +669,6 @@ let string_of_definition_object_kind = let open Decls in function
         return (
           if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i
         )
-      | VernacBackTo i ->
-        return (keyword "BackTo" ++ pr_intarg i)
 
     (* State management *)
       | VernacWriteState s ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c048c7d83..9af8d8b67c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2298,7 +2298,6 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacResetName _
   | VernacResetInitial
   | VernacBack _
-  | VernacBackTo _
   | VernacAbort _ ->
     anomaly (str "type_vernac")
   (* Syntax *)
@@ -2630,7 +2629,6 @@ and interp_expr ?proof ~atts ~st c =
   | VernacResetName _  -> anomaly (str "VernacResetName not handled by Stm.")
   | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.")
   | VernacBack _       -> anomaly (str "VernacBack not handled by Stm.")
-  | VernacBackTo _     -> anomaly (str "VernacBackTo not handled by Stm.")
 
   (* This one is possible to handle here *)
   | VernacAbort id    -> CErrors.user_err  (str "Abort cannot be used through the Load command")
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 6f09d9a39b..0968632c2d 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -359,7 +359,6 @@ type nonrec vernac_expr =
   | VernacResetName of lident
   | VernacResetInitial
   | VernacBack of int
-  | VernacBackTo of int
 
   (* Commands *)
   | VernacCreateHintDb of string * bool
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 1dd8164ebc..747998c6cc 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -32,7 +32,6 @@ let rec has_Fail v = v |> CAst.with_val (function
 let is_navigation_vernac_expr = function
   | VernacResetInitial
   | VernacResetName _
-  | VernacBackTo _
   | VernacBack _ -> true
   | _ -> false