diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-05 16:47:03 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-05 16:47:03 +0000 |
| commit | ac2ca408aef1759e4682d989a40ab332068edcdb (patch) | |
| tree | c33bd5f94b5da11544706492d5746e8894c05f0a /library/library.ml | |
| parent | 98db1b73f6ab89763ef386a2055528db91e4e152 (diff) | |
Lib.node: merge OpenedModtype and OpenedModule, same for Closed...
This allows more sharing of code (cf. start_module / end_module)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14452 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/library/library.ml b/library/library.ml index 447d53610..9c602adbb 100644 --- a/library/library.ml +++ b/library/library.ml @@ -543,7 +543,7 @@ let set_xml_require f = xml_require := f let require_library_from_dirpath modrefl export = let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in let modrefl = List.map fst modrefl in - if Lib.is_modtype () || Lib.is_module () then + if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> @@ -562,7 +562,7 @@ let require_library qidl export = let require_library_from_file idopt file export = let modref,needed = rec_intern_library_from_file idopt file in let needed = List.rev needed in - if Lib.is_modtype () || Lib.is_module () then begin + if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,[modref],None)); Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) export @@ -578,7 +578,7 @@ let import_module export (loc,qid) = try match Nametab.locate_module qid with | MPfile dir -> - if Lib.is_modtype () || Lib.is_module () || not export then + if Lib.is_module_or_modtype () || not export then add_anonymous_leaf (in_import (dir, export)) else add_anonymous_leaf (in_import (dir, export)) |