Prove [A * (B * C) <~> (A * B) * C]

Make use of the new dependent goals feature to make the proof prettier.
Merge pull request #428 from JasonGross/prod-type-assoc

LGTM. I am merging because it is so small and it does not conflict with other stuff.

Prove [A * (B * C) <~> (A * B) * C]
Use the coq-git ppa on travis

Now that ezyang's ppa works on precise, we can use it rather than
building Coq ourselves; this is about 10 minutes faster on each build.
We keep one test running Coq, to make sure that the pinned version of
Coq can always build the relevant version of the library.
Merge pull request #431 from JasonGross/travis-ppa

Great! Thanks @ezyang!
I am assuming we now have a ppa for Coq trunk.

Use the coq-git ppa on travis
Add format specifiers to notations to remove space

Now things like [p^] will display as [p^] rather than [p ^].  This means
that confusing expressions like [p ^ @ ! x] will be rendered as the less
confusing [p^ @ !x].
Merge pull request #432 from JasonGross/format-notations

Add format specifiers to notations to remove space