From 6f016d1b7fdb5a4a1deba5403cd119d7c1dd070d Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 3 Aug 2017 23:25:25 +0200
Subject: [PATCH] Remove a useless vernacular command

---
 FiniteSets/representations/T.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/FiniteSets/representations/T.v b/FiniteSets/representations/T.v
index c27ebb2..f99ef53 100644
--- a/FiniteSets/representations/T.v
+++ b/FiniteSets/representations/T.v
@@ -73,8 +73,6 @@ Module Export T.
 
 End T.
 
-Check T.
-
 Section merely_dec_lem.
   Variable A : hProp.
   Context `{Univalence}.