> Actually tooltips are so useless and annoying (flickering) in coq mode
> that I wanted the disabling option to be as immediate as possible. It
> would probably be better to disable it by default and put the option
> in the settings menu.
> Fine with me.
I agree, please go ahead Pierre.
> By the way is there a "emacs gui recommendations somewhere?"
> I don't know any.
Me neither. There are recommendations about Emacs conventions scattered
through the Lisp reference manuals and apart from that I try to follow what
Emacs itself does and the standard applications it ships with.
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
ProofGeneral-devel mailing list