From 72201ba9afb95ed0bfdd9e9e2cdeb089b7224a76 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 6 Jan 2020 14:35:08 +0100
Subject: Checker: use inductive's check_template flag

And enable related test.
---
 checker/checkInductive.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'checker/checkInductive.ml')

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
-- 
cgit v1.2.3