This changeset defines notation for the Iris style of writing Hoare triples:
{{{ P }}} e {{{ v1 .. vn; T, Q }}} := P ★ (∀ v1 .. vn, Q → Φ T) ⊢ WP e {{ Φ }}
For no good reason the notation is parsing only, although I do not declare it as such. We might want to do that though, since it might be too hard to understand a Hoare triple goal without unfolding it.
I have changed the barrier specifications to use the new notation in an attempt to demonstrate their usefulness (or, at a minimum, their applicability). The changes are rather minimal, as you can see.
Changes
First and foremost, the specifications change. (Duh!) Then, there are three kinds of changes to the proofs:

The first
iIntros
needs to take care of introducingΦ
. No big deal, in my opinion. 
Introducing the spatial assumptions needs one additional level of structure since we go from
P1 ★ P2 ★ (∀ v, Q v ★ Φ v)
to(P1 ★ P2) ★ (∀ v, Q v ★ Φ v)

A postcondition of
True
leads to the rather annoying hypothesisTrue ★ Φ v
, which (as far as I can tell) cannot be made to behave the same as just (Φ v) in the context ofiFrame
.
Applicability
I have also looked at most other examples of specifications in heap_lang/lib. The notation seems to be applicable to almost all of them. The only place where I spotted an obvious mismatch is par.v, where the current lemmas have a later before the generalized postcondition, as in ... ★ (∀ .., ... ★ ▷ Φ ..) ⊢ WP ..
. We could always add another pair of notations for this special case, I suppose.
Nomenclature
I think "Texan triple" would be a good name, seeing how everything is bigger in Texas, including the number of curly braces.