aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-16 16:15:59 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-16 16:18:14 +0100
commit4b7c0d2caad07f7d1199f37f86ae9830c09d81ca (patch)
tree0eaa583f56381a328cd2785d219ba4777db2f0e3 /test-suite
parent507cd85244db835f13bc65cb9b92aa903180989c (diff)
Cleaner treatment of parameters in inferCumulativity
No using a mutable counter to skip them, instead we keep them in the environment.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/success/cumulativity.v10
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 1fb3abfe4..e05762477 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -124,3 +124,13 @@ Inductive Mut1 A :=
with Mut2 A :=
| Base2 : Type -> Mut2 A
| Node2 : Mut1 A -> Mut2 A.
+
+(* If we don't reduce T while inferring cumulativity for the
+ constructor we will see a Rel and believe i is irrelevant. *)
+Inductive withparams@{i j} (T:=Type@{i}:Type@{j}) := mkwithparams : T -> withparams.
+
+Definition withparams_co@{i i' j|i < i', i' < j} : withparams@{i j} -> withparams@{i' j}
+ := fun x => x.
+
+Fail Definition withparams_not_irr@{i i' j|i' < i, i' < j} : withparams@{i j} -> withparams@{i' j}
+ := fun x => x.