Warning : “Set this option from the IDE menu instead” in coq

42 Views Asked by At

I'm studying the Chapter "Imp" of Software foundation. I runned the command Unset Printing Coercions. in Coq Ide, the coq Message warned me that "Set this option from the IDE menu instead" and obviously the command doesn't work. I guess maybe this command will work in the Coq prompt environment, But I want to know what I should do if I want to use "Unset Printing" command in Coq Ide?

1

There are 1 best solutions below

0
On BEST ANSWER

You should go under the "View" menu, and tick/untick the "Display coercions" button.