From 493b5d18971c8c19eaeccfc992d1212c6479d227 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 16 Dec 2015 15:38:19 +0100
Subject: CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no
 Vernacular command is mapped.

---
 intf/vernacexpr.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 32c0f29751..0e659459e9 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -420,7 +420,6 @@ type vernac_expr =
   | VernacLocate of locatable
   | VernacRegister of lident * register_kind
   | VernacComments of comment list
-  | VernacNop
 
   (* Stm backdoor *)
   | VernacStm of vernac_expr stm_vernac
-- 
cgit v1.2.3