diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-07-28 13:29:36 +0200 |
|---|---|---|
| committer | Amin Timany <amintimany@gmail.com> | 2017-07-31 18:05:54 +0200 |
| commit | 3b7e7f7738737475cb0f09130b0487c85906dd2b (patch) | |
| tree | 5e3990e47e793837f0ff2b6d7b87dba310ee535d /test-suite | |
| parent | 28998d55aaaf0ad0e78477db5601a5bc9a6657b1 (diff) | |
Change the option for cumulativity
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 a978f6b90..7906a5b15 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 8854435cf..0ee85712e 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. |