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 /kernel/reduction.ml | |
| 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 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4ecbec0ed..81fbd4f5e 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -251,11 +251,8 @@ let convert_inductives cv_pb ind nargs u1 u2 (s, check) = cv_pb ind nargs u1 u2 s, check let constructor_cumulativity_arguments (mind, ind, ctor) = - let nparamsctxt = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in - nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1) + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1) let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s = match mind.Declarations.mind_universes with |