Skip to content
Snippets Groups Projects
Commit 2e75ac23 authored by Ralf Jung's avatar Ralf Jung
Browse files

enable coercion path warning

parent 7b456885
No related branches found
No related tags found
No related merge requests found
Pipeline #26077 passed
-Q theories lrust
# We sometimes want to locally override notation (e.g. in proofmode/base.v, bi/embedding.v), and there
# is no good way to do that with scopes.
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection
......@@ -8,8 +7,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 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/lifetime/model/definitions.v
theories/lifetime/model/faking.v
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment