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.

---
 library/global.ml  | 2 --
 library/global.mli | 1 -
 2 files changed, 3 deletions(-)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index fbbe09301b..8706238f5a 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -192,8 +192,6 @@ let is_polymorphic r = Environ.is_polymorphic (env()) r
 
 let is_template_polymorphic r = is_template_polymorphic (env ()) r
 
-let is_template_checked r = is_template_checked (env ()) r
-
 let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r
 
 let is_type_in_type r = is_type_in_type (env ()) r
diff --git a/library/global.mli b/library/global.mli
index b6bd69c17c..0198ac5952 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -150,7 +150,6 @@ val is_joined_environment : unit -> bool
 
 val is_polymorphic : GlobRef.t -> bool
 val is_template_polymorphic : GlobRef.t -> bool
-val is_template_checked : GlobRef.t -> bool
 val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list
 val is_type_in_type : GlobRef.t -> bool
 
-- 
cgit v1.2.3