Re: [PG-devel] Howto disable the double hit terminator for Coq?

2012-09-03 Thread Hendrik Tews
Pierre Courtieu writes: (define-key coq-mode-map (kbd ".") 'self-insert-command) (define-key coq-mode-map (kbd ";") 'self-insert-command) No, I want the default Proof General electric terminator thing, where one "." asserts up to the last phrase. Sorry for being not clear enough about this

Re: [PG-devel] Howto disable the double hit terminator for Coq?

2012-09-03 Thread Pierre Courtieu
:-) Good point, (define-key coq-mode-map (kbd ".") 'self-insert-command) (define-key coq-mode-map (kbd ";") 'self-insert-command) Should do the thing but I will add a customization variable. Sorry for the inconvenience, I did not think someone would notice this before I finish my experiment on t