From 26d180fa0b27edc773fd07c73906e4ed56475200 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 16 Nov 2016 10:51:39 +0100 Subject: [stm] Remove STM-related vernaculars I think these commands never make a lot of sense on scripts other than debugging and we have better methods now. The last remaining command, used for the tty emulation has been renamed to VtBack, but it should go away at some point too once the legacy interfaces are removed. --- toplevel/vernac.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'toplevel/vernac.ml') diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index bfdae85d5..ba5bc5506 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -27,8 +27,7 @@ let rec is_navigation_vernac = function | VernacResetName _ | VernacBacktrack _ | VernacBackTo _ - | VernacBack _ - | VernacStm _ -> true + | VernacBack _ -> true | VernacRedirect (_, (_,c)) | VernacTime (_,c) -> is_navigation_vernac c (* Time Back* is harmless *) -- cgit v1.2.3