diff options
Diffstat (limited to 'test-suite/bugs/opened/HoTT_coq_033.v')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_033.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_033.v b/test-suite/bugs/opened/HoTT_coq_033.v index c4dbf74cd2..e357fce324 100644 --- a/test-suite/bugs/opened/HoTT_coq_033.v +++ b/test-suite/bugs/opened/HoTT_coq_033.v @@ -7,6 +7,8 @@ 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'). -Monomorphic Definition bar := @JMeq _ (@JMeq). +(* Note: This should not fail *) +Fail Monomorphic Definition bar := @JMeq _ (@JMeq). |