diff --git a/_CoqProject b/_CoqProject index 3a2d7910af2234cd8b0cc0da76c168535411cbc7..8a8ef0b08a202d7e2a222d400b22a7e5008e84d7 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 955511477b6ddb59435600228d9f6bb200658dc8..c8bedf946c839a818ce6abdf88047c2458aff04b 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}%"]