Commit 78de859d authored by MEVEL Glen's avatar MEVEL Glen

hide warning about ambiguous coercion paths

parent a18a1836
......@@ -2,6 +2,9 @@
-arg -w -arg -notation-overridden,-redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# Iris has some ambiguous coercion paths (TLC has one, too)
# which produce a lot of warnings starting with Coq 8.10.
-arg -w -arg -ambiguous-paths
theories/heap_lang/lang.v
theories/heap_lang/adequacy.v
......
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