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 coq/coq#18563 by @andres-erbsen in #148
• Adapt to coq/coq#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 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

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 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 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. coq/coq#16910. by @ppedrot in #95
• adapt for coq/coq#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

Rewriter v0.0.5

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

Rewriter v0.0.4

Last release compatible with Coq 8.11 -- 8.14. Supports Coq 8.11 -- Coq 8.15 (and possibly 8.16)

What's Changed

• Drop support for Coq < 8.11, make hint globality explicit by @JasonGross in #45
• Don't leave over a useless let-in in cache_term by @JasonGross in #49
• Remove some unused requires by @JasonGross in #50
• Clear unused deps in cache_term for transparent_abstract by @JasonGross in #51
• Split off Reify.v by @JasonGross in #52
• Add an example dealing with defined constants by @JasonGross in #53

Full Changelog: v0.0.3...v0.0.4

Rewriter v0.0.3

Last release compatible with Coq 8.9 and 8.10. Supports Coq 8.9 -- Coq 8.15 (and possibly 8.16)

Rewriter v0.0.2

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

What's Changed

• Use simple notypeclasses refine in transparent assert by @JasonGross in #24
• Future proof mod_bound_nonneg by @mrhaandi in #25
• Prove wf_smart_App_curried by @JasonGross in #26
• Overlay for coq/coq#14224 by @jfehrle in #27
• Switch to a heterogenous base_interp_beq by @JasonGross in #28
• Adapt to Coq PR #14379: change of semantics of Reserved Infix "'o'" by @herbelin in #29
• Add support for seprate ml files for Coq 8.15 by @JasonGross in #31
• Adapting to Coq PR #14711: Evd.check_univ_decl returns also the universe binders by @herbelin in #30
• Adapt w.r.t. coq/coq#14903. by @ppedrot in #32
• [CI] Update Coq versions by @JasonGross in #33
• Bump etc/coq-scripts from 1ad4075 to c34a5e9 by @dependabot in #35
• Bump etc/coq-scripts from c34a5e9 to 3be05c7 by @dependabot in #36
• Add util lemmas ported from fiat-crypto by @JasonGross in #37
• adapt to coq/coq#15220 by @gares in #34
• Bump actions/checkout from 2 to 3 by @dependabot in #38
• Bump etc/coq-scripts from 3be05c7 to 7e68a28 by @dependabot in #39

New Contributors

• @mrhaandi made their first contribution in #25
• @jfehrle made their first contribution in #27
• @dependabot made their first contribution in #35
• @gares made their first contribution in #34

Full Changelog: v0.0.1...v0.0.2