diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-15 13:29:23 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-15 13:29:23 +0200 |
| commit | e04ce4144522b71c0d6bf3df868b2f3586eb5d5f (patch) | |
| tree | de9388379d7de682c3d40984f2431022b74842d9 | |
| parent | 0a51137f7ff80afdcf216d85cd8be25a531bc39b (diff) | |
Remove HoTT bug #33, as the stdlib won't become polymorphic in the next version.
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_033.v | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_033.v b/test-suite/bugs/opened/HoTT_coq_033.v deleted file mode 100644 index e357fce32..000000000 --- a/test-suite/bugs/opened/HoTT_coq_033.v +++ /dev/null @@ -1,14 +0,0 @@ -(** JMeq should be polymorphic *) -Require Import JMeq. - -Set Implicit Arguments. - -Monomorphic Inductive JMeq' (A : Type) (x : A) -: forall B : Type, B -> Prop := - JMeq'_refl : JMeq' x x. - -(* Note: This should fail (the [Fail] should be present in the final file, even when in bugs/closed) *) -Fail Monomorphic Definition foo := @JMeq' _ (@JMeq'). - -(* Note: This should not fail *) -Fail Monomorphic Definition bar := @JMeq _ (@JMeq). |