From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 26 Jan 2016 16:56:33 +0100
Subject: Imported Upstream version 8.5

---
 test-suite/success/proof_using.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'test-suite/success/proof_using.v')

diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index c83f45e2..adaa05ad 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -178,6 +178,7 @@ End Let.
 
 Check (test_let 3).
 
+(* Disabled
 Section Clear.
 
 Variable a: nat.
@@ -192,6 +193,6 @@ trivial.
 Qed.
 
 End Clear.
-
+*)
 
 
-- 
cgit v1.2.3