search

gmalecha / template-coq

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

Coq 8.6 #31

Closed yforster closed 7 years ago

yforster commented 7 years ago

Github can't open pull requests against new branches, so I opened it against coq-8.5

As mentioned in the issue, I'm not sure wether the Vernacular commands work (but don't see a reason why not), only "Quote" "Definition" ident(name) ":=" "Eval" red_expr(rd) "in" constr(def) is definitely broken and commented out.

aa755 commented 7 years ago

These changes are not backward compatible with coq-8.5 So I suggest creating a new 8.6 branch in this repo. Perhaps the owners can git-pull the yforster:coq-8.6 branch to a seperate branch in this repo?

gmalecha commented 7 years ago

Yes, this will get pulled into a separate branch.

gmalecha commented 7 years ago

A bit of hackery, but things seem to look good now. I don't have coq 8.6 installed right now, but I'm happy to merge this into the newly created 8.6 branch.