From bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 24 Sep 2014 22:40:11 +0200
Subject: Update test-suite files.

---
 test-suite/bugs/opened/1773.v | 10 ----------
 test-suite/bugs/opened/3657.v | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 33 insertions(+), 10 deletions(-)
 delete mode 100644 test-suite/bugs/opened/1773.v
 create mode 100644 test-suite/bugs/opened/3657.v

(limited to 'test-suite/bugs/opened')

diff --git a/test-suite/bugs/opened/1773.v b/test-suite/bugs/opened/1773.v
deleted file mode 100644
index 4aabf19c98..0000000000
--- a/test-suite/bugs/opened/1773.v
+++ /dev/null
@@ -1,10 +0,0 @@
-Goal forall B C : nat -> nat -> Prop, forall k, C 0 k ->
-  (exists A, (forall k', C A k' -> B A k') -> B A k).
-Proof.
-  intros B C k H.
-  econstructor.
-  intros X.
-  apply X.
-  apply H.
-Qed.
-
diff --git a/test-suite/bugs/opened/3657.v b/test-suite/bugs/opened/3657.v
new file mode 100644
index 0000000000..6faec0765e
--- /dev/null
+++ b/test-suite/bugs/opened/3657.v
@@ -0,0 +1,33 @@
+(* Set Primitive Projections. *)
+Class foo {A} {a : A} := { bar := a; baz : bar = bar }.
+Arguments bar {_} _ {_}.
+Instance: forall A a, @foo A a.
+intros; constructor.
+abstract reflexivity.
+Defined.
+Goal @bar _ Set _ = (@bar _ (fun _ : Set => Set) _) nat.
+Proof.
+  Check (bar Set).
+  Check (bar (fun _ : Set => Set)).
+  Fail change (bar (fun _ : Set => Set)) with (bar Set). (* Error: Conversion test raised an anomaly *)
+
+Abort.
+
+
+Module A.
+Universes i j.
+Constraint i < j.
+Variable  foo : Type@{i}.
+Goal Type@{i}.
+  Fail let t := constr:(Type@{j}) in
+  change Type with t.
+Abort.
+
+Goal Type@{j}.
+  Fail let t := constr:(Type@{i}) in
+  change Type with t.
+  let t := constr:(Type@{i}) in
+  change t. exact foo.
+Defined.
+
+End A.
-- 
cgit v1.2.3