HoTT/HoTT — pull request #65 by mikeshulman (2013-02-06 05:18:40+00:00)
Title: Greatly improved Record tactics, thanks to help from Jason Gross

The issig tactics now:
1. Don't require passing the fibration as an argument
2. All have the same name
3. Build coherent equivalences directly, rather than with adjointify
4. Are a bit faster
5. Incorporate more Ltac black magic.