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
How to avoid Emacs prompts about risky local variables
Merge pull request #433 from mikeshulman/lvdoc

How to avoid Emacs prompts about risky local variables
Add Utf8 notations in a separate file
Add notation <>, add Utf8 notations from stdlib
Replace BULLET OPERATOR (∙) with BULLET (•)

Apparently, Emacs' built-in `tex` mode can do BULLET (`\bu` in
agda-mode), but not BULLET OPERATOR (`\.` in agda-mode).
Add an error message about BULLET OPERATOR

E.g., So that people coming from HoTT-Agda are less confused when using
agda-mode input.
Add unicode instructions