Moving to Program Instances for examples, renamed iHammer to iSmash, empty_hyps are now removed on introduction.

Changed inc_dec to be more like caper's, removed some extra rwlock methods to more fit with caper/starling.

Separated int_as_nat_diff library, extra pure hints no longer need ugly ltac overriding, improved spin and ticket lock allocation specs.

Improved support for asynchronous proof running in barrier and peterson, collapsed some implementations, added more data on other tools and incorporated them into table.

Can now iInv on SolveSep goal, minor changes, improved table generation function to incorporate data about other tools' examples.

Fail is a better default definition for Ltac extension points, added tactic for pure solving of bool_decide equalities.