diff --git a/theories/options.v b/theories/options.v
index 907e59ce4882f51fc082477f554139a22b3c497b..a228ffdf6c781a64937bf2104f48c5b08d89e3b6 100644
--- a/theories/options.v
+++ b/theories/options.v
@@ -2,4 +2,6 @@
 (* Everything here should be [Export Set], which means when this
 file is *imported*, the option will only apply on the import site
 but not transitively. *)
+
 Export Set Default Proof Using "Type".
+Export Set Suggest Proof Using. (* also warns about forgotten [Proof.] *)