diff options
| author | Gaëtan Gilbert | 2020-01-06 14:35:08 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-27 14:12:52 +0100 |
| commit | 72201ba9afb95ed0bfdd9e9e2cdeb089b7224a76 (patch) | |
| tree | 689b991242ee441c15ef244a85b80f0912eeeebe /checker/checkInductive.ml | |
| parent | 506b35913103c17e4d27663aa0f977452d5815b0 (diff) | |
Checker: use inductive's check_template flag
And enable related test.
Diffstat (limited to 'checker/checkInductive.ml')
| -rw-r--r-- | checker/checkInductive.ml | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index e606d60d96..a2cf44389e 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -144,10 +144,16 @@ let check_inductive env mind mb = = (* 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 = 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 |