vscoq icon indicating copy to clipboard operation
vscoq copied to clipboard

Published 20 hours ago • verified publisher icon coq-community

Parsing issues with MetaCoq

Open thomas-lamiaux opened this issue 5 months ago • 3 comments

At the moment, basically all the files in https://github.com/thomas-lamiaux/generating_recursors creates parsing issue. I can not exactly isolate a file as it happens from time to time when I open files.

You can check out the issue by cloning the repo, doing make, and trying to check the files in the folder recursors_api.

I am using coq 8.19.2, the associated version of Equations and MetaCoq and vscoq 2.1.7.

thomas-lamiaux avatar Sep 09 '24 08:09 thomas-lamiaux