HoTT/HoTT — pull request #164 by JasonGross (2013-08-02 18:14:40+00:00)
Title: Fix theories/Functorish.v

I'm not sure whether or not the last line in that proof is needed in an
old version of HoTT/coq, but I'm pretty sure it's not needed in the
newest version. Chaining it with the previous command and adding a
[try] permits it to be run only if necessary.