Skip to content
Snippets Groups Projects
Commit c5f3b5d4 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

disable ambiguous-paths warnings

ssreflect doesn't care about these, so we don't want to see them when
importing `util.int`
parent 7265fc4e
No related branches found
No related tags found
1 merge request!300silence some warnings
...@@ -27,7 +27,7 @@ commonCoqProject: ...@@ -27,7 +27,7 @@ commonCoqProject:
@echo "# Automatically created by make, do not edit" > $(COQ_PROJ) @echo "# Automatically created by make, do not edit" > $(COQ_PROJ)
@echo "# (edit Makefile instead)" >> $(COQ_PROJ) @echo "# (edit Makefile instead)" >> $(COQ_PROJ)
@echo "" >> $(COQ_PROJ) @echo "" >> $(COQ_PROJ)
@echo "-arg \"-w -notation-overriden,-parsing,-projection-no-head-constant\"" >> $(COQ_PROJ) @echo "-arg \"-w -notation-overriden,-parsing,-projection-no-head-constant,-ambiguous-paths\"" >> $(COQ_PROJ)
@echo "" >> $(COQ_PROJ) @echo "" >> $(COQ_PROJ)
allCoqProject: commonCoqProject allCoqProject: commonCoqProject
......
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