> 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
David Aspinall writes:
> I just committed the first version of parallel background
> compilation for Coq.
It sounds very useful! Are there some Coq users who are testing for you?
Not that I know.
H.
___
ProofGeneral-devel mailing list
Proo
Pierre Courtieu writes:
Since double hit terminator is more or less an alternative to electric
terminator, I have put them side by side in coq menu, to see if people
OK, I thought "double hit" would modify the behavior of electric
terminator.
like it, but I did not make it geenric yet
> I just came across proof-shell-pre-interrupt-hook. I can't find
> any location where this hook is run. Am I missing something?
Likely obsolete but let me check some old versions:
http://proofgeneral.inf.ed.ac.uk/trac/ticket/457
--
The University of Edinburgh is a charitable body, registered
> I just committed the first version of parallel background
> compilation for Coq.
It sounds very useful! Are there some Coq users who are testing for you?
- David
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
__
