From 6cd14bf253f681d0465f8dce1d84a54a4f104d9c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Jun 2017 11:22:38 +0200
Subject: Remove non-working Show Tree and Show Node commands.

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

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index c928e0bbbf..b3b3327272 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -97,11 +97,9 @@ type locatable =
 type showable =
   | ShowGoal of goal_reference
   | ShowProof
-  | ShowNode
   | ShowScript
   | ShowExistentials
   | ShowUniverses
-  | ShowTree
   | ShowProofNames
   | ShowIntros of bool
   | ShowMatch of reference
-- 
cgit v1.2.3