Configuration updates

gnus-settings.el

@@ -136,6 +136,10 @@ BAE Systems"))))
       (to-address . "sw-dev@lists.riscv.org")
       (to-list . "sw-dev@lists.riscv.org")
       (list-identifier . "\\[riscv-sw\\]"))
+     ("list\\.coq\\.fiat$ "
+      (to-address . "fiat@lists.csail.mit.edu")
+      (to-list . "fiat@lists.csail.mit.edu")
+      (list-identifier . "\\[Fiat\\]"))
      ("list\\.gsoc\\.mentors$"
       (to-address . "google-summer-of-code-mentors-list@googlegroups.com")
       (to-list . "google-summer-of-code-mentors-list@googlegroups.com")
@@ -191,7 +195,8 @@ BAE Systems"))))
       (gcc-self . t))
      ("list\\.bahai\\.tarjuman"
       (to-address . "tarjuman@bahai-library.com")
-      (to-list . "tarjuman@bahai-library.com"))
+      (to-list . "tarjuman@bahai-library.com")
+      (list-identifier . "\\[tj\\]"))
      ("list\\.emacs\\.devel$"
       (to-address . "emacs-devel@gnu.org")
       (to-list . "emacs-devel@gnu.org")

init.el

@@ -2939,7 +2939,8 @@ Inspired by Erik Naggum's `recursive-edit-with-single-window'."
   :bind ("C-c e m" . macrostep-expand))
 
 (use-package magit
-  :load-path "site-lisp/magit/lisp"
+  :load-path ("site-lisp/magit/lisp"
+              "site-lisp/with-editor")
   :bind (("C-x g" . magit-status)
          ("C-x G" . magit-status-with-prefix))
   :preface
@@ -3340,15 +3341,16 @@ Inspired by Erik Naggum's `recursive-edit-with-single-window'."
 
   :config
   (use-package company-coq
-    :disabled t
     :load-path "site-lisp/company-coq"
     :commands company-coq-mode
     :preface
     (use-package company-math
       :load-path "site-lisp/company-math"
+      :defer t
       :preface
       (use-package math-symbols-lists
-        :load-path "site-lisp/math-symbol-lists"))
+        :load-path "site-lisp/math-symbol-lists"
+        :defer t))
     :config
     (unbind-key "M-<return>" company-coq-map))
 
@@ -3364,7 +3366,7 @@ Inspired by Erik Naggum's `recursive-edit-with-single-window'."
        (holes-mode -1)
        (whitespace-mode 1)
        ;; (ggtags-mode 1)
-       ;; (set-input-method "Agda")
+       (set-input-method "Agda")
        ;; (proof-unicode-tokens-enable 1)
        (add-hook 'proof-shell-extend-queue-hook
                  (lambda ()
@@ -3381,6 +3383,7 @@ Inspired by Erik Naggum's `recursive-edit-with-single-window'."
                             (interactive)
                             (proof-layout-windows)
                             (proof-prf)) coq-mode-map)
+    (bind-key "C-c C-a C-r" #'coq-SearchRewrite coq-mode-map)
     (bind-key "C-c C-a C-s" #'coq-SearchConstant coq-mode-map)
     (unbind-key "C-c h" coq-mode-map))
 

settings.el

@@ -287,6 +287,9 @@
     ("^ \\*Minibuf-.*\\*$" "^\\*Summary" "^\\*Article" "^#")))
  '(clean-buffer-list-kill-regexps (quote (".*")))
  '(column-number-mode t)
+ '(company-coq-disabled-features
+   (quote
+    (hello unicode-math-backend refman-tactic-abbrevs-backend refman-vernac-abbrevs-backend dynamic-symbols-backend)))
  '(company-coq-prettify-symbols-alist
    (quote
     (("|-" . 8866)