From 800b2b1a51c77a328042f47d24e2517266029544 Mon Sep 17 00:00:00 2001
From: tslil clingman <>
Date: Sun, 12 Jan 2020 11:46:40 -0500
Subject: Changes from using bison

---
 emacs/inits/25-theorems.el | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

(limited to 'emacs/inits/25-theorems.el')

diff --git a/emacs/inits/25-theorems.el b/emacs/inits/25-theorems.el
index b72dabc..f5ab26b 100644
--- a/emacs/inits/25-theorems.el
+++ b/emacs/inits/25-theorems.el
@@ -1,4 +1,4 @@
-;; Time-stamp: <2020-01-06 20:36:12 (tslil@bison)>
+;; Time-stamp: <2020-01-08 18:37:56 (tslil@bison)>
 
 ;; -----------------------------------------------------------------------------
 ;; Coq
@@ -50,8 +50,8 @@
 (defun mike-implicify (ntimes)
   (interactive "p")
   (save-excursion
+    (re-search-backward "(\\|{")
     (dotimes (i ntimes)
-      (re-search-backward "(\\|{")
       (if (looking-at "(")
           (progn (delete-char 1)
                  (insert "{")
@@ -64,7 +64,9 @@
                (backward-char 1)
                (forward-sexp 1)
                (delete-char -1)
-               (insert ")"))))))
+               (insert ")")))
+      (re-search-forward "(\\|{")
+      (backward-char 1))))
 
 (use-package proof-general
   :ensure t
@@ -81,7 +83,8 @@
         (enlarge-window-horizontally (- (+ 7 fill-column) ww)))))
   (defun coq-local-environment ()
     (require 'corral)
-    (bind-keys ("M-i" . mike-implicify)
+    (bind-keys :map coq-mode-map
+               ("M-i" . mike-implicify)
                ("M-a" . forward-sexp)
                ("M-e" . backward-sexp)
                ("M-/" . lh-matching-delim)
@@ -93,7 +96,7 @@
                ("M-]" . corral-brackets-backward)
                ("C-(" . lh-slurp-forward)
                ("C-)" . lh-slurp-backward)
-               ("C-s" . isearch-forward-proof-mode-map))
+               ("C-s" . isearch-forward))
     (let* ((data (alist-get use-coq-env coq-env nil nil #'string-equal))
            (topdir (expand-file-name (plist-get data :topdir)))
            (binary (plist-get data :binary))
@@ -102,6 +105,7 @@
       (visit-tags-table (concat topdir "TAGS"))
       ;; Formatting
       (setq fill-column 70)
+      (visual-line-mode 1)
       (set-fringe-mode 0)
       (make-local-variable 'before-save-hook)
       (add-hook 'before-save-hook 'delete-trailing-whitespace)
-- 
cgit v1.2.3