aboutsummaryrefslogtreecommitdiff
path: root/library/global.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/global.ml')
-rw-r--r--library/global.ml2
1 files changed, 0 insertions, 2 deletions
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