emenel/doomemacs
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Merge pull request #2067 from rgrinberg/disable-hello-company-coq

Browse source 
lang/coq: proof-splash-enable = nil & refactor
This commit is contained in:
Henrik Lissner 2019-11-16 13:26:33 -05:00 • committed by GitHub
commit 2ce6d3a66d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 8 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

14
modules/lang/coq/config.el
View file

@ -9,7 +9,8 @@
;; tries to load `proof-site'. We prevent this by defining these two variables
;; early, in our own autoloads file.
(setq pg-init--script-full-path (locate-library "proof-general")
pg-init--pg-root (file-name-directory pg-init--script-full-path))
pg-init--pg-root (file-name-directory pg-init--script-full-path)
proof-splash-enable nil)
;;;###package coq
@ -73,14 +74,15 @@
:references #'company-coq-grep-symbol
:documentation #'company-coq-doc)
(if (not (featurep! :completion company))
(setq company-coq-disabled-features '(company company-defaults))
(setq company-coq-disabled-features '(hello company-defaults))
(if (featurep! :completion company)
(map! :map coq-mode-map [remap company-complete-common]
#'company-indent-or-complete-common)
;; `company-coq''s company defaults impose idle-completion on folks, so
;; we'll set up company ourselves.
(add-to-list 'company-coq-disabled-features 'company-defaults)
;; See https://github.com/cpitclaudel/company-coq/issues/42
(map! :map coq-mode-map [remap company-complete-common]
#'company-indent-or-complete-common))
(add-to-list 'company-coq-disabled-features 'company))
(map! :map coq-mode-map
:localleader