The Coq mailing list

[Wendy Verbruggen <verbruwj AT cs.tcd.ie>]

Hi all,

I have a problem running CoqIDE with the option -impredicative-set on  
MacOS X. I have installed version 8.1pl2 from the Coq download page  
(using the .dmg file for coq and for coqide) and they both seem to be  
working fine.

However, I need to run CoqIDE with option -impredicative-set but when  
I run the command

/Applications/CoqIde.app/Contents/MacOS/coqide - impredicative-set

it seems to completely ignore this option. It starts CoqIDE alright,  
but the -impredicative-set option is off.

Does anyone know how to give an option to CoqIDE when installed using  
the .dmg files?

(It works fine on another Mac machine where I have manually compiled  
Coq. This means the coqide executable is not in an .app folder, so  
maybe that is the problem?).

Thanks,
Wendy