From b6264bb2df9b73b905af126ede49cd31abf0e7da Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Feb 2020 18:13:25 +0100
Subject: Remove the Template Check option.

---
 printing/printer.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 97e0528939..8af4d1d932 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -859,8 +859,6 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
-  | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism
-                                       on parameter universes has not been checked. *)
   | TypeInType of GlobRef.t (* a constant which relies on type in type *)
 
 type context_object =
@@ -880,13 +878,10 @@ struct
         Constant.CanOrd.compare k1 k2
     | Positive m1 , Positive m2 ->
         MutInd.CanOrd.compare m1 m2
-    | TemplatePolymorphic m1, TemplatePolymorphic m2 ->
-        MutInd.CanOrd.compare m1 m2
     | Guarded k1 , Guarded k2 ->
         GlobRef.Ordered.compare k1 k2
     | _ , Constant _ -> 1
     | _ , Positive _ -> 1
-    | _, TemplatePolymorphic _ -> 1
     | _ -> -1
 
   let compare x y =
@@ -947,9 +942,6 @@ let pr_assumptionset env sigma s =
           hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.")
       | Guarded gr ->
           hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.")
-      | TemplatePolymorphic m ->
-          hov 2 (safe_pr_inductive env m ++ spc () ++
-                 strbrk"is assumed template polymorphic on all its universe parameters.")
       | TypeInType gr ->
          hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.")
     in
-- 
cgit v1.2.3