search

gmalecha / template-coq

Reflection library for Coq
MIT License
12 stars 0 forks source link

Port to Coq8.6 #30

Closed yforster closed 7 years ago

yforster commented 7 years ago

Hi,

is somebody by chance already working on a port of template-coq to Coq 8.6?

I was able to fix most problems (or at least many) by following the changes.txt file, but the use of the ltac_apply function fails, and I can't figure out why.

I pushed my changes to my fork of the repo: https://github.com/yforster/template-coq/commit/5771a9d590b20c51e3ff82e702ae28b1132dd3dd

Any ideas what's wrong with ltac_apply? I couldn't find anything useful in the changes file.

Thanks in advance Yannick

yforster commented 7 years ago

I ended up copy-pasting the definition of ltac_apply from newring.ml, hoping that it would do the right thing, and, luckily, it looks like it does.

I pushed everything to my fork, the only thing not compiling is the vernacular Quote Definition ... := Eval ... in .... We don't need any of the vernacular commands, so I don't really know wether they are working, but quote_term and denote_term both work fine now.

I can file a pull request if you want, but didn't just yet, because of the potentially broken Vernaculars.

gmalecha commented 7 years ago

Thanks! I don't know of anyone else that has ported to 8.6 so this is great.

If the changes are not backwards compatible, please file a pull request against a new branch for 8.6.

gmalecha commented 7 years ago

This is closed in #31. Thanks for the PR!