deal with some Coq 8.18 warnings

_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

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.