Re: [PG-devel] proof-shell-pre-interrupt-hook ?

2012-11-14 Thread David Aspinall
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

Re: [PG-devel] Coq menu entries

2012-11-14 Thread Hendrik Tews
Pierre Courtieu pierre.court...@cnam.fr 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