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 d2d1efcb2c..b681fb876e 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; } @@ -91,6 +89,9 @@ let eq_recarg a1 a2 = match a1, a2 with let eq_reloc_tbl = Array.equal (fun x y -> Int.equal (fst x) (fst y) && Int.equal (snd x) (snd y)) +let eq_in_context (ctx1, t1) (ctx2, t2) = + Context.Rel.equal Constr.equal ctx1 ctx2 && Constr.equal t1 t2 + let check_packet env mind ind { mind_typename; mind_arity_ctxt; mind_arity; mind_consnames; mind_user_lc; mind_nrealargs; mind_nrealdecls; mind_kelim; mind_nf_lc; @@ -107,7 +108,7 @@ let check_packet env mind ind check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls); 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); + check "mind_nf_lc" (Array.equal eq_in_context ind.mind_nf_lc mind_nf_lc); (* NB: here syntactic equality is not just an optimisation, we also care about the shape of the terms *) @@ -135,7 +136,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 *) @@ -157,6 +159,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; |