Adapt to coq/coq#18973.

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq

https://metacoq.github.io

MIT License

367 stars 79 forks source link

Closed rlepigre closed 2 months ago

JasonGross commented 2 months ago

Surely this will require similar changes in PCUIC and quotation at least, right?

rlepigre commented 2 months ago

Surely this will require similar changes in PCUIC and quotation at least, right?

OK, I'll have another look, thanks. I should probably have let my local build finish. :sweat_smile:

rlepigre commented 2 months ago

Note that this might not be complete yet: I'm having performance trouble.

proux01 commented 2 months ago

Upstream merged, please merge

proux01 commented 2 months ago

Ping @mattam82 or @ppedrot (you have the rights IIRC)