From 4326f5272ce595f93cda0fcafc81bf75bb435f0d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 18:35:57 +0200
Subject: [PATCH] Remove `-ambiguous-paths` option.

---
 _CoqProject | 2 --
 1 file changed, 2 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 900568c5e..d2742fd19 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
-- 
GitLab