aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/library.mli')
-rw-r--r--library/library.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/library/library.mli b/library/library.mli
index 2b7ecc664..c6bd8fe0b 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -79,8 +79,5 @@ val locate_qualified_library :
bool -> qualid -> library_location * dir_path * System.physical_path
val try_locate_qualified_library : qualid located -> dir_path * string
-(* Reserve Coq prefix for the standard library *)
-val check_coq_overwriting : dir_path -> unit
-
(*s Statistics: display the memory use of a library. *)
val mem : dir_path -> Pp.std_ppcmds