my emacs init file for coq

init.el

(defun load-if-exists (file) "load a file if it exists"
  (if (file-exists-p file) (load-file file) ()))

(load-if-exists "~/.emacs.d/ProofGeneral/generic/proof-site.el")
(custom-set-variables
 ;; custom-set-variables was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 '(coq-double-hit-enable t)
 '(inhibit-startup-screen t)
 '(proof-three-window-mode-policy (quote hybrid))
 '(show-paren-mode t))

(delete-selection-mode 1)

(defun coq-set-up () (set-input-method "Agda"))

(add-hook 'coq-mode-hook 'coq-set-up)

;; Load company-coq when opening Coq files
(add-hook 'coq-mode-hook #'company-coq-mode)

(load-if-exists "~/tuareg-master/tuareg-site-file.el")

(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/"))
(when (< emacs-major-version 24)
  (add-to-list 'package-archives '("gnu" . "http://elpa.gnu.org/packages/")))
(package-initialize)

(load-theme 'monokai t)

(load-if-exists "~/.emacs.d/agda-input.el")
(require 'agda-input)

(global-set-key [home] 'beginning-of-line)
(global-set-key [end] 'end-of-line)