diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-01 01:15:22 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-01 01:23:50 +0200 |
| commit | 8b15eee6125f7f8596f17e9c982fb944a5e3f9be (patch) | |
| tree | 925e8278a09b12a38108332f4872c1d434080110 /vernac | |
| parent | 2d2d16430822f1768ce4f3c62ef0750b94e4747f (diff) | |
[stm] Move VernacBacktrack to the toplevel.
This command is legacy, equivalent to `EditAt` and only used by
Emacs. We move it to the toplevel so we can kill some legacy code and
in particular the `part_of_script` hack.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 1 | ||||
| -rw-r--r-- | vernac/vernacprop.ml | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 9ff4e3302..4b99836fd 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2008,7 +2008,6 @@ let interp ?proof ~atts ~st c = | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command") | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") - | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command") (* Resetting *) | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index a837b77a3..0fdd2faaf 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -31,7 +31,6 @@ let rec has_Fail = function let is_navigation_vernac_expr = function | VernacResetInitial | VernacResetName _ - | VernacBacktrack _ | VernacBackTo _ | VernacBack _ -> true | _ -> false |