diff options
| author | Gaëtan Gilbert | 2018-12-19 12:43:23 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-19 12:43:23 +0100 |
| commit | d3d142f406239b6e528d27454d1b3f4e3d6fd4ea (patch) | |
| tree | 698fa2735529982d7a10ccaf711b554d0262d0db /checker | |
| parent | 2cad4dec40cef2aecb19c5a0e5a1368392be8d88 (diff) | |
coqchk: fix check for kelim with functors
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checkInductive.ml | 5 |
1 files changed, 4 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 |