diff options
| author | Amin Timany | 2017-07-07 14:09:31 +0200 |
|---|---|---|
| committer | Amin Timany | 2017-07-31 18:05:54 +0200 |
| commit | fbe0b2645eab84012aec50e76d94e15a3fefe664 (patch) | |
| tree | 40aa5ddc6c55f889b1d92b547b5d48d02bd5e23c /test-suite | |
| parent | 17f37f42792b3150fcebb6236b9896845957b89d (diff) | |
Issue error on monomorphic cumulative inductives
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/cumulativity.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index ebf817cfc5..604da2108e 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -1,3 +1,9 @@ +Polymorphic Cumulative Inductive T1 := t1 : T1. +Fail Monomorphic Cumulative Inductive T2 := t2 : T2. + +Polymorphic Cumulative Record R1 := { r1 : T1 }. +Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}. + Set Universe Polymorphism. Set Inductive Cumulativity. Set Printing Universes. |