search

cpitclaudel / company-coq

A Coq IDE build on top of Proof General's Coq mode
GNU General Public License v3.0
351 stars 29 forks source link

Keys bound while company-coq is not active #164

Open jonsterling opened 7 years ago

jonsterling commented 7 years ago

I've recently installed and begun using company-coq, and it's fantastic! Thank you for your hard work.

One thing I have noticed, however, is that even in buffers where company-coq is not activated, its keybindings seem to be active, and are clobbering the keybindings of other modes. In particular, I am currently editing a LaTeX file using latex-mode/auctex, and C-c C-e (which used to be bound to LaTeX-environment) is now bound to company-coq-eval-last-sexp.

Is this supposed to be the case even when company-coq is not running?

cpitclaudel commented 7 years ago

Nope, definitely not. How are you enabling company-coq?

jonsterling commented 7 years ago

company-coq is being enabled as a hook for coq-mode:

(add-hook 'coq-mode-hook #'company-coq-mode)

One interesting thing is, I just ran M-x describe-mode and I see that the Company-Coq--Keybindings minor mode is active, but I don't understand why (I didn't turn it on manually).

cpitclaudel commented 7 years ago

It gets turned on locally when you open a Coq file. This sounds like a weird bug. Can you try reproducing it in a minimal environment ?

jonsterling commented 7 years ago

@cpitclaudel Sure! I'll do so as soon as I can.

Thanks for putting up with all my weird and annoying questions 😃