diff --git a/_CoqProject b/_CoqProject
index 900568c5eac3877854e6f7d9ea9a896536c66b9a..d2742fd1994f27135471d50b0da4cd0746da6abc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,8 +8,6 @@
 -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 live with it.
--arg -w -arg -ambiguous-paths
 
 theories/algebra/monoid.v
 theories/algebra/cmra.v