aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst20
-rw-r--r--stm/stm.ml4
-rw-r--r--stm/vernac_classifier.ml2
-rw-r--r--toplevel/coqloop.ml2
-rw-r--r--toplevel/g_toplevel.mlg6
-rw-r--r--vernac/g_vernac.mlg1
-rw-r--r--vernac/ppvernac.ml2
-rw-r--r--vernac/vernacentries.ml2
-rw-r--r--vernac/vernacexpr.ml1
-rw-r--r--vernac/vernacprop.ml1
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:25:43 +0000