From 8b15eee6125f7f8596f17e9c982fb944a5e3f9be Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
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.
---
 printing/ppvernac.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 7df0a0c94..9dce65374 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -591,8 +591,6 @@ open Decl_kinds
         )
       | VernacUndoTo i ->
         return (keyword "Undo" ++ spc() ++ keyword "To" ++ pr_intarg i)
-      | VernacBacktrack (i,j,k) ->
-        return (keyword "Backtrack" ++  spc() ++ prlist_with_sep sep int [i;j;k])
       | VernacFocus i ->
         return (keyword "Focus" ++ pr_opt int i)
       | VernacShow s ->
-- 
cgit v1.2.3