2018-08-27 12:57:07 +02:00
|
|
|
;;; lang/coq/config.el -*- lexical-binding: t; -*-
|
|
|
|
|
|
2018-08-31 03:31:58 +02:00
|
|
|
;; `coq'
|
|
|
|
|
(setq proof-electric-terminator-enable t)
|
2018-08-27 15:35:18 +02:00
|
|
|
|
2019-03-02 01:56:32 -05:00
|
|
|
;; We've replaced coq-mode abbrevs with yasnippet snippets (in the snippets
|
|
|
|
|
;; library included with Doom).
|
2018-10-06 23:45:09 +02:00
|
|
|
(setq coq-mode-abbrev-table '())
|
|
|
|
|
|
2019-09-07 17:00:23 +09:00
|
|
|
(map! :after coq-mode
|
|
|
|
|
:map coq-mode-map
|
|
|
|
|
:localleader
|
|
|
|
|
"]" #'proof-assert-next-command-interactive
|
|
|
|
|
"[" #'proof-undo-last-successful-command
|
|
|
|
|
"." #'proof-goto-point
|
|
|
|
|
(:prefix ("l" . "layout")
|
|
|
|
|
"c" #'pg-response-clear-displays
|
|
|
|
|
"l" #'proof-layout-windows
|
|
|
|
|
"p" #'proof-prf)
|
|
|
|
|
(:prefix ("p" . "proof")
|
|
|
|
|
"i" #'proof-interrupt-process
|
|
|
|
|
"p" #'proof-process-buffer
|
|
|
|
|
"q" #'proof-shell-exit
|
|
|
|
|
"r" #'proof-retract-buffer)
|
|
|
|
|
(:prefix ("a" . "about/print/check")
|
|
|
|
|
"a" #'coq-Print
|
|
|
|
|
"A" #'coq-Print-with-all
|
|
|
|
|
"b" #'coq-About
|
|
|
|
|
"B" #'coq-About-with-all
|
|
|
|
|
"c" #'coq-Check
|
|
|
|
|
"C" #'coq-Check-show-all
|
|
|
|
|
"f" #'proof-find-theorems
|
|
|
|
|
(:prefix ("i" . "implicits")
|
|
|
|
|
"b" #'coq-About-with-implicits
|
|
|
|
|
"c" #'coq-Check-show-implicits
|
|
|
|
|
"i" #'coq-Print-with-implicits))
|
|
|
|
|
(:prefix ("g" . "goto")
|
|
|
|
|
"e" #'proof-goto-command-end
|
|
|
|
|
"l" #'proof-goto-end-of-locked
|
|
|
|
|
"s" #'proof-goto-command-start)
|
|
|
|
|
(:prefix ("i" . "insert")
|
|
|
|
|
"c" #'coq-insert-command
|
|
|
|
|
"e" #'coq-end-Section
|
|
|
|
|
"i" #'coq-insert-intros
|
|
|
|
|
"r" #'coq-insert-requires
|
|
|
|
|
"s" #'coq-insert-section-or-module
|
|
|
|
|
"t" #'coq-insert-tactic
|
|
|
|
|
"T" #'coq-insert-tactical))
|
2019-03-02 01:56:32 -05:00
|
|
|
|
2018-08-27 12:57:07 +02:00
|
|
|
(after! company-coq
|
2018-12-03 22:23:57 -05:00
|
|
|
(set-popup-rule! "^\\*\\(?:response\\|goals\\)\\*" :ignore t)
|
2018-08-27 13:57:00 +02:00
|
|
|
(set-lookup-handlers! 'company-coq-mode
|
|
|
|
|
:definition #'company-coq-jump-to-definition
|
2018-08-27 14:11:14 +02:00
|
|
|
:references #'company-coq-grep-symbol
|
2018-08-27 13:57:00 +02:00
|
|
|
:documentation #'company-coq-doc)
|
2018-08-31 03:32:25 +02:00
|
|
|
(unless (featurep! :completion company)
|
2019-09-07 17:00:23 +09:00
|
|
|
(setq company-coq-disabled-features '(company company-defaults)))
|
|
|
|
|
|
|
|
|
|
(map! :map coq-mode-map
|
|
|
|
|
:localleader
|
|
|
|
|
(:prefix ("i" . "insert")
|
|
|
|
|
"l" #'company-coq-lemma-from-goal
|
|
|
|
|
"m" #'company-coq-insert-match-construct)
|
|
|
|
|
"ao" #'company-coq-occur
|
|
|
|
|
(:prefix ("h" . "help")
|
|
|
|
|
"e" #'company-coq-document-error
|
|
|
|
|
"E" #'company-coq-browse-error-messages
|
|
|
|
|
"h" #'company-coq-doc)))
|
