diff options
| author | herbelin | 2008-04-15 16:35:54 +0000 |
|---|---|---|
| committer | herbelin | 2008-04-15 16:35:54 +0000 |
| commit | f907cc977bb80e3654174de03aeaed2cb4aa4a7e (patch) | |
| tree | 4df4871b13560cb50476185ab8ef16dabcc8cdac /test-suite/bugs/opened | |
| parent | a81f52f601c9851d59d0a9f53f0a46c7444fcab1 (diff) | |
Mises à jour bugs, CHANGES, code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10801 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1774.v | 18 | ||||
| -rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1775.v | 39 |
2 files changed, 0 insertions, 57 deletions
diff --git a/test-suite/bugs/opened/shouldnotfail/1774.v b/test-suite/bugs/opened/shouldnotfail/1774.v deleted file mode 100644 index 4c24b481bd..0000000000 --- a/test-suite/bugs/opened/shouldnotfail/1774.v +++ /dev/null @@ -1,18 +0,0 @@ -Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop). -Axiom plImp : forall k P Q, - pl P Q k -> forall (P':nat -> Prop), - (forall k', P k' -> P' k') -> forall (Q':nat -> Prop), - (forall k', Q k' -> Q' k') -> - pl P' Q' k. - -Definition nexists (P:nat -> nat -> Prop) : nat -> Prop := - fun k' => exists k, P k k'. - -Goal forall k (A:nat -> nat -> Prop) (B:nat -> Prop), - pl (nexists A) B k. -intros. -eapply plImp. -2:intros m' M'; econstructor; apply M'. -2:intros m' M'; apply M'. -simpl. -Admitted. diff --git a/test-suite/bugs/opened/shouldnotfail/1775.v b/test-suite/bugs/opened/shouldnotfail/1775.v deleted file mode 100644 index dab4120b96..0000000000 --- a/test-suite/bugs/opened/shouldnotfail/1775.v +++ /dev/null @@ -1,39 +0,0 @@ -Axiom pair : nat -> nat -> nat -> Prop. -Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop). -Axiom plImp : forall k P Q, - pl P Q k -> forall (P':nat -> Prop), - (forall k', P k' -> P' k') -> forall (Q':nat -> Prop), - (forall k', Q k' -> Q' k') -> - pl P' Q' k. - -Definition nexists (P:nat -> nat -> Prop) : nat -> Prop := - fun k' => exists k, P k k'. - -Goal forall s k k' m, - (pl k' (nexists (fun w => (nexists (fun b => pl (pair w w) - (pl (pair s b) - (nexists (fun w0 => (nexists (fun a => pl (pair b w0) - (nexists (fun w1 => (nexists (fun c => pl - (pair a w1) (pl (pair a c) k))))))))))))))) m. -intros. -eapply plImp; [ | eauto | intros ]. -2:econstructor. -2:econstructor. -2:eapply plImp; [ | eauto | intros ]. -3:eapply plImp; [ | eauto | intros ]. -4:econstructor. -4:econstructor. -4:eapply plImp; [ | eauto | intros ]. -5:econstructor. -5:econstructor. -5:eauto. -4:eauto. -3:eauto. -2:eauto. - -assert (X := 1). -clear X. (* very slow! *) - -simpl. (* exception Not_found *) - -Admitted. |