diff --git a/_CoqProject b/_CoqProject index 40d932068a6fbcef8ff7620e330f483cd4210e40..a47c7168d9f7f2efa1087263ceb74e7521b5cce8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -7,7 +7,7 @@ # Custom flags (to be kept in sync with the dune file at the root of the repo). # Fixing this one requires Coq 8.19 -arg -w -arg -argument-scope-delimiter -# 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 stdpp/options.v