Added a popup rule to ignore proof general popups

This commit is contained in:
Elijah Malaby 2018-12-02 13:22:42 -05:00
parent abc7ca84d8
commit dcbcc4d1e7

View file

@ -6,6 +6,8 @@
(setq coq-mode-abbrev-table '())
(after! company-coq
(set-popup-rules!
'(("^\\*\\(response\\|goals\\)\\*" :ignore t)))
(set-lookup-handlers! 'company-coq-mode
:definition #'company-coq-jump-to-definition
:references #'company-coq-grep-symbol