From 8fece563228264511511ff5483de69511d117e81 Mon Sep 17 00:00:00 2001 From: Jeremy Kaplan Date: Sun, 6 Dec 2015 13:13:41 -0500 Subject: [PATCH] Remove proof general from emacs --- emacs/init.el | 7 ------- 1 file changed, 7 deletions(-) diff --git a/emacs/init.el b/emacs/init.el index 175ee57..6347424 100644 --- a/emacs/init.el +++ b/emacs/init.el @@ -79,9 +79,6 @@ '(initial-scratch-message "") '(menu-bar-mode nil) '(mouse-wheel-mode nil) - '(proof-assistants (quote (coq))) - '(proof-splash-enable nil) - '(proof-three-window-mode-policy (quote hybrid)) '(require-final-newline t) '(scheme-program-name "mit-scheme") '(show-paren-delay 0) @@ -97,7 +94,6 @@ ;; Your init file should contain only one such instance. ;; If there is more than one, they won't work right. '(hl-line ((t (:background "black")))) - '(proof-locked-face ((t (:underline nil :weight bold)))) '(tuareg-font-lock-operator-face ((t (:inherit font-lock-keyword-face))))) (require 'autopair) @@ -283,9 +279,6 @@ they line up with the line containing the corresponding opening bracket." (add-to-list 'custom-theme-load-path "~/.emacs.d/themes") (load-theme 'jdkaplan t) -;; Proof General -(load-file "/usr/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el") - ;; sup (add-to-list 'auto-mode-alist '("/sup.*eml$" . message-mode)) (add-hook 'message-mode-hook