the-lambda-church/coquille

Incompatibility with minibufexpl

Closed this issue · 2 comments

When the minibufexpl plugin is installed, coquille can initialize and :CoqLaunch seems so succeed, but doesn't make any command (CoqNext, CoqToCursor,...) available.

Not sure if this is a big issue, but it should at least be mentioned in the readme (took me some time to realize the source of the problem). Especially because minibufexpl is part of the standard vim plugins package in some linux distributions (like arch).

Hi!

I personally never used minibufexpl, so I wasn't aware of the problem. I will install it some time this week to try and see where your problem might be coming from!

Once again : sorry for the delay, this could have been fixed way sooner.

The bug was funny : when initializing the IDE (i.e. on CoqLaunch) I was opening the Goal and Infos buffers, before making the command accessible. The thing is, as new buffers appeared, minibufexpl would then take the focus. Since I bound the commands to the buffer, they were then accessible in minibufexpl buffer, but not in your Coq buffer.

Sorry for the inconvenience.