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.

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

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index b3b3327272..cabd06735f 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -103,7 +103,6 @@ type showable =
   | ShowProofNames
   | ShowIntros of bool
   | ShowMatch of reference
-  | ShowThesis
 
 type comment =
   | CommentConstr of constr_expr
-- 
cgit v1.2.3