From 6c683786c8100259e8c78b710e4a75974ae00eba Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Sat, 15 Apr 2017 22:10:08 +0200
Subject: Remove VernacError

---
 stm/vernac_classifier.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'stm/vernac_classifier.ml')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index fb6adaec5..c4f392f20 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -202,8 +202,7 @@ let rec classify_vernac e =
     (* What are these? *)
     | VernacToplevelControl _
     | VernacRestoreState _
-    | VernacWriteState _
-    | VernacError _ -> VtUnknown, VtNow
+    | VernacWriteState _ -> VtUnknown, VtNow
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
         try List.assoc s !classifiers l ()
-- 
cgit v1.2.3