HoTT/HoTT — pull request #134 by JasonGross (2013-07-04 16:56:21+00:00)
Title: Prefix 'Instance' with 'Global'

[Instance]s are, by default, local to sections. This includes the
AssumeFunext sections. I've gone through and prefixed all of the
[Instance]s inside of AssumeFunext sections with [Global], so they get
picked up by typeclass search. I haven't (yet) gone through the files
thoroughly to make sure that no other local [Instance]s show up in
sections.

This bit me when trying to do some things in my category theory library.

I may go back and check the remaining instances soon.

Once again, my emacs has removed all the trailing spaces from the relevant files. I can resubmit this pull request without those line changes if desired.