diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-18 12:18:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-18 12:18:05 +0200 |
| commit | 88e2da8c1b9403f5eac19df4f6c55fedca948bcc (patch) | |
| tree | 01f750142359361f800e0dc2dfe422f145f491c5 /test-suite/bugs/opened | |
| parent | 139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (diff) | |
| parent | fdd6a17b272995237c9f95fc465bb1ff6871bedc (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/3819.v | 11 |
1 files changed, 0 insertions, 11 deletions
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. |