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, 1 insertions, 1 deletions

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);