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.

---
 kernel/declarations.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index c550b0d432..ac130d018d 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -89,10 +89,6 @@ type typing_flags = {
   indices_matter: bool;
   (** The universe of an inductive type must be above that of its indices. *)
 
-  check_template : bool;
-  (* If [false] then we don't check that the universes template-polymorphic
-     inductive parameterize on are necessarily local and unbounded from below.
-     This potentially introduces inconsistencies. *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
-- 
cgit v1.2.3