From 916a8dc2c6b1dd8400d5c44b5d9c7fc793cc0e97 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 16 Jul 2015 21:40:42 +0200 Subject: Remove old test file for #3819 (now fixed). --- test-suite/bugs/opened/3819.v | 11 ----------- 1 file changed, 11 deletions(-) delete mode 100644 test-suite/bugs/opened/3819.v (limited to 'test-suite/bugs/opened') diff --git a/test-suite/bugs/opened/3819.v b/test-suite/bugs/opened/3819.v deleted file mode 100644 index 7105a6587..000000000 --- a/test-suite/bugs/opened/3819.v +++ /dev/null @@ -1,11 +0,0 @@ -Set Universe Polymorphism. - -Record Op := { t : Type ; op : t -> t }. - -Canonical Structure OpType : Op := Build_Op Type (fun X => X). - -Lemma test1 (X:Type) : eq (op OpType X) X. -Proof eq_refl. - -Lemma test2 (A:Type) : eq (op _ A) A. -Fail Proof eq_refl. -- cgit v1.2.3