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
:-) 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