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?
You should go under the "View" menu, and tick/untick the "Display coercions" button.