From 8689bd7078060bda79e574d6ce19e5195894b186 Mon Sep 17 00:00:00 2001
From: Johannes Hostert <jhostert@ethz.ch>
Date: Fri, 31 Jan 2025 14:07:24 +0100
Subject: [PATCH] compatibility with rocq (aka Coq) 9.0
---
_CoqProject | 3 +++
coq-simuliris.opam | 2 +-
2 files changed, 4 insertions(+), 1 deletion(-)
diff --git a/_CoqProject b/_CoqProject
index beae3548..8ab07cf5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,6 +6,9 @@
-arg -w -arg -redundant-canonical-projection
# 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
theories/logic/satisfiable.v
theories/simulation/language.v
diff --git a/coq-simuliris.opam b/coq-simuliris.opam
index 06cc5342..05fa0ef8 100644
--- a/coq-simuliris.opam
+++ b/coq-simuliris.opam
@@ -9,7 +9,7 @@ synopsis: "Local Simulation proofs, the Iris style"
depends: [
"coq-iris" { (= "dev.2025-01-25.1.8a8f05fb") | (= "dev") }
- "coq-equations" { (= "1.3+8.19") | (= "1.3.1+8.20") | (= "dev") }
+ "coq-equations" { (= "1.3+8.19") | (= "1.3.1+8.20") | (= "1.3.1+8.21") | (= "dev") }
]
build: [make "-j%{jobs}%"]
--
GitLab