Made the side-conditions of lemmas always come last when chaining "apply in"

in presence of destruction of conjunctive types.


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

1 files changed, 29 insertions, 5 deletions

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 7f00417148..45da9593c2 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -297,13 +297,37 @@ reflexivity.
 exact I.
 Qed.
 
-(* Check chaining of "apply in" on the last subgoal (assuming that
-   side conditions come first) *)
+(* Check that "apply" is chained on the last subgoal of each lemma and
+   that side conditions come first (as it is the case since 8.2) *)
 
-Lemma chaining :
-  forall B C D : Prop, (True -> B -> C) -> (C -> D) -> B -> D.
+Lemma chaining : 
+  forall A B C : Prop,
+  (1=1 -> (2=2 -> A -> B) /\ True) ->
+  (3=3 -> (True /\ (4=4 -> C -> A))) -> C -> B.
 Proof.
 intros.
-apply H, H0 in H1; auto.
+apply H, H0.
+exact (refl_equal 1).
+exact (refl_equal 2).
+exact (refl_equal 3).
+exact (refl_equal 4).
+assumption.
 Qed.
 
+(* Check that the side conditions of "apply in", even when chained and
+   used through conjunctions, come last (as it is the case for single
+   calls to "apply in" w/o destruction of conjunction since 8.2) *)
+
+Lemma chaining_in :
+  forall A B C : Prop, 
+  (1=1 -> True /\ (B -> 2=2 -> 5=0)) ->
+  (3=3 -> (A -> 4=4 -> B) /\ True) -> A -> 0=5.
+Proof.
+intros.
+apply H0, H in H1 as ->.
+exact (refl_equal 0).
+exact (refl_equal 1).
+exact (refl_equal 2).
+exact (refl_equal 3).
+exact (refl_equal 4).
+Qed.