diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/coqchk/cumulativity.v | 2 | ||||
| -rw-r--r-- | test-suite/success/cumulativity.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v index a978f6b901..7906a5b15e 100644 --- a/test-suite/coqchk/cumulativity.v +++ b/test-suite/coqchk/cumulativity.v @@ -1,5 +1,5 @@ Set Universe Polymorphism. -Set Inductive Cumulativity. +Set Polymorphic Inductive Cumulativity. Set Printing Universes. Inductive List (A: Type) := nil | cons : A -> List A -> List A. diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 8854435cf3..0ee85712e2 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -5,7 +5,7 @@ Polymorphic Cumulative Record R1 := { r1 : T1 }. Fail Monomorphic Cumulative Inductive R2 := {r2 : T1}. Set Universe Polymorphism. -Set Inductive Cumulativity. +Set Polymorphic Inductive Cumulativity. Set Printing Universes. Inductive List (A: Type) := nil | cons : A -> List A -> List A. |