From f3091cc36df45fe575d03854d04b5d9c373a3f8e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Oct 2024 10:01:13 +0200
Subject: [PATCH] silence some warnings on coq.dev that we cannot fix yet

---
 _CoqProject | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/_CoqProject b/_CoqProject
index a47c7168..2eaad25d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -9,6 +9,9 @@
 -arg -w -arg -argument-scope-delimiter
 # Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
 -arg -w -arg -notation-incompatible-prefix
+# We can't do this migration yet until we require Coq 9.0
+-arg -w -arg -deprecated-from-Coq
+-arg -w -arg -deprecated-dirpath-Coq
 
 stdpp/options.v
 stdpp/base.v
-- 
GitLab