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.

---
 printing/ppvernac.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 0f065e251b..5110cf7b23 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1224,8 +1224,6 @@ module Make
               (keyword "Comments" ++ spc()
                ++ prlist_with_sep sep (pr_comment pr_constr) l)
           )
-        | VernacNop ->
-          mt()
 
         (* Toplevel control *)
         | VernacToplevelControl exn ->
-- 
cgit v1.2.3