aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/check.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/check.ml')
-rw-r--r--checker/check.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 88306e214..03a18280a 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -264,7 +264,7 @@ let try_locate_qualified_library qid =
(*s Loading from disk to cache (preparation phase) *)
let raw_intern_library =
- snd (System.raw_extern_intern Coq_config.vo_magic_number ".vo")
+ snd (System.raw_extern_intern Coq_config.vo_magic_number)
let with_magic_number_check f a =
try f a