diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldfail')
| -rw-r--r-- | test-suite/bugs/closed/shouldfail/1703.v | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldfail/1898.v | 5 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldfail/1915.v | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldfail/2006.v | 23 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldfail/2251.v | 5 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldfail/2406.v | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldfail/2586.v | 5 |
7 files changed, 0 insertions, 54 deletions
diff --git a/test-suite/bugs/closed/shouldfail/1703.v b/test-suite/bugs/closed/shouldfail/1703.v deleted file mode 100644 index 6b5198cc..00000000 --- a/test-suite/bugs/closed/shouldfail/1703.v +++ /dev/null @@ -1,7 +0,0 @@ -(* Check correct binding of intros until used in Ltac *) - -Ltac intros_until n := intros until n. - -Goal forall i j m n : nat, i = 0 /\ j = 0 /\ m = 0 /\ n = 0. -intro i. -intros until i. diff --git a/test-suite/bugs/closed/shouldfail/1898.v b/test-suite/bugs/closed/shouldfail/1898.v deleted file mode 100644 index 92490eb9..00000000 --- a/test-suite/bugs/closed/shouldfail/1898.v +++ /dev/null @@ -1,5 +0,0 @@ -(* folding should not allow circular dependencies *) - -Lemma bug_fold_unfold : True. - set (h := 1). - fold h in h. diff --git a/test-suite/bugs/closed/shouldfail/1915.v b/test-suite/bugs/closed/shouldfail/1915.v deleted file mode 100644 index a96a482c..00000000 --- a/test-suite/bugs/closed/shouldfail/1915.v +++ /dev/null @@ -1,6 +0,0 @@ - -Require Import Setoid. - -Goal forall x, impl True (x = 0) -> x = 0 -> False. -intros x H E. -rewrite H in E.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldfail/2006.v b/test-suite/bugs/closed/shouldfail/2006.v deleted file mode 100644 index 91a16f95..00000000 --- a/test-suite/bugs/closed/shouldfail/2006.v +++ /dev/null @@ -1,23 +0,0 @@ -(* Take the type constraint on Record into account *) - -Definition Type1 := Type. -Record R : Type1 := { p:Type1 }. (* was accepted before trunk revision 11619 *) - -(* -Remarks: - -- The behaviour was inconsistent with the one of Inductive, e.g. - - Inductive R : Type1 := Build_R : Type1 -> R. - - was correctly refused. - -- CoRN makes some use of the following configuration: - - Definition CProp := Type. - Record R : CProp := { ... }. - - CoRN may have to change the CProp definition into a notation if the - preservation of the former semantics of Record type constraints - turns to be required. -*) diff --git a/test-suite/bugs/closed/shouldfail/2251.v b/test-suite/bugs/closed/shouldfail/2251.v deleted file mode 100644 index 642717f4..00000000 --- a/test-suite/bugs/closed/shouldfail/2251.v +++ /dev/null @@ -1,5 +0,0 @@ -(* Check that rewrite does not apply to single evars *) - -Lemma evar_rewrite : (forall a : nat, a = 0 -> True) -> True. -intros; eapply H. (* goal is ?30 = nil *) -rewrite plus_n_Sm. diff --git a/test-suite/bugs/closed/shouldfail/2406.v b/test-suite/bugs/closed/shouldfail/2406.v deleted file mode 100644 index 112ea2bb..00000000 --- a/test-suite/bugs/closed/shouldfail/2406.v +++ /dev/null @@ -1,3 +0,0 @@ -(* Check correct handling of unsupported notations *) -Notation "''" := (fun x => x) (at level 20). -Definition crash_the_rooster f := . diff --git a/test-suite/bugs/closed/shouldfail/2586.v b/test-suite/bugs/closed/shouldfail/2586.v deleted file mode 100644 index 6111a641..00000000 --- a/test-suite/bugs/closed/shouldfail/2586.v +++ /dev/null @@ -1,5 +0,0 @@ -Require Import Setoid SetoidClass Program. - -Goal forall `(Setoid nat) x y, x == y -> S x == S y. - intros. - clsubst H0.
\ No newline at end of file |