Stream: Coq users

Topic: Set Impredicative

view this post on Zulip Étienne Miquey (Nov 03 2020 at 18:05):

Hi all, this might a very dumb question, I know that Coq can be called with the -impredicative-set option, but is there a way to do this interactively? The bottom line of my question is: if I want Set to be impredicative in my IDE (in my case ProofGeneral), do I need to reconfigure the way Coq is called for each session or is there any better solution ?

view this post on Zulip Jasper Hugunin (Nov 03 2020 at 18:10):

There may be a ProofGeneral specific answer, but if you put -arg -impredicative-set in your _CoqProject file, most IDEs should pick it up. (some documentation)

view this post on Zulip Étienne Miquey (Nov 03 2020 at 18:14):

This solves my problem, thanks a lot!

Last updated: Apr 20 2024 at 15:01 UTC