Remove dependency of fancy updates on the program language.
This merge request removes the dependency on the program language from the encoding of invariants, fancy updates, and many constructions such as boxes, sts, auth, ... This reason for doing this, is that in some cases one might not want to use the Iris definition of weakest preconditions or the Iris interface for a programming language.
I have achieved this factoring out a type class
invG that keeps track of the ghost state needed for encoding invariants from the type class
irisG. Fancy updates, boxes and sts are parametrized by
invG, and not by
irisG (which depends on the language).
TODO: state adequacy for fancy updates in a self-contained way.