diff options
| -rw-r--r-- | checker/checkInductive.ml | 5 | ||||
| -rw-r--r-- | test-suite/coqchk/inductive_functor_squash.v | 15 |
2 files changed, 19 insertions, 1 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index c823db956d..d2d1efcb2c 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -77,6 +77,9 @@ let check_arity env ar1 ar2 = match ar1, ar2 with (* template_level is inferred by indtypes, so functor application can produce a smaller one *) | (RegularArity _ | TemplateArity _), _ -> false +let check_kelim k1 k2 = + List.for_all (fun x -> List.mem_f Sorts.family_equal x k2) k1 + (* Use [eq_ind_chk] because when we rebuild the recargs we have lost the knowledge of who is the canonical version. Try with to see test-suite/coqchk/include.v *) @@ -102,7 +105,7 @@ let check_packet env mind ind check "mind_user_lc" (Array.equal Constr.equal ind.mind_user_lc mind_user_lc); check "mind_nrealargs" Int.(equal ind.mind_nrealargs mind_nrealargs); check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls); - check "mind_kelim" (List.equal Sorts.family_equal ind.mind_kelim mind_kelim); + check "mind_kelim" (check_kelim ind.mind_kelim mind_kelim); check "mind_nf_lc" (Array.equal Constr.equal ind.mind_nf_lc mind_nf_lc); (* NB: here syntactic equality is not just an optimisation, we also diff --git a/test-suite/coqchk/inductive_functor_squash.v b/test-suite/coqchk/inductive_functor_squash.v new file mode 100644 index 0000000000..9d33fafc4c --- /dev/null +++ b/test-suite/coqchk/inductive_functor_squash.v @@ -0,0 +1,15 @@ + + +Module Type T. + Parameter f : nat -> Type. +End T. + +Module F(A:T). + Inductive ind : Prop := + C : A.f 0 -> ind. +End F. + +Module A. Definition f (x:nat) := True. End A. + +Module M := F A. +(* M.ind could eliminate into Set/Type even though F.ind can't *) |