diff --git a/theories/options.v b/theories/options.v
index fa046af6c585f8afc6a29b980e0f4ffcc4bf433d..7e3856858e2a8b84e9f61b0034e0de133151aee5 100644
--- a/theories/options.v
+++ b/theories/options.v
@@ -4,6 +4,9 @@ file is *imported*, the option will only apply on the import site
 but not transitively. *)
 
 Export Set Default Proof Using "Type".
+(* FIXME: cannot enable this yet as some files disable 'Default Proof Using'.
+Export Set Suggest Proof Using. *)
+Export Set Default Goal Selector "!".
 
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.