From e8a6cf51f9671c92b90cc84473d84526e69173c8 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 23 Jul 2010 10:00:11 +0000 Subject: 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 --- library/goptions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library') 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 -- cgit v1.2.3