From e69b5f0a036648e997d9ce36b8b4fe277a542e8f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 14 Sep 2023 14:29:07 +0200
Subject: [PATCH] deal with some Coq 8.18 warnings

---
 _CoqProject            | 4 ++++
 iris/prelude/options.v | 4 ++--
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 0a078486a..cf13c3743 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 80f9b75bf..d7a84d1c1 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.
-- 
GitLab