;; I appreciate the effort of writing a splash-screen, but the angry
;; general on the gif scares me.
(setq proof-splash-seen t)

;;; Hybrid mode is by far the best.
(setq proof-three-window-mode-policy 'hybrid)

;;; I don't know who wants to evaluate comments
;;; one-by-one, but I don't.
(setq proof-script-fly-past-comments t)

(with-eval-after-load 'coq
  ;; The most common command by far. Having a 3(!)
  ;; keys long sequence for this command is just a
  ;; crime.
  (define-key coq-mode-map "\M-n"
    #'proof-assert-next-command-interactive)

  ;; Proof navigation didn't work for me. So please
  ;; stand aside for my paragraph navigation.
  ;; https://endlessparentheses.com/meta-binds-part-2-a-peeve-with-paragraphs.html
  (define-key coq-mode-map "\M-e" nil)
  (define-key coq-mode-map "\M-a" nil)

  ;; Small convenience for commonly written commands.
  (define-key coq-mode-map "\C-c\C-m" "\nend\t")
  (define-key coq-mode-map "\C-c\C-e"
    #'endless/qed)
  (defun endless/qed ()
    (interactive)
    (unless (memq (char-before) '(?\s ?\n ?\r))
      (insert " "))
    (insert "Qed.")
    (proof-assert-next-command-interactive)))

(defun open-after-coq-command ()
  (when (looking-at-p " *(\\*")
    (open-line 1)))

(advice-add 'proof-assert-next-command-interactive
            :after #'open-after-coq-command)

(define-abbrev-table 'coq-mode-abbrev-table '())
(define-abbrev coq-mode-abbrev-table "re" "reflexivity.")
(define-abbrev coq-mode-abbrev-table "id" "induction")
(define-abbrev coq-mode-abbrev-table "si" "simpl.")
(advice-add 'proof-assert-next-command-interactive
            :before #'expand-abbrev)

(when (fboundp 'company-coq-initialize)
  (add-hook 'coq-mode-hook #'company-coq-initialize))