From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 test-suite/success/clear.v | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/success/clear.v

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

diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v
new file mode 100644
index 00000000..444146f7
--- /dev/null
+++ b/test-suite/success/clear.v
@@ -0,0 +1,6 @@
+Goal forall x:nat, (forall x, x=0 -> True)->True.
+  intros; eapply H.
+  instantiate (1:=(fun y => _) (S x)).
+  simpl.
+  clear x || trivial.
+Qed.
-- 
cgit v1.2.3