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

Adapt to coq/coq#18082 (Ltac2 mutable refs are not values) #115

Closed SkySkimmer closed 1 year ago

SkySkimmer commented 1 year ago

Should be backwards compatible.