test_wholefile.v incompatible with 8.17

Open hendriktews opened this issue 2 years ago • 1 comments

The Hint Resolve command in ci/test_wholefile.v triggers a fatal warning in Coq 8.17. Test 060_coq-test-wholefile in ci/coq-tests.el fails therefore for 8.17.

Apr 08 '23 13:04 hendriktews

@hendriktews I've been trying to get in touch with you - especially about the Debian packaging for proofgeneral... could you contact me? I'm jpuydt and a Debian developer so you can guess a valid mail.

Thanks!

Jun 20 '23 08:06 SnarkBoojum