diff --git a/_CoqProject b/_CoqProject index a5316e76dc2151fca37eb29249a85f8d349f00b3..32c033fea19431f8a924bc5d67a517469f35d4a8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -4,6 +4,8 @@ # 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 is often incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216 +-arg -w -arg -notation-incompatible-prefix theories/barrier/proof.v theories/barrier/specification.v