diff options
| author | Enrico Tassi | 2019-07-29 13:59:37 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-07-29 13:59:37 +0200 |
| commit | fd9185ba9f72bb7631dbd0d113717ac15804451a (patch) | |
| tree | 4bc7acd28ff535a3cc38c7b7ca13f8504c2a697d /vernac | |
| parent | c7a1972e2ac492cdef8726c236a151c61ec2df96 (diff) | |
| parent | a352716c040280ed7c2cca84f0464b4081ec7727 (diff) | |
Merge PR #10574: Remove deprecated `Backtrack` command
Reviewed-by: ejgallego
Reviewed-by: gares
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 1 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 1 | ||||
| -rw-r--r-- | vernac/vernacprop.ml | 1 |
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 |