cpitclaudel/company-coq

How can I turn off the documentation presentation(the company-coq : documentation buffer) at completion

shrubbroom opened this issue · 2 comments

shrubbroom commented

I use company-coq for a while since Emacs 26. After I upgrade to Emacs 27, I found that a documentation buffer will be shown automatically when I am typing tactics and names. I find it bothering most time since it will just cover the goals buffer. How can I turn off this feature. Thanks.

cpitclaudel commented

Surprising; I can't reproduce this. Could you clarify if this happens with a clean config?

shrubbroom commented

I find this popping up since I enable the company-quickhelp-mode in coq-mode. Things go well after I close it. Thanks for your kind reminding.

  • 👍1