diff options
author | 2010-10-14 17:58:31 +0200 | |
---|---|---|
committer | 2010-10-14 17:58:31 +0200 | |
commit | d06cea3ce4526736b5d32ba1780dbbc87c37c981 (patch) | |
tree | 2c2ea5a4633a41cfd4451e1eefb79c171312c881 /test-suite/bugs/closed | |
parent | aae7cec8d7f5048215b7ed06a8e94cb032bfd21a (diff) | |
parent | 8f4d4c66134804bbf2d2fe65c893b68387272d31 (diff) |
Merge commit 'upstream/8.3+dfsg' into experimental/master
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2360.v | 13 | ||||
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2375.v | 18 | ||||
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2388.v | 10 |
3 files changed, 41 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2360.v b/test-suite/bugs/closed/shouldsucceed/2360.v new file mode 100644 index 00000000..4ae97c97 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2360.v @@ -0,0 +1,13 @@ +(* This failed in V8.3 because descend_in_conjunctions built ill-typed terms *) +Definition interp (etyp : nat -> Type) (p: nat) := etyp p. + +Record Value (etyp : nat -> Type) := Mk { + typ : nat; + value : interp etyp typ +}. + +Definition some_value (etyp : nat -> Type) : (Value etyp). +Proof. + intros. + Fail apply Mk. (* Check that it does not raise an anomaly *) + diff --git a/test-suite/bugs/closed/shouldsucceed/2375.v b/test-suite/bugs/closed/shouldsucceed/2375.v new file mode 100644 index 00000000..c17c426c --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2375.v @@ -0,0 +1,18 @@ +(* In the following code, the (superfluous) lemma [lem] is responsible +for the failure of congruence. *) + +Definition f : nat -> Prop := fun x => True. + +Lemma lem : forall x, (True -> True) = ( True -> f x). +Proof. + intros. reflexivity. +Qed. + +Goal forall (x:nat), x = x. +Proof. + intros. + assert (lem := lem). + (*clear ax.*) + congruence. +Qed. + diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v new file mode 100644 index 00000000..c7926711 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2388.v @@ -0,0 +1,10 @@ +(* Error message was not printed in the correct environment *) + +Fail Parameters (A:Prop) (a:A A). + +(* This is a variant (reported as part of bug #2347) *) + +Require Import EquivDec. +Fail Program Instance bool_eq_eqdec : EqDec bool eq := + {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}. + |