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.

1 files 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 ()