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