diff options
| -rw-r--r-- | library/goptions.ml | 2 | ||||
| -rw-r--r-- | pretyping/classops.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
3 files changed, 6 insertions, 4 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 75771a52ec..5b18195987 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -249,7 +249,7 @@ let declare_option cast uncast let (gdecl_obj,_) = (* "Global": survives section and modules. *) declare_object {(default_object ("G "^nickname key)) with cache_function = (fun (_,v) -> write v); - classify_function = (fun v -> Keep v); + classify_function = (fun v -> Substitute v); discharge_function = (fun (_,v) -> Some v); load_function = (fun _ (_,v) -> write v)} in diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 282f181ebb..9fd94c75b8 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -342,8 +342,8 @@ open Goptions let _ = declare_bool_option { optsync = true; - optname = "automatic importation of coercions"; - optkey = ["Automatic";"Coercions";"Importation"]; + optname = "automatic import of coercions"; + optkey = ["Automatic";"Coercions";"Import"]; optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 05795566ae..22bfde6f18 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 () ++ |