diff options
Diffstat (limited to 'checker/checkInductive.ml')
| -rw-r--r-- | checker/checkInductive.ml | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index c823db956d..4329b2d743 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -28,11 +28,8 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = | PrimRecord data -> Some (Some (Array.map pi1 data)) in let mind_entry_universes = match mb.mind_universes with - | Monomorphic_ind univs -> Monomorphic_ind_entry univs - | Polymorphic_ind auctx -> Polymorphic_ind_entry (AUContext.names auctx, AUContext.repr auctx) - | Cumulative_ind auctx -> - Cumulative_ind_entry (AUContext.names (ACumulativityInfo.univ_context auctx), - ACumulativityInfo.repr auctx) + | Monomorphic univs -> Monomorphic_entry univs + | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx) in let mind_entry_inds = Array.map_to_list (fun ind -> let mind_entry_arity, mind_entry_template = match ind.mind_arity with @@ -64,6 +61,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = mind_entry_params = mb.mind_params_ctxt; mind_entry_inds; mind_entry_universes; + mind_entry_variance = mb.mind_variance; mind_entry_private = mb.mind_private; } @@ -77,6 +75,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 +103,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 @@ -132,7 +133,8 @@ let check_same_record r1 r2 = match r1, r2 with let check_inductive env mind mb = let entry = to_entry mb in let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps; - mind_nparams; mind_nparams_rec; mind_params_ctxt; mind_universes; + mind_nparams; mind_nparams_rec; mind_params_ctxt; + mind_universes; mind_variance; mind_private; mind_typing_flags; } = (* Locally set the oracle for further typechecking *) @@ -154,6 +156,7 @@ let check_inductive env mind mb = check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt); ignore mind_universes; (* Indtypes did the necessary checking *) + ignore mind_variance; (* Indtypes did the necessary checking *) ignore mind_private; (* passed through Indtypes *) ignore mind_typing_flags; |