diff options
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. |