diff --git a/_CoqProject b/_CoqProject
index 0a078486a5f77b9a6c4f7c5dd000010fdacfe52f..cf13c3743775582b3232e6412a879e7c1f08fbf2 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -18,6 +18,10 @@
 # Disabling warnings about future coercion syntax that requires Coq 8.17
 # (https://github.com/coq/coq/pull/16230)
 -arg -w -arg -future-coercion-class-field
+# Some warnings exist only on some Coq versions
+-arg -w -arg -unknown-warning
+# Since we still support Coq 8.15, we cannot yet deal with these deprecations.
+-arg -w -arg -deprecated-since-8.18
 
 iris/prelude/options.v
 iris/prelude/prelude.v
diff --git a/iris/prelude/options.v b/iris/prelude/options.v
index 80f9b75bf13501f32ffed25321e80a669093a893..d7a84d1c155d65322e041b1a9a46aea96e6845ef 100644
--- a/iris/prelude/options.v
+++ b/iris/prelude/options.v
@@ -10,11 +10,11 @@ file is *imported*, the option will only apply on the import site
 but not transitively. *)
 From stdpp Require Export options.
 
-Export Set Suggest Proof Using. (* also warns about forgotten [Proof.] *)
+#[export] Set Suggest Proof Using. (* also warns about forgotten [Proof.] *)
 
 (* We always annotate hints with locality ([Global] or [Local]). This enforces
 that at least global hints are annotated. *)
-Export Set Warnings "+deprecated-hint-without-locality".
+#[export] Set Warnings "+deprecated-hint-without-locality".
 
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.