From 4b7c0d2caad07f7d1199f37f86ae9830c09d81ca Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 16 Feb 2018 16:15:59 +0100 Subject: Cleaner treatment of parameters in inferCumulativity No using a mutable counter to skip them, instead we keep them in the environment. --- test-suite/success/cumulativity.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'test-suite') 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. -- cgit v1.2.3