From a352716c040280ed7c2cca84f0464b4081ec7727 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Jul 2019 18:25:08 +0200
Subject: 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.
---
 doc/sphinx/proof-engine/vernacular-commands.rst | 20 --------------------
 1 file changed, 20 deletions(-)

(limited to 'doc')

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
-- 
cgit v1.2.3