Add a [path_induction_hammer] tactic

It's a more powerful version of [path_induction], but doesn't have very
good computational behavior.  It's somewhat tuned for speed, but is
unfortunately rather fiddly, speed-wise.

This closes #173.
Qualify the import of the Tactics module.

This way, we don't get a warning about ambiguous imports.
Undo use of [symmetry] in [done]

It seems that sometimes Coq decides to use the built-in tactic
regardless of what we do.
Merge pull request #176 from JasonGross/path-induction-hammer

Add a [path_induction_hammer] tactic
Merge pull request #178 from JasonGross/undo-symmetry

Undo use of [symmetry] in [done]
Merge pull request #177 from JasonGross/rename-tactics

Qualify the import of the Tactics module.
I think it is OK to do trivial changes like this yourself, without a pull request.
Merge branch 'master' of https://github.com/HoTT/HoTT