问CoqIde关于汽车战术的奇怪信息
EN

Stack Overflow用户

提问于 2018-09-20 07:48:09

回答 1查看 52关注 0票数 0

在使用“尝试策略”中的“auto”或“电子自动”项目时，CoqIde将使用以下消息进行响应，无论当前位置在何处：

Currently, the parsing api only supports parsing at the tip of the document.
You wanted to parse at: 0 but the current tip is: 54

这里怎么了？

发布于 2018-09-20 09:54:33

这是Coq中的一个bug，可能已经在master分支中修复了。请到https://github.com/coq/coq/issues报到

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/52420130

复制

相似问题

问CoqIde关于汽车战术的奇怪信息EN