awesome-emacs/doomemacs
1
0
Fork 0
mirror of https://github.com/doomemacs/doomemacs synced 2025-09-12 15:36:53 -05:00
Code Issues Packages Projects Releases Wiki Activity

fix(coq): corfu integration w/ company-coq

Browse Source 
Close: #8491
Co-authored-by: qcfu-bu <qcfu-bu@users.noreply.github.com>
This commit is contained in:
Henrik Lissner
2025-09-11 23:28:24 -04:00
parent 6fcdb49225
commit 05137e14a5
1 changed files with 3 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
modules/lang/coq/config.el
View File

@@ -77,18 +77,15 @@
:references #'company-coq-grep-symbol
:documentation #'company-coq-doc)
(setq company-coq-disabled-features '(hello company-defaults spinner))
(setq company-coq-disabled-features '(hello company company-defaults spinner))
(cond ((modulep! :completion corfu)
;; HACK: company-coq activates `company-mode', though it's not really
;; needed when we're relying on Corfu, hence these hacks:
(add-hook! 'coq-mode-local-vars-hook
(defun +coq-init-capf-completion-h ()
(when (bound-and-true-p company-mode)
(company-mode -1))
(add-hook 'completion-at-point-functions
(cape-company-to-capf 'company-coq-master-backend)
nil t)))
(dolist (b '(company-coq-master-backend company-coq-math-symbols-backend))
(add-to-list 'completion-at-point-functions (cape-company-to-capf b)))))
(defadvice! +coq--proof-goto-point-advice (&rest _)
:override #'company-coq--proof-goto-point-advice
(when (bound-and-true-p company-candidates)