[Heapster] Reduce catchpoints and add more Mbox proofs#1413

Merged

eddywestbrook merged 6 commits intomasterfrom heapster-reduce-catchpoints

Aug 9, 2021

+318-301

Commits on Aug 6, 2021

add proofs for mbox_len, _concat_chains, _drop, add Ltac Profiling cmds
m-yac
committed

Commits on Aug 7, 2021

changed how the catch rule is translated, so that branches that could fail are pruned in favor of branches that are guaranteed not to
Eddy Westbrook
committed

Commits on Aug 9, 2021

update generated examples, get proofs working again
m-yac
committed
finish mbox_drop, mbox_concat_chains proofs, remove commented-out bits
m-yac
committed
small tweak to the code to address a suggestion from Matt Y
Eddy Westbrook
committed
Merge remote-tracking branch 'origin/master' into heapster-reduce-catchpoints
Eddy Westbrook
committed