From 8b15eee6125f7f8596f17e9c982fb944a5e3f9be Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 1 Apr 2018 01:15:22 +0200
Subject: [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.
---
 intf/vernacexpr.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index dc1110ad86..e029c78e49 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
-- 
cgit v1.2.3