diff options
| -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 e357fce324..0000000000 --- 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). |