From 2c96be02dfa0a6169856a844dfc36b7f1053d0c5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 3 Sep 2014 10:32:50 +0200
Subject: Yes another remaining clearing bug with 'apply in'.

---
 test-suite/success/apply.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 7f1a8f5d45..e10f621aa3 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -496,3 +496,17 @@ Goal forall A B C: Prop, (True -> A -> B /\ C) -> A -> B.
 intros * H.
 apply H.
 Abort.
+
+(* This failed between 2 and 3 September 2014 *)
+
+Goal forall A B C D:Prop, (A<->B)/\(C<->D) -> A -> B.
+intros.
+apply H in H0.
+pose proof I as H1. (* Test that H1 does not exist *)
+Abort.
+
+Goal forall A B C D:Prop, (A<->B)/\(C<->D) -> A.
+intros.
+apply H.
+pose proof I as H0. (* Test that H0 does not exist *)
+Abort.
-- 
cgit v1.2.3