diff --git a/_CoqProject b/_CoqProject index 1c252fed8ab3f9361cde0f208c296a04303d0ec4..5f77c3f8d75fa496e748bebabffcd1a233afff82 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