Romain Tetley
Romain Tetley
@gares what is the status on this ?
Unable to reproduce on master. Closing.
On first investigation there seems to be a strange behaviour in manual mode. To reproduce: 1) Interpret to the line in question (182). This should trigger the error. 2) Invalidate...
You should test the latest version (vscoq2) which has an experimental option to do just that ! Just don't forget to toggle the completion setting which is disabled by default...
I've been checking this issue on VsCoq 2 and the provided example seems to be working okay (it takes a little longer than a second but nothing as unreasonable as...
I am unable to reproduce this crash. Could you give more information on your set up and maybe the error message for context ? You can get more information in...
Closing as I am unable to reproduce.
Hi ! Thanks for your feedback :-) It seems that the ```coq Module NatPlayground2. ``` line is the culprit. If I comment it out it no longer crashes. This is...
After investigation, this seems to come from the Module command which fails in the interp phase but succeeds in the synterp phase. When you declare a logical object after that,...
I believe it fails because in the example a Module is declared on top of an open proof.