diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-21 14:22:36 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-21 14:22:36 +0000 |
| commit | f43d96aec71449e3b75e9fd732e87694cec5db8f (patch) | |
| tree | 593eff77bb330585bc5b604d3f7aba186204d55d /checker/check.ml | |
| parent | 7f3a79cd9426b009021e2096805f94c5641988da (diff) | |
Removing mandatory suffixes for library files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 2 |
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 |