From 26aeece9486ba279a0ec8f1e3a9d9e8faf88ac01 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 2 Oct 2024 16:54:12 +0200 Subject: [PATCH] update warning comment --- _CoqProject | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/_CoqProject b/_CoqProject index 970b6099..7a631b7f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -4,7 +4,7 @@ # Cannot use non-canonical projections as it causes massive unification failures # (https://github.com/coq/coq/issues/6294). -arg -w -arg -redundant-canonical-projection -# https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216 +# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216 -arg -w -arg -notation-incompatible-prefix theories/barrier/proof.v -- GitLab