Commit d21f89df authored by Robbert Krebbers's avatar Robbert Krebbers

Silent some warnings (as in Iris).

parent 00f9af1c
Pipeline #40289 failed with stage
in 15 minutes and 20 seconds
-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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment