diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-12-11 10:22:44 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-12-11 10:22:44 +0000 |
commit | 30243d55bd7f9ec5597f0db17f955eef0c7d5c67 (patch) | |
tree | 1576bbb0da6139940040bb2e3b21e01916e89bb6 /test-suite | |
parent | 90e17b8f5c5494a41daf9f3a613e987b1515cbc3 (diff) |
Test pour le bug #1754
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10364 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1754.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/shouldnotfail/1754.v b/test-suite/bugs/opened/shouldnotfail/1754.v new file mode 100644 index 000000000..768d9c990 --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/1754.v @@ -0,0 +1,24 @@ +Axiom hp : Set. +Axiom cont : nat -> hp -> Prop. +Axiom sconj : (hp -> Prop) -> (hp -> Prop) -> hp -> Prop. +Axiom sconjImpl : forall h A B, + (sconj A B) h -> forall (A' B': hp -> Prop), + (forall h', A h' -> A' h') -> + (forall h', B h' -> B' h') -> + (sconj A' B') h. + +Definition cont' (h:hp) := exists y, cont y h. + +Lemma foo : forall h x y A, + (sconj (cont x) (sconj (cont y) A)) h -> + (sconj cont' (sconj cont' A)) h. +Proof. + intros h x y A H. + eapply sconjImpl. + 2:intros h' Hp'; econstructor; apply Hp'. + 2:intros h' Hp'; eapply sconjImpl. + 3:intros h'' Hp''; econstructor; apply Hp''. + 3:intros h'' Hp''; apply Hp''. + 2:apply Hp'. + try clear H. +Admitted. |