diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 23:11:11 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 23:11:11 +0100 |
commit | 5f989f48eaaf5e13568fce9849f40bc554ca0166 (patch) | |
tree | 2e425ede76c1522294e992fb270694b63bbd9624 | |
parent | 020c3448cc71618c3e74f64ae6217113072d1bbd (diff) | |
parent | ee573583701c8e53e8b82978998a9df93170cd79 (diff) |
Merge PR #6946: Fix expected number of arguments for cumulative constructors.
-rw-r--r-- | kernel/reduction.ml | 7 | ||||
-rw-r--r-- | test-suite/success/cumulativity.v | 9 |
2 files changed, 11 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 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. |