search

mit-plv / rewriter

Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Other
22 stars 20 forks source link

Rely on upstreamed Ltac2 functions (prompted by coq/coq#18973). #155

Closed rlepigre closed 4 months ago

rlepigre commented 4 months ago

Both of these iter functions have been upstreamed into Coq itself, so we should be able to just remove them

Indeed, up to a small API change for the second function. So, I guess this can be merged directly?