diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-08 15:11:34 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-09 20:27:39 +0100 |
| commit | ee573583701c8e53e8b82978998a9df93170cd79 (patch) | |
| tree | 4670034d0f36cc5103bdc87c2d0348bd51aa6a3b /test-suite/success | |
| parent | 1f2a922d52251f79a11d75c2205e6827a07e591b (diff) | |
Fix expected number of arguments for cumulative constructors.
We expected `nparams + nrealargs + consnrealargs` but the `nrealargs`
should not be there. This breaks cumulativity of constructors for any
inductive with indices (so records still work, explaining why the test
case in #6747 works).
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/cumulativity.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index dfa305dc6..3d97f27b1 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -128,3 +128,12 @@ Definition foo2@{i} : bar@{i} := let x := mkfoo in x. (* must reduce *) (* Rigid universes however should not be unified unnecessarily. *) Definition foo3@{i j|} : foo@{i} := let x := mkfoo@{j} in x. Definition foo4@{i j|} : bar@{i} := let x := mkfoo@{j} in x. + +(* Constructors for an inductive with indices *) +Module WithIndex. + Inductive foo@{i} : (Prop -> Prop) -> Prop := mkfoo: foo (fun x => x). + + Monomorphic Universes i j. + Monomorphic Constraint i < j. + Definition bar : eq mkfoo@{i} mkfoo@{j} := eq_refl _. +End WithIndex. |