summaryrefslogtreecommitdiff
path: root/test-suite/success/proof_using.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/proof_using.v')
-rw-r--r--test-suite/success/proof_using.v3
1 files changed, 2 insertions, 1 deletions
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.
-
+*)