fix comment
Merge pull request #623 from mikeshulman/trunc-leq

trunc_leq transparent & not an instance, no no-ops in trunc_contr
.+3, .+4, .+5
Merge pull request #625 from JasonGross/more-dot-plus

.+3, .+4, .+5
Merge branch 'master' into comodalities
Comodalities basically working, and tested in a trivial case.

The universe annotations are really annoying to get right -- the error messages don't
completely help pinpoint the problem -- and the last one doesn't even work in the pinned
coq, although it does in trunk.