Put 'delete-selection t on coq-terminator-insert

delete-selection-mode requires command that insert text to be annotated
with a 'delete-selection property.

1 files changed, 2 insertions, 0 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 2f9e65ca..e45076c9 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2720,6 +2720,8 @@ are non-nil at the same time, this gives priority to the former."
     ;; otherwise call this, which checks proof-electric-terminator-enable
     (proof-electric-terminator count)))
 
+(put 'coq-terminator-insert 'delete-selection t)
+
 ;; Setting the new mapping for terminator, overrides the following in proof-script:
 ;; (define-key proof-mode-map (vector (aref proof-terminal-string 0)) 'proof-electric-terminator)