Compatible with Coq 8.15 and 8.16, requires OCaml >= 4.08
What's Changed
- Bump rewriter for more reification performance, including caching reified lemmas via LetIn
- Bump rewriter to regain Ltac2 reification performance on par with Ltac1 by @JasonGross in #1389
- More Ltac2 Reification performance experiments by @JasonGross in #1403
- Bump rewriter: Don't duplicate reification typechecking time in Qed by @JasonGross in #1409
- More selective correctness proof tactics for PushButtonSynthesis by @JasonGross in #1416
- Bump rewriter for Cache reified lemmas with LetIn by @JasonGross in #1413
- Automatically increase stack size to avoid stack overflows in OCaml compilation of extracted binaries by @JasonGross in #1430
- Add stacksize warnings to avoid confusion by @JasonGross in #1407
- Split out makefiles to allow binary testing without Coq files by @JasonGross in #1423
- Performance improvements in GarageDoor
- use vm_compute instead of Ltac to check instruction bounds by @samuelgruetter in #1429
- More Blind Optmimizations for GarageDoor by @andres-erbsen in #1431
Full Changelog: v0.0.15...v0.0.16