search

the-lambda-church / coquille

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

fix handling of message in answers #55

Closed dwarfmaster closed 7 years ago

dwarfmaster commented 7 years ago

With my version of coqtop The Coq Proof Assistant, version 8.6 (March 2017), messages content may have changed place in the xml. I am thus updating it. Should also fix #54

teto commented 7 years ago

LGTM I've had problems with this as well with coq 8.5.

dwarfmaster commented 7 years ago

poke @trefis

dadoomer commented 7 years ago

Thank you!

yilongli commented 7 years ago

Thanks. This patch saves my day. Any reason not to merge it?

trefis commented 7 years ago

@lucas8 in the code around your change I can see we always access the val field of whatever parse_value returned. We don't anymore with your code. Any reason for that change?

dwarfmaster commented 7 years ago

@trefis I don't see what you're speaking about : inside get_answer, the val field of parse_value isn't used anymore. What may cause the misunderstanding is that the type of parse_value depends on the structure of the XML parsed, which apparently changed between the coq versions.

trefis commented 7 years ago

I misread a call to parse_response as a call to parse_value.

I haven't tested but will trust you that this works, merging.