diff options
| author | Pierre-Marie Pédrot | 2018-11-03 19:41:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-03 19:41:11 +0100 |
| commit | 782736024e75a67c7dd1cbb7801b217f72f79fe5 (patch) | |
| tree | 9ab84e41d80db908a1b1efb1ec8ed541ba5f6505 | |
| parent | 2e970d6c7876963a9845cae4153fe39cac81b587 (diff) | |
| parent | baa8812294d48bf9d0e6e62a39440e9ffb2b93e2 (diff) | |
Merge PR #8877: Fix #8876: expected number of arguments for cumulative constructors
| -rw-r--r-- | checker/reduction.ml | 5 | ||||
| -rw-r--r-- | test-suite/coqchk/bug_8876.v | 19 |
2 files changed, 20 insertions, 4 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index 58a3f4e410..1158152f63 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -192,10 +192,7 @@ let convert_constructors | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2 | Cumulative_ind cumi -> let num_cnstr_args = - let nparamsctxt = - mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs - in - nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1) + mind.mind_nparams + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1) in if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then convert_universes univs u1 u2 diff --git a/test-suite/coqchk/bug_8876.v b/test-suite/coqchk/bug_8876.v new file mode 100644 index 0000000000..2d20511a04 --- /dev/null +++ b/test-suite/coqchk/bug_8876.v @@ -0,0 +1,19 @@ +(* -*- coq-prog-args: ("-noinit"); -*- *) +Require Import Coq.Init.Notations. + +Notation "x -> y" := (forall _ : x, y). + +Inductive eq {A:Type} (a:A) : A -> Prop := eq_refl : eq a a. + +Set Universe Polymorphism. +Set Polymorphic Inductive Cumulativity. +Set Printing Universes. + +(* 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. |