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
Merge pull request #469 from mikeshulman/implicit

Don't use "Set Implicit Arguments" in the core.
Merge pull request #465 from mikeshulman/prod

Some stylistic preferences in Prod.v