HoTT/HoTT — pull request #133 by JasonGross (2013-07-02 19:06:35+00:00)
Title: More notation fixes

The main reason for this pull request is to put `'o'` inside of a scope; when trying to port my category theory library to be built on top of HoTT, I discovered that I couldn't effectively use `'o'` as a notation after importing HoTT because it got stuck in the default scope. I figured I'd also put the other notations in scopes while I was at it; it's much easier to overwrite a notation or hide it, should you want to, if it's in a scope.

I've checked to make sure that the library still compiles. One backwards-incompatible change is that we'll now need to `Open trunc_scope` to use the `<=` notation for truncation. This can be remedied by opening it globally in `Overture.v`, if that's desirable.

If you want, I can remove the churn caused by emacs removing trailing spaces, but I figured I'd leave it in unless told otherwise.