search

the-lambda-church / coquille

Interactive theorem proving with Coq in vim.
ISC License
186 stars 68 forks source link

Fixes #18 #19

Closed bhuber closed 10 years ago

bhuber commented 10 years ago

See http://coq.inria.fr/distrib/V8.4pl3/CHANGES for relevant protocol changes and https://github.com/tauli/CoqIDE/commit/2e5578c8078c7aa60aee491d037cc6eed1ab3a8c for sample fix in CoqIDE project.

Tested a bit on v8.4pl3 but not backtested on older versions. Seems to work but I haven't done anything too complicated with it (still learning coq).

trefis commented 10 years ago

Hi!

Thanks for the link to CHANGES; I had such a fix locally too and I wasn't sure it was enough, but it apparently is. I merged your changes.

bhuber commented 10 years ago

np, thanks for accepting the patch