Rewriter v0.0.7
Pre-release
Pre-release
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