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 /stm/vernac_classifier.ml | |
| 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 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 9a8af3a58..a78323323 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -183,7 +183,7 @@ let classify_vernac e = | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ | VernacResetName _ | VernacResetInitial - | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow + | VernacBackTo _ | VernacRestart -> VtMeta, VtNow (* What are these? *) | VernacRestoreState _ | VernacWriteState _ -> VtSideff [], VtNow |