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.

5 files changed, 0 insertions, 7 deletions

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