Rewriter v0.0.5
Pre-release
Pre-release
A pre-release tag for use with Fiat Cryptography v0.0.15 and a non-dev opam package.
Reification now uses Ltac2, and so we only support Coq >= 8.15
What's Changed
- Use
$$
instead of$
to avoid Ltac2 conflict by @JasonGross in #55 - Port reification to Ltac2 by @JasonGross in #57
- Adapt w.r.t. coq/coq#16488. by @ppedrot in #59
- Remove accidental duplication of ml code by @JasonGross in #60
- Make debugging of rewriting example a bit easier by @JasonGross in #61
- Add some Ltac2 util and fix some Ltac2 debug functions by @JasonGross in #63
- Add Ltac2 util and clean up old version cruft by @JasonGross in #65
- More Ltac2 Util by @JasonGross in #66
- Port rewrite rule reification to Ltac2 for improved performance by @JasonGross in #62
Full Changelog: v0.0.4...v0.0.5