Update STYLE.md

Suggests a different approach to managing typeclass instances now that the "export" locality attribute is available

STYLE.md

@@ -430,15 +430,22 @@ Hint Immediate foo : typeclass_instances.
 
 ### 3.4. Local and Global Instances ###
 
-When declaring an `Instance` you should *always* use either the
-`Local` or the `Global` keyword.  The former makes the instance local
-to the current section, module, or file (although its *definition*
-will still be visible globally, it won't be in the instance database
-for typeclass resolution outside its containing section, module or
-file), while the latter puts it in the instance database globally.
-If you write `Instance` without `Local` or `Global`, Coq will
-sometimes make it local and sometimes global, so to avoid confusion it
-is better to always specify explicitly which you intend.
+Each `Instance` declaration has an associated "locality attribute".
+The `Local` attribute makes the instance local to the current section, module,
+or file (although its *definition* will still be visible globally, it won't be
+in the instance database for typeclass resolution outside its containing section,
+module or file). The `Global` attribute makes the instance available in
+any file that "loads" this file via the `Require` command,
+which is a transitive relation including all direct and indirect dependencies of the current file.
+The `#[export]` locality uses the module system to manage the scope of the typeclass hint, 
+so that the hint is available wherever the module is opened using the `Import` keyword
+(analogous to "open" in ML languages).
+
+When declaring an `Instance` you should prefer the `export` locality attribute
+to the `global` locality attribute. Inside a section, you should
+explicitly annotate instance declarations as `Local` or `#[export]`
+to avoid ambiguity. Outside a section, you may omit the annotation,
+and in this case Coq defaults to the `export` attribute since 8.18.
 
 ### 3.5. Using Typeclasses ###