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/check_stat.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'checker/check_stat.ml')

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