From 3813ba5229cf42597cd30a08e842e0832e5253cb Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Jun 2017 11:25:26 +0200
Subject: Remove Show Thesis command which was never implemented.

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

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 81f41cba13..9d28bc4f84 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -568,7 +568,6 @@ open Decl_kinds
           | ShowProofNames -> keyword "Show Conjectures"
           | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
           | ShowMatch id -> keyword "Show Match " ++ pr_reference id
-          | ShowThesis -> keyword "Show Thesis"
         in
         return (pr_showable s)
       | VernacCheckGuard ->
-- 
cgit v1.2.3