diff options
| author | Pierre-Marie Pédrot | 2019-02-02 17:48:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-02 17:48:02 +0100 |
| commit | 8eeb5d6004a4d9bb8fbd776ac4c8273adb2887a6 (patch) | |
| tree | fe05667312ad548813e84334efaea68b9091f45e /checker | |
| parent | 0d4b9df02c37c7107e9cdc085a8b7b2a6039b9bf (diff) | |
| parent | d3d142f406239b6e528d27454d1b3f4e3d6fd4ea (diff) | |
Merge PR #9250: coqchk: fix check for kelim with functors
Ack-by: mattam82
Reviewed-by: ppedrot
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 |