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.

1 files changed, 0 insertions, 20 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