diff --git a/_CoqProject b/_CoqProject index a47c7168d9f7f2efa1087263ceb74e7521b5cce8..2eaad25d23f7f38f275f57f450f896bfddcf3001 100644 --- a/_CoqProject +++ b/_CoqProject @@ -9,6 +9,9 @@ -arg -w -arg -argument-scope-delimiter # Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216 -arg -w -arg -notation-incompatible-prefix +# We can't do this migration yet until we require Coq 9.0 +-arg -w -arg -deprecated-from-Coq +-arg -w -arg -deprecated-dirpath-Coq stdpp/options.v stdpp/base.v