Release Rewriter v0.0.10 · mit-plv/rewriter

Last release compatible with Coq 8.15, 8.16. Compatible with Coq 8.15--8.18.

What's Changed

Adapt to coq/coq#18082 (Ltac2 mutable refs are not values) by @SkySkimmer in #115
Adapt to coq/coq#18164 by @Villetaneuse in #119
Adapt to coq/coq#18197 (List and Array fold argument order change) by @SkySkimmer in #120
Adapt to coq/coq#17836 (sort poly) by @SkySkimmer in #109
Fix Util/Strings/String.v by @Villetaneuse in #123
Adapt to coq/coq#18280 (case relevance outside case info) by @SkySkimmer in #122
Add expr.Wf4 by @JasonGross in #124
Add more wf3/wf4 proofs by @JasonGross in #125
Generalize is_not_higher_order by @JasonGross in #126
Add type.eqv_of_is_not_higher_order by @JasonGross in #127
Add related_hetero_and_Proper by @JasonGross in #128
Add prod_rect_nodep_eta by @JasonGross in #129
Allow leaving over shelved goals when debugging cache_term by @JasonGross in #130
Fix unfolding of let in rewrite rule proving by @JasonGross in #131
More expressive debugging in handle_reified_rewrite_rules_interp by @JasonGross in #132
Add expr.reify_as_interp_related by @JasonGross in #133
Provide a convenience hypothesis with eqv assumptions in rewrite rules side-conditions by @JasonGross in #134
Allow prove_eq_by_Proper to prove Proper instances recursively and by assumption by @JasonGross in #135

Full Changelog: v0.0.9...v0.0.10