The main changes are:

* Function calls in the operational semantics
* Mutually recursive function calls in the axiomatic semantics
* A general definition of the interpretation of the axiomatic semantics  so as
  to improve reusability (useful for function calls, and also for expressions
  in future versions)
* Type classes for stack independent, memory independent, and memory extensible
  assertions, and a lot of instances to automatically derive these properties.
* Many additional lemmas on the memory and more robust tactics to simplify
  goals involving is_free and mem_disjoint
* Proof of preservation of statements in the smallstep semantics

* Some new tactics: feed, feed destruct, feed inversion, etc...
* More robust tactic scripts using bullets and structured scripts
* Truncate most lines at 80 characters