diff options
Diffstat (limited to 'checker/checkInductive.ml')
| -rw-r--r-- | checker/checkInductive.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index a1d5aedb01..c370a77ea0 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -164,16 +164,7 @@ let check_inductive env mind mb = 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 + let env = CheckFlags.set_local_flags mb.mind_typing_flags env in Indtypes.check_inductive env ~sec_univs:None mind entry in let check = check mind in |