From ef027954e62e193ab02bdd7d28254089da2babde Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 14 Sep 2009 22:11:35 +0000
Subject: Remove proof-strict-read-only-toggle call (no longer defined, and
 anyway wrong technique).  Instead use inhibit-read-only to allow write in
 possibly read-only area.

---
 coq/coq.el | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 0e551c9a..14d3b4f6 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1124,9 +1124,8 @@ tactical.  Based on idea mentioned in Coq reference manual."
                           proof-shell-last-response-output))
        (substr (match-string 1 proof-shell-last-response-output)))
     (coq-find-command-end-backward)
-    (proof-strict-read-only-toggle -1)
-    (insert (concat " as " substr))
-    (proof-strict-read-only-toggle 1)))
+    (let ((inhibit-read-only t)) 
+      (insert (concat " as " substr)))))
 
 
 (defun coq-insert-match ()
-- 
cgit v1.2.3