Pierre Courtieu
Pierre Courtieu
OK I see, compilation breaks.
Sorry for the delay, I will review your PR shortly. Thanks for it!
> * Probably a missing cancel-timer somewhere. I will investigate a bit more. It is just that the timer should not be launched when the semi's type is `'comment`.
If you want a script where coq still hangs you can use this: ``` Lemma foobar: True. Proof. idtac.+ } ```
It seems to work, but is it really what we expect? When one launch a big thunk of coq commands, if the global execution of the whole thunk takes more...
Hi, thanks for reporting this. Note that if you split "?;" into "? ;" it works. PG does not detect that "?;" is not one token but two. By default...
Hi. Thanks for reporting. Indeed there is a problem with error detection since a few weeks. I will try to fix that shortly. FTR this does not seem to be...
No it has actually nothing to do with error detection. It is yet another case where PG splitting the coq file into single commands wrongly. Here the `{` at start...
Nice idea.
8.9 is only 2 years old. Let us not drop it until one or two years from now imho.