Checker: use inductive's check_template flag

And enable related test.

1 files changed, 5 insertions, 1 deletions

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 =