From 33742251e62a49c7996b96ca7077cf985627d14b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 15 Dec 2015 23:15:02 +0100
Subject: Proof using: do not clear unused section hyps automatically

The option is still there, but not documented since it is too
dangerous.  Hints and type classes instances are not taking cleared
variables into account.
---
 test-suite/success/proof_using.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'test-suite/success')

diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index c83f45e2a..adaa05ad0 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