From a50aecc7a56b7b7b1c676009f1936599366eb4ba Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 2 Sep 2014 11:37:05 +0200
Subject: Another fix than 19a7a5789c to avoid descend_in_conjunction to use
 fresh names interferring with names later generated in intropatterns (as
 introduced in 72498d6d68ac which passed "clenv_refine_in continued by pattern
 introduction" to descend_in_conjunction while only a pure clenv_refine was
 passed before). The 72498d6d68ac version was generating fresh names in the
 wrong order (morally-private names for descend_in_conjunction before
 user-level names in clenv_refine_in). The 19a7a5789c fix was introducing
 expressions not handled by the refine from logic.ml.

In particular, this fixes RelationAlgebra.
---
 test-suite/success/apply.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 48db9c41cf..7f1a8f5d45 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -489,3 +489,10 @@ split.
 exact H. (* Check that generated names are H and H0 *)
 exact H0.
 Qed.
+
+(* This failed at some time in between 18 August 2014 and 2 September 2014 *)
+
+Goal forall A B C: Prop, (True -> A -> B /\ C) -> A -> B.
+intros * H.
+apply H.
+Abort.
-- 
cgit v1.2.3