diff options
Diffstat (limited to 'checker/checkInductive.ml')
| -rw-r--r-- | checker/checkInductive.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 051f51bbb3..62e732ce69 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -170,7 +170,6 @@ let check_inductive env mind mb = 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 |