v0.0.9: straightline: do not match below binders (#493)

When flattening seps, straightline was matching below binders which it
couldn't simplify. This caused some slowdown because the match and
simplify happened on each run, each hypothesis, and each wrongly
bracketed sep in that hypothesis.

Simply replacing _ with ?_a resolves it because the matching can't bind
something that's unresolved to _a.

Also adding some tests for ProgramLogic, for this issue and the previous
one I fixed where straightline was destructing context variables, which
it shouldn't.

v0.0.8

Commits: v0.0.7...v0.0.8

v0.0.7

sketch wp_read_RDH

v0.0.5

For Coq platform 8.17 beta.

Bedrock2 v0.0.4

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

What's Changed (Partial List)

• use vm_compute instead of Ltac to check instruction bounds
• Pass -native-compiler ondemand for bedrock2 ex by @JasonGross in #283
• trying to merge egraph-less parts from egraphs branch by @samuelgruetter in #284

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

Bedrock2 v0.0.3

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

What's Changed

• make bedrock2_install now installs examples by @JasonGross in #281

Full Changelog: v0.0.2...v0.0.3

Bedrock2 v0.0.2

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

What's Changed

• add in-memory uint128 add for 32-bit by @andres-erbsen in #240
• try out SepCalls in lightbulb.v by @andres-erbsen in #244
• Add support for metrics in the FlatToRiscvFunctions and FlattenExpr passes by @pratapsingh1729 in #246
• Adapt w.r.t. rocq-prover/rocq#16004 by @Alizter in #250
• Name Coq builds so they are more stable across updates by @JasonGross in #258
• Fix probable typo introduced in bcd4bcf by @JasonGross in #265
• Faster ensure_free by @JasonGross in #267
• Memmove by @andres-erbsen in #275
• add memequal, memswap, memconst by @andres-erbsen in #277
• Python instead of sed by @andres-erbsen in #276
• Add CI tests for Windows and Mac by @JasonGross in #272
• speed up WeakestPreconditionProofs by @andres-erbsen in #280

New Contributors

• @pratapsingh1729 made their first contribution in #246
• @Alizter made their first contribution in #250

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

Bedrock2 v0.0.1

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