diff options
| author | herbelin | 2003-10-08 10:32:08 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-08 10:32:08 +0000 |
| commit | 402dbb2ac9632e5745f194e891ea09a16a282084 (patch) | |
| tree | 78ef9f53afed1dbb314f48b6cc82707c6b9c1e16 /library | |
| parent | 5fd4535eb5af11cf89b94d3929110e7866df0d8e (diff) | |
Mise en place d'un mecanisme ne chargeant pas les preuves opaques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4539 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 25 |
1 files changed, 15 insertions, 10 deletions
diff --git a/library/library.ml b/library/library.ml index bc74043449..c450114b9e 100644 --- a/library/library.ml +++ b/library/library.ml @@ -339,10 +339,13 @@ let with_magic_number_check f a = spc () ++ str"It is corrupted" ++ spc () ++ str"or was compiled with another version of Coq.") +let lighten_library m = + if !Options.dont_load_proofs then lighten_library m else m + let mk_library md f digest = { library_name = md.md_name; library_filename = f; - library_compiled = md.md_compiled; + library_compiled = lighten_library md.md_compiled; library_objects = md.md_objects; library_deps = md.md_deps; library_imports = md.md_imports; @@ -371,13 +374,16 @@ let rec intern_library (dir, f) = (str ("The file " ^ f ^ " contains library") ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); - compunit_cache := CompilingLibraryMap.add dir m !compunit_cache; - try - List.iter (intern_mandatory_library dir) m.library_deps; - m - with e -> - compunit_cache := CompilingLibraryMap.remove dir !compunit_cache; - raise e + intern_and_cache_library dir m + +and intern_and_cache_library dir m = + compunit_cache := CompilingLibraryMap.add dir m !compunit_cache; + try + List.iter (intern_mandatory_library dir) m.library_deps; + m + with e -> + compunit_cache := CompilingLibraryMap.remove dir !compunit_cache; + raise e and intern_mandatory_library caller (dir,d) = let m = intern_absolute_library_from dir in @@ -422,8 +428,7 @@ let rec_intern_by_filename_only id f = m'.library_filename); m.library_name with Not_found -> - compunit_cache := CompilingLibraryMap.add m.library_name m !compunit_cache; - List.iter (intern_mandatory_library m.library_name) m.library_deps; + let m = intern_and_cache_library m.library_name m in m.library_name let locate_qualified_library qid = |