search

gmalecha / template-coq

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

Fix bugs with LetIn #25

Closed mattam82 closed 8 years ago

mattam82 commented 8 years ago

In Coq's representation the body comes first, unlike tLetIn Fixed quote and unquoting as well and added a test in the test-suite.

mattam82 commented 8 years ago

Wait a second. Maybe we should keep the representation of Coq instead?

mattam82 commented 8 years ago

That seems better to me. Now code relying on the bug (like in certicoq) will work unmodified.

gmalecha commented 8 years ago

Thanks, Matthieu! You do as much (maybe more) work than me. Would you like me to make you a contributor? @mattam82

mattam82 commented 8 years ago

Sure !

On Mon, May 2, 2016 at 6:39 PM Gregory Malecha notifications@github.com wrote:

Thanks, Matthieu! You do as much (maybe more) work than me. Would you like me to make you a contributor? @mattam82 https://github.com/mattam82

— You are receiving this because you were mentioned.

Reply to this email directly or view it on GitHub https://github.com/gmalecha/template-coq/pull/25#issuecomment-216287223