diff options
Diffstat (limited to 'checker/checkInductive.ml')
| -rw-r--r-- | checker/checkInductive.ml | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 06ee4fcc7a..a2cf44389e 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -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,16 +139,22 @@ 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 *) let mb_flags = mb.mind_typing_flags in - let env = Environ.set_typing_flags {env.env_typing_flags with check_guarded = mb_flags.check_guarded; - 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 + let env = Environ.set_typing_flags + {env.env_typing_flags with + check_guarded = mb_flags.check_guarded; + check_positive = mb_flags.check_positive; + check_universes = mb_flags.check_universes; + check_template = mb_flags.check_template; + conv_oracle = mb_flags.conv_oracle; + } + env + in + Indtypes.check_inductive env ~sec_univs:None mind entry in let check = check mind in @@ -165,7 +171,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; |