Improving descend_in_conjunctions (using a combinators instead of a tactic)

what allows to better control position of side-conditions.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12612 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 24 insertions, 7 deletions

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 45da9593c..3fc8a9792 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -270,13 +270,6 @@ exact O.
 trivial.
 Qed.
 
-(* Test non-regression of (temporary) bug 1980 *)
-
-Goal True.
-try eapply ex_intro.
-trivial.
-Qed.
-
 (* Check pattern-unification on evars in apply unification *)
 
 Lemma evar : exists f : nat -> nat, forall x, f x = 0 -> x = 0.
@@ -331,3 +324,27 @@ exact (refl_equal 2).
 exact (refl_equal 3).
 exact (refl_equal 4).
 Qed.
+
+(* From 12612, descent in conjunctions is more powerful *)
+(* The following, which was failing badly in bug 1980, is now accepted
+   (even if somehow surprising) *)
+
+Goal True.
+eapply ex_intro.
+instantiate (2:=fun _ :True => True).
+instantiate (1:=I).
+exact I.
+Qed.
+
+(* The following, which were not accepted, are now accepted as
+    expected by descent in conjunctions *)
+
+Goal True.
+eapply (ex_intro (fun _ => True) I).    
+exact I.
+Qed.
+
+Goal True.
+eapply (fun (A:Prop) (x:A) => conj I x).
+exact I.
+Qed.