diff --git a/_CoqProject b/_CoqProject
index 92912c9ecf935c6f54fd6fdc5ad6749fdf9e8636..d94909bca82971e7975c804d6bc1ba5c6f81f1fb 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,6 +8,8 @@
 -arg -w -arg -convert_concl_no_check
 # "Declare Scope" does not exist yet in 8.9.
 -arg -w -arg -undeclared-scope
+# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
+-arg -w -arg -ambiguous-paths
 
 theories/algebra/monoid.v
 theories/algebra/cmra.v