Rewriter v0.0.9
Pre-release
Pre-release
Compatibility with Coq 8.18
What's Changed
- Factor rewriter reification through Ltac2 Constr.Usafe.iter by @JasonGross in #111
- Adapt to coq/coq#17533 (use correct plugin name in ltac2_extra external) by @SkySkimmer in #101
- Adapt to coq/coq#17475 (Ltac2 externals can have arity 0) by @SkySkimmer in #102
- Use
Constr.is_proj
for checking projections by @JasonGross in #110 - Version Util.Tactics2.{Constr,Proj,DestProj} by @JasonGross in #113
Proj.equal
has been upstreamed, so use it directly by @JasonGross in #114- Bump etc/coq-scripts from
efae533
to8ce1d5d
by @dependabot in #103 - Bump etc/coq-scripts from
8ce1d5d
to8b66ebe
by @dependabot in #108 - ProofsCommonTactics: log failing inital goals by @andres-erbsen in #104
- Bump actions/checkout from 3 to 4 by @dependabot in #105
- Add publication by @JasonGross in #106
- Move CI up by @JasonGross in #107
- Add separate files for v8.19 by @JasonGross in #112
- [CI] Add newer Coq by @JasonGross in #100
Full Changelog: v0.0.8...v0.0.9