Avi Shinnar (Dec 13 2020 at 16:59): Avi Shinnar (Dec 13 2020 at 16:59):I tried adding to the _CoqProject file:
-arg -set -arg "Warnings=+default,ambiguous-path,typechecker"
to be strict about not having warnings in our code (except for some that occur from importing Coquelicot).
While this works, it seems to break Search for some reason.
Am I doing something wrong, or is this a bug that i should report?
Théo Zimmermann (Dec 13 2020 at 18:44):You are probably using SSReflect? Is that correct?
Théo Zimmermann (Dec 13 2020 at 18:44):In 8.12, you get warnings when using Search and SSReflect to let you know that the Search implementation changed.
Théo Zimmermann (Dec 13 2020 at 18:45):You should disable that warning -ssr-search-moved.
Avi Shinnar (Dec 13 2020 at 21:10):Théo Zimmermann said:
You should disable that warning
-ssr-search-moved.
that worked, thanks!
Last updated: Oct 05 2023 at 02:01 UTC