Using the standard (type class based) transitivity tactic for more controlable proof terms.
brackets
Removing @ notation magic
Merge branch 'master' of github.com:HoTT/HoTT

Conflicts:
	theories/hit/V.v
I prefer simple tactics to `match ... in ... return ...`
I prefer `exact _` to `typeclasses eauto`
few style fixes
Merge branch 'master' of github.com:HoTT/HoTT
Correcting merge, including suggestions.
Don't use "Set Implicit Arguments" in the core.
make clean in the install script

As per
https://github.com/HoTT/HoTT/commit/bab2b34719108dbc5da66ac40c6fe01e64f4071b#commitcomment-7695206,
this will prevent having subtlely inconsistent .vo files when you
recompile Coq.
s/Record Elimination/Nonrecursive Elimination/

As per https://coq.inria.fr/bugs/show_bug.cgi?id=3586, [Set Record
Elimination Schemes] is going away eventually.
Merge pull request #473 from JasonGross/install-make-clean

make clean in the install script
Merge pull request #474 from JasonGross/set-nonrecursive-elim

s/Set Record Elimination Schemes/Set Nonrecursive Elimination Schemes/
Merge branch 'master' of github.com:HoTT/HoTT

Conflicts:
	theories/hit/epi.v
merging, for real this time.
Making concat more readable
Being explicit about location
Add quick and vi2vo targets

It doesn't seem to help much at the moment, but maybe we'll grow some
very slow Qed'ed proofs and want to use this target.

c.f.
https://github.com/coq/coq/blob/trunk/doc/refman/AsyncProofs.tex#L98 for
documentation.

```bash
$ make clean
...
$ time make -j10
real    2m51.868s
user    4m7.179s
sys     8m45.765s

$ make clean
...
$ time make quick -j10

real    2m54.031s
user    4m15.360s
sys     8m52.969s

$ time make vi2vo J=10

real    0m21.458s
user    0m9.161s
sys     0m17.161s

```

This closes #471.
Merge pull request #469 from mikeshulman/implicit

Don't use "Set Implicit Arguments" in the core.