diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-07 05:34:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-07 05:34:24 +0000 |
| commit | 5131209a85e65c4c8619899373ea3d1ce866ba78 (patch) | |
| tree | 464eabb29419617952e1caf46f4c680e838a4886 /library | |
| parent | 7f467f7fb09abba8e0cb2dca2c50c3adc0509c59 (diff) | |
Suppression de la dépendance des .vo en le nom physique des modules
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2379 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml index 4b8fdfbc0..c9116b059 100644 --- a/library/library.ml +++ b/library/library.ml @@ -402,13 +402,17 @@ let cache_require (_,(modref,export)) = if export then m.module_exported <- true; open_module false m.module_name + (* keeps the require marker for closed section replay but removes + OS dependent fields from .vo files for cross-platform compatibility *) +let export_require ((a,b,_),e) = Some ((a,b,""),e) + let (in_require, out_require) = declare_object ("REQUIRE", { cache_function = cache_require; load_function = (fun _ -> ()); open_function = (fun _ -> ()); - export_function = (fun i -> Some i) }) + export_function = export_require }) let require_module spec qid fileopt export = (* Trop contraignant |