From 0f9b4075028073714acfd2eb0b01cb8d5b94c25a Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
Date: Tue, 6 Oct 2015 21:46:42 -0400
Subject: Put 'delete-selection t on coq-terminator-insert

delete-selection-mode requires command that insert text to be annotated
with a 'delete-selection property.
---
 coq/coq.el | 2 ++
 1 file changed, 2 insertions(+)

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)
 
-- 
cgit v1.2.3