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 /ide/MacOS | |
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 'ide/MacOS')
0 files changed, 0 insertions, 0 deletions