The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

thanks a lot for your answers!

Locate does what I want. Print only works for notations, which consist of a 
single operator, but not for multi part notations. Locate works even if only 
a part of a notation is given (in double quotes).

Also the switch off notation menu in the IDE is quite interesting. It can 
give some interesting insights in what is going on under the hood (e.g. 
string representation). I guess it is time for me to review all the menus.

Thanks & best regards,

Michael