summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
commit3e96002677226c0cdaa8f355938a76cfb37a722a (patch)
tree3ca96e142fdb68e464d2f5f403f315282b94f922 /test-suite/bugs/closed/shouldsucceed
parentf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff)
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2360.v13
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2375.v18
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2388.v10
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}.
+