From b4825012568dd59ed147db490fbd6f4e511db6bf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 3 Oct 2024 10:40:10 +0200
Subject: [PATCH] update dependencies; warning should be gone
---
_CoqProject | 2 --
coq-lifetime-logic.opam | 2 +-
2 files changed, 1 insertion(+), 3 deletions(-)
diff --git a/_CoqProject b/_CoqProject
index 3a2d7910..8a8ef0b0 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,8 +8,6 @@
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-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
lifetime/model/definitions.v
lifetime/model/faking.v
diff --git a/coq-lifetime-logic.opam b/coq-lifetime-logic.opam
index 95551147..c8bedf94 100644
--- a/coq-lifetime-logic.opam
+++ b/coq-lifetime-logic.opam
@@ -12,7 +12,7 @@ The lifetime logic extends Iris with a notion of "borrowing".
"""
depends: [
- "coq-iris" { (= "dev.2024-10-02.0.4320aaee") | (= "dev") }
+ "coq-iris" { (= "dev.2024-10-03.0.4871f965") | (= "dev") }
]
build: ["./make-package" "lifetime" "-j%{jobs}%"]
--
GitLab