Ramkumar Ramachandra (May 28 2020 at 14:21): Ramkumar Ramachandra (May 28 2020 at 14:21):#97 doesn't work for me anymore, due to an opam upgrade this morning. I don't know which version of coq and coq-hott it's supposed to work with. I currently have coq.8.11.1 and coq-hott.8.11 installed.
Ramkumar Ramachandra (May 28 2020 at 14:27):"Interpret to point failed: Error: Request coqtop/interpretToPoint failed unexpectedly without providing any details."
Ramkumar Ramachandra (May 28 2020 at 14:32):Sorry, the diagnosis was incorrect: I'd also pulled HoTT, which needed a rebuild.
vlj (Jun 04 2020 at 19:32):It's possible to use vscoq with hoqtop ?
Ramkumar Ramachandra (Jun 05 2020 at 06:10):Yes, I'm using it successfully with #97.
Ramkumar Ramachandra (Jun 05 2020 at 06:13):I've been trying to get @Maxime Dénès to merge it into vscoq.
Last updated: Jun 04 2023 at 23:30 UTC