Checker: use inductive's check_template flag

And enable related test.

3 files changed, 24 insertions, 18 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
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index a67945ae94..d115744707 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -56,6 +56,9 @@ let pr_nonpositive env =
   let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in
   pr_assumptions "Inductives whose positivity is assumed" inds
 
+let pr_unsafe_template env =
+  let inds = fold_inductives  (fun c cb acc -> if not cb.mind_typing_flags.check_template then MutInd.to_string c :: acc else acc) env [] in
+  pr_assumptions "Inductives using unchecked template polymorphism" inds
 
 let print_context env =
   if !output_context then begin
@@ -67,7 +70,8 @@ let print_context env =
       str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++
-      str "* " ++ hov 0 (pr_nonpositive env)))
+      str "* " ++ hov 0 (pr_nonpositive env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_unsafe_template env)))
   end
 
 let stats env =
diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v
index 75b2a56169..fbd9c8bcba 100644
--- a/test-suite/failure/Template.v
+++ b/test-suite/failure/Template.v
@@ -1,4 +1,4 @@
-(*
+
 Module TestUnsetTemplateCheck.
   Unset Template Check.
 
@@ -15,18 +15,14 @@ Module TestUnsetTemplateCheck.
   (* Can only succeed if no template check is performed *)
   Check myind True : Prop.
 
-  Print Assumptions myind.
-  (*
-  Axioms:
-  myind is template polymorphic on all its universe parameters.
-   *)
   About myind.
-(*
-myind : Type@{Top.60} -> Type@{Top.60}
 
-myind is assumed template universe polymorphic on Top.60
-Argument scope is [type_scope]
-Expands to: Inductive Top.TestUnsetTemplateCheck.myind
-*)
+  (* test discharge puts things in the right order (by using the
+     checker on the result) *)
+  Section S.
+
+    Variables (A:Type) (a:A).
+    Inductive bb (B:Type) := BB : forall a', a = a' -> B -> bb B.
+  End S.
+
 End TestUnsetTemplateCheck.
-*)