From d21f89df7dce4bbef9e01941abc26806b53a010d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 16 Dec 2020 18:59:36 +0100
Subject: [PATCH] Silent some warnings (as in Iris).

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

diff --git a/_CoqProject b/_CoqProject
index 1c252fe..5f77c3f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,8 @@
 -Q theories actris
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
+# Coq emits warnings when a custom entry is reimported, this is too noisy.
+-arg -w -arg -custom-entry-overriden
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
-- 
GitLab