Fixes #779 regression cannot step Fail correctly.

ProofGeneral / PG

This repo is the new home of Proof General

https://proofgeneral.github.io

GNU General Public License v3.0

491 stars 88 forks source link

Fixes #779 regression cannot step Fail correctly. #780

Closed Matafou closed 4 months ago

Matafou commented 4 months ago

As suggested by @hendriktews: added a "no-error" regexp.

Also adapted the tests so that they pass with coq pre-8.20 and post-8.20. No need to ass more tests case imho.

Matafou commented 4 months ago

Initial issue report: #779 .

hendriktews commented 4 months ago

Thanks for this PR, it now looks fine to me. I suggest to merge when the tests are successful. At some stage we should add proof-shell-no-error-regexp to PG-adapting.