making holes.el cleaner, with the help of Stefan Monnier. I had to

adapt coq.el to these modifications.

2 files changed, 4 insertions, 10 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index d2e31539..29fc9b96 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -221,7 +221,7 @@
      ["fun3          f3<C-BS>" (holes-insert-and-expand "f3") t]
      ["fun4          f4<C-BS>" (holes-insert-and-expand "f4") t]
      ""
-     ["if then else  if<C-BS>"  (holes-insert-and-expand "li") t]
+     ["if then else  if<C-BS>"  (holes-insert-and-expand "if") t]
      ["let in        li<C-BS>"  (holes-insert-and-expand "li") t]
      ""
      ["match         m<C-BS>"  (holes-insert-and-expand "m") t]
diff --git a/coq/coq.el b/coq/coq.el
index d034ff92..cbc5a056 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -106,7 +106,7 @@ To disable coqc being called (and use only make), set this to nil."
   (interactive  "sSection name: ")
   (let ((p (point)))
     (insert "Section " s ".\n#\nEnd " s ".")
-    (holes-replace-string-by-holes-backward-move-point 1 holes-empty-hole-string)
+    (holes-replace-string-by-holes-backward p)
     (goto-char p)
     (holes-set-point-next-hole-destroy))
 )
@@ -128,10 +128,10 @@ To disable coqc being called (and use only make), set this to nil."
     (if (string-equal typkind "")
         (progn
           (insert mods " " s ".\n#\nEnd " s ".")
-          (holes-replace-string-by-holes-backward-move-point 1 holes-empty-hole-string)
+          (holes-replace-string-by-holes-backward p)
           (goto-char p))
       (insert mods " " s " " typkind " #.\n#\nEnd " s ".")
-      (holes-replace-string-by-holes-backward-move-point 2 holes-empty-hole-string)
+      (holes-replace-string-by-holes-backward p)
       (goto-char p)
       (holes-set-point-next-hole-destroy))
     )
@@ -639,12 +639,6 @@ Based on idea mentioned in Coq reference manual."
 ;; mode: you can use this (C-c C-l) to do what binding below did.
 ;;(define-key coq-keymap [(control f3)] 'coq-three-b)
 
-; This is arguable, but completion with a three key shortcut is bad, 
-; and the default meta-/ is bad on some keyboards (especially french ones)
-(define-key global-map [(control backspace)] 'expand-abbrev)
-;; da: do you also want a key for unexpand-abbrev?  (maybe just undo is ok)
-
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Indentation                                                    ;;