PG "processes" bogus tactics

Open Ptival opened this issue 6 years ago • 1 comments

The following two commands:

Goal 2 + 2 = 5.
{| I can write whatever I want here... |}.

are being processed correctly by my version of PG+coq.

It seems like the second one should not be accepted.

Feb 13 '20 08:02 Ptival

Hi, thanks for reporting. Indeed the coq process reports an error and PG do not detect it. Strange.

Feb 13 '20 08:02 Matafou