v0.0.15

Compatible with Coq 8.18, 8.19, 8.20, Rocq 9.0, 9.1

v0.0.14

Compatible with Coq 8.18, 8.19, 8.20, Rocq 9.0, 9.1

What's Changed

• Adapt to rocq-prover/rocq#20816 by @proux01 in #177
• Adapt to rocq-prover/rocq#21110. by @ppedrot in #178
• Adapt to rocq-prover/rocq#21380. by @ppedrot in #183
• Adapt to rocq-prover/rocq#21195 (add quality constraint kind) by @jrosain in #182
• Adapt to rocq-prover/rocq#21391. by @ppedrot in #184
• Adapt to rocq-prover/rocq#21394. by @ppedrot in #185
• Adapt to rocq-prover/rocq#21395 (revert univ_decl name change) by @SkySkimmer in #186
• Adapt to rocq-prover/rocq#21421. by @ppedrot in #187
• Adapt to rocq-prover/rocq#21419 by @mattam82 in #188
• Adapt to rocq-prover/rocq#21467. by @ppedrot in #189

New Contributors

• @Copilot made their first contribution in #180
• @jrosain made their first contribution in #182
• @mattam82 made their first contribution in #188

Full Changelog: v0.0.13...v0.0.14

Rewriter v0.0.13

Compatible with Coq 8.18, 8.19, 8.20, Rocq 9.0

What's Changed

• Adapt to rocq-prover/rocq#19690 (Hint Extern follows default proof mode) by @SkySkimmer in #171
• Adapt w.r.t. rocq-prover/rocq#20423. by @ppedrot in #172

Full Changelog: v0.0.12...v0.0.13

Rewriter v0.0.12

Compatible with Coq 8.18, 8.19, 8.20

What's Changed

• Rely on upstreamed Ltac2 functions (prompted by rocq-prover/rocq#18973). by @rlepigre in #155
• Adapt to rocq-prover/rocq#19384 (cleanup ustate universe demote APIs) by @SkySkimmer in #156
• speedup wf{3,4}_of_wf by factorizing raw matches to definitions by @SkySkimmer in #157
• Adapt to rocq-prover/rocq#19530 by @proux01 in #159
• Adapt to rocq-prover/rocq#19620 (Global.push_context_set no strict argument) by @SkySkimmer in #160
• add missing nounfold for Qeq_bool in Sample.v (for coq/coq##19801) by @andres-erbsen in #164
• Adapt to coq#19822 by @Tragicus in #165

New Contributors

• @rlepigre made their first contribution in #155
• @proux01 made their first contribution in #159
• @Tragicus made their first contribution in #165

Full Changelog: v0.0.11...v0.0.12

Rewriter v0.0.11

Compatible with Coq 8.17, 8.18, 8.19.

What's Changed

• Add profiling for cbn by @JasonGross in #141
• Add more debug profiling (replace_type_try_transport) by @JasonGross in #143
• More error messages when .coq-version creation fails by @JasonGross in #144
• Move unfolding of fst and snd earlier by @JasonGross in #142
• adapt to rocq-prover/rocq#18563 by @andres-erbsen in #148
• Adapt to rocq-prover/rocq#18624 (Tac2ffi / Tac2val split) by @SkySkimmer in #149

New Contributors

• @divergentdave made their first contribution in #147

Full Changelog: v0.0.10...v0.0.11

Rewriter v0.0.10

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

What's Changed

• Adapt to rocq-prover/rocq#18082 (Ltac2 mutable refs are not values) by @SkySkimmer in #115
• Adapt to rocq-prover/rocq#18164 by @Villetaneuse in #119
• Adapt to rocq-prover/rocq#18197 (List and Array fold argument order change) by @SkySkimmer in #120
• Adapt to rocq-prover/rocq#17836 (sort poly) by @SkySkimmer in #109
• Fix Util/Strings/String.v by @Villetaneuse in #123
• Adapt to rocq-prover/rocq#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

New Contributors

• @Villetaneuse made their first contribution in #119

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

Rewriter v0.0.9

Compatibility with Coq 8.18

What's Changed

• Factor rewriter reification through Ltac2 Constr.Usafe.iter by @JasonGross in #111
• Adapt to rocq-prover/rocq#17533 (use correct plugin name in ltac2_extra external) by @SkySkimmer in #101
• Adapt to rocq-prover/rocq#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 to 8ce1d5d by @dependabot in #103
• Bump etc/coq-scripts from 8ce1d5d to 8b66ebe 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

Rewriter v0.0.8

What's Changed

• Better "cannot strip functional dependencies" message by @JasonGross in #83
• When replacing Coq version info, display the replacement by @JasonGross in #82
• Fix for realpath not in zsh by @JasonGross in #91
• Adapt w.r.t. rocq-prover/rocq#16910. by @ppedrot in #95
• adapt for rocq-prover/rocq#17022 by @andres-erbsen in #96

New Contributors

• @andres-erbsen made their first contribution in #96

Full Changelog: v0.0.7...v0.0.8

Rewriter v0.0.7

A pre-release tag for use with Fiat Cryptography v0.0.16 and a non-dev opam package.

What's Changed

• Cache reified lemmas with LetIn by @JasonGross in #77
• Next batch of Ltac2 reification attempted performance improvements / experiments by @JasonGross in #67
• Add debug profiling to _Reify_rhs by @JasonGross in #68
• Don't duplicate reification typechecking time in Qed by @JasonGross in #69
• Remove dead code by @JasonGross in #70
• Don't allocate an unchecked evar for identifier types by @JasonGross in #71
• Add UnderLetsCacheProofs for better Reify_rhs proofs by @JasonGross in #72
• Control.once in debug_profile by @JasonGross in #76
• Global Strategy -1000 [UnderLets.to_expr]. by @JasonGross in #75
• Route through _Reify_rhs for all rewriting by @JasonGross in #73
• Add some Ltac2 util by @JasonGross in #78
• reify_in_context_opt now returns reified types too by @JasonGross in #74
• Use to_expr_App instead of to_expr so that reduction works correctly by @JasonGross in #79

Full Changelog: v0.0.6...v0.0.7

Rewriter v0.0.6

A pre-release tag for use with Fiat Cryptography v0.0.15 and a non-dev opam package.

Fixes an issue in v0.0.5 that causes fiat-crypto to not build.

Full Changelog: v0.0.5...v0.0.6