diff options
Diffstat (limited to 'checker/checkInductive.ml')
| -rw-r--r-- | checker/checkInductive.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index d20eea7874..e606d60d96 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -61,7 +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_cumulative= Option.has_some mb.mind_variance; mind_entry_private = mb.mind_private; } @@ -73,7 +73,7 @@ let check_arity env ar1 ar2 = match ar1, ar2 with List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && UGraph.check_leq (universes env) template_level ar.template_level (* template_level is inferred by indtypes, so functor application can produce a smaller one *) - | (RegularArity _ | TemplateArity _), _ -> false + | (RegularArity _ | TemplateArity _), _ -> assert false let check_kelim k1 k2 = Sorts.family_leq k1 k2 @@ -139,7 +139,7 @@ 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_variance; + mind_universes; mind_variance; mind_sec_variance; mind_private; mind_typing_flags; } = (* Locally set typing flags for further typechecking *) @@ -148,7 +148,7 @@ let check_inductive env mind mb = check_positive = mb_flags.check_positive; check_universes = mb_flags.check_universes; conv_oracle = mb_flags.conv_oracle} env in - Indtypes.check_inductive env mind entry + Indtypes.check_inductive env ~sec_univs:None mind entry in let check = check mind in @@ -165,7 +165,9 @@ 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 *) + check "mind_variance" (Option.equal (Array.equal Univ.Variance.equal) + mb.mind_variance mind_variance); + check "mind_sec_variance" (Option.is_empty mind_sec_variance); ignore mind_private; (* passed through Indtypes *) ignore mind_typing_flags; |