diff options
Diffstat (limited to 'checker/checkInductive.ml')
| -rw-r--r-- | checker/checkInductive.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 4f4527ca12..d20eea7874 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -75,8 +75,7 @@ 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 +let check_kelim k1 k2 = Sorts.family_leq k1 k2 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost the knowledge of who is the canonical version. @@ -143,8 +142,12 @@ let check_inductive env mind mb = mind_universes; mind_variance; mind_private; mind_typing_flags; } = - (* Locally set the oracle for further typechecking *) - let env = Environ.set_oracle env mb.mind_typing_flags.conv_oracle in + (* 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 in let check = check mind in |