ML code compatibility for Coq PR # 6285

mit-plv / fiat

Mostly Automated Synthesis of Correct-by-Construction Programs

http://plv.csail.mit.edu/fiat/

Other

147 stars 31 forks source link

Closed mattam82 closed 1 year ago

mattam82 commented 3 years ago

Do not merge yet. Follows coq/coq#6285

JasonGross commented 3 years ago

This seems wrong, I thought the ML API for Coq 8.13.X was frozen? Should I split off the v8.14 files?

mattam82 commented 3 years ago

Yes please, I didn't know how to do it and just wanted to check my PR was building correctly on the CI

JasonGross commented 3 years ago

Hopefully https://github.com/mit-plv/fiat/pull/51 should do the trick. I'll merge it if it passes CI and then ask you to rebase this on top of that.

JasonGross commented 3 years ago

Please rebase on current master

mattam82 commented 3 years ago

Thanks!

JasonGross commented 1 year ago

Choosing this as the Coq PR was closed in December 2021