Compatible with Coq 8.17, 8.18; requires OCaml >= 4.08.
Last release compatible with Coq 8.17
What's Changed
- fiat-crypto code generator now runs on the web!
- Add js_of_ocaml build and deployment by @JasonGross in #1737
- Use WebWorkers and a cache for js-of-ocaml by @JasonGross in #1739
- Add wasm_of_ocaml build by @JasonGross in #1747
- Deploy WASM integration to https://mit-plv.github.io/fiat-crypto by @JasonGross in #1749
- Fix DCE/Subst01 to work under lambdas by @JasonGross in #1809
- Make install targets depend on vo files by @JasonGross in #1741
- zig: use "const" for variables that are never mutated by @jedisct1 in #1742
- Adapt to expr.Wf4 by @JasonGross in #1752
- adapt to coq/coq#18164 by @Villetaneuse in #1760
- Future-proof CompilersTestCases by @JasonGross in #1762
- Factor ZRange Proper proof by @JasonGross in #1764
- Add some more ZRangeProofs by @JasonGross in #1766
- Update ZRangeProofs by @JasonGross in #1767
- Add support for applying bool functions to zrange by @JasonGross in #1770
- Add
Util.Option.bind2by @JasonGross in #1768 - More fine-grained bounds analysis by @JasonGross in #1769
- Add more identifiers for saturated solinas by @JasonGross in #1773
- Add remaining identifiers for saturated solinas by @JasonGross in #1774
- Add
subst!andtypeof!toNotations.vby @JasonGross in #1775 - Allow leaving over shelved goals when debugging cache_term by @JasonGross in #1779
- Add prod_rect rewrite rule for saturated arithmetic by @JasonGross in #1780
- Augment rewrite rule proving tactics for saturated arithmetic by @JasonGross in #1783
- Cache intermediate values for Edwards addition by @bMacSwigg in #1808
New Contributors
Full Changelog: v0.1.0...v0.1.1