Cleaner treatment of parameters in inferCumulativity

No using a mutable counter to skip them, instead we keep them in the
environment.

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.