search

the-lambda-church / coquille

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

Add debug buffer, fix a bug #70

Open WangNan0 opened 6 years ago

WangNan0 commented 6 years ago

Python raise an exception when dealing 'Qed.' in coq8.5. This patch fix it.

A debug facility is added to help people check the communication between vim and coqtop. See commit message for usage.