From 1e481bdeb09f86fdfd83d4fc7b0f7de8209dc15d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 10 Jun 2019 18:26:16 +0200
Subject: [PATCH] silence ambiguous paths warnings

---
 _CoqProject | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/_CoqProject b/_CoqProject
index 92912c9ec..d94909bca 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
-- 
GitLab