diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-23 10:00:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-23 10:00:11 +0000 |
| commit | e8a6cf51f9671c92b90cc84473d84526e69173c8 (patch) | |
| tree | 19ee543495f1fe08f6d68d268d5cd957aea8e760 /toplevel/vernacentries.ml | |
| parent | f11fc1871babffd64e9d3be99197f91a0dfc8b69 (diff) | |
Some fine-tuning after removal of automatic imports of coercions in r13310
- Moved Global Set from Keep to Substitute to ensure it is activated
in real time and not only after the main parts of the module
- Renamed Importation into Import in option name
- Made "Print Libraries" prints the modules in the importation order
(which is the most relevant order for non-commutative declarations)
instead of load order
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13318 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 05795566a..22bfde6f1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -174,7 +174,9 @@ let print_loadpath dir = let print_modules () = let opened = Library.opened_libraries () and loaded = Library.loaded_libraries () in - let loaded_opened = list_intersect loaded opened + (* we intersect over opened to preserve the order of opened since *) + (* non-commutative operations (e.g. visibility) are done at import time *) + let loaded_opened = list_intersect opened loaded and only_loaded = list_subtract loaded opened in str"Loaded and imported library files: " ++ pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++ |