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-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)
|
2018-08-27 12:57:07 +02:00
|
|
|
(setq company-coq-disabled-features '(company company-defaults))))
|
