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 ?
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)
This solves my problem, thanks a lot!
Last updated: Feb 06 2023 at 12:04 UTC