aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-04-01 01:15:22 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-04-01 01:23:50 +0200
commit8b15eee6125f7f8596f17e9c982fb944a5e3f9be (patch)
tree925e8278a09b12a38108332f4872c1d434080110 /intf
parent2d2d16430822f1768ce4f3c62ef0750b94e4747f (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 'intf')
-rw-r--r--intf/vernacexpr.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index dc1110ad8..e029c78e4 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -446,7 +446,6 @@ type nonrec vernac_expr =
| VernacRestart
| VernacUndo of int
| VernacUndoTo of int
- | VernacBacktrack of int*int*int
| VernacFocus of int option
| VernacUnfocus
| VernacUnfocused