Stream: Coq users

Topic: Conflict between strict warnings and Search?


view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Dec 13 2020 at 18:44):

You are probably using SSReflect? Is that correct?

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Dec 13 2020 at 18:45):

You should disable that warning -ssr-search-moved.

view this post on Zulip 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: Jan 31 2023 at 13:02 UTC