From f4332e3274487d9fbb28607550b8c5381bf72af8 Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <lepigre@mpi-sws.org>
Date: Thu, 6 Apr 2023 07:39:31 +0200
Subject: [PATCH] Add support for Coq version 8.17.0.
---
_CoqProject | 3 +++
coq-iris.opam | 2 +-
2 files changed, 4 insertions(+), 1 deletion(-)
diff --git a/_CoqProject b/_CoqProject
index 198cf2a91..98c2f076b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -17,6 +17,9 @@
-arg -w -arg -redundant-canonical-projection
# Fixing this one requires Coq 8.15.
-arg -w -arg -deprecated-typeclasses-transparency-without-locality
+# 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
iris/prelude/options.v
iris/prelude/prelude.v
diff --git a/coq-iris.opam b/coq-iris.opam
index 3880f2dfa..285ff423b 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -27,7 +27,7 @@ tags: [
]
depends: [
- "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
+ "coq" { (>= "8.13" & < "8.18~") | (= "dev") }
"coq-stdpp" { (= "dev.2023-03-24.1.504d165a") | (= "dev") }
]
--
GitLab