Uniformize reflective subuniverses and modalities

And also add a few more examples.  This closes #457.  The use of typeclasses is a bit hackish (see comments in `ReflectiveSubuniverse.v`), but it's the best way I've been able to think of to avoid having to pass the modality as an argument to everything all the time when there is only one modality hanging around.
Ah, I see.  Note that if you replace `foo` with `@foo _`, you get the same result in both cases.  I'm trying to figure out how http://coq.inria.fr/refman/Reference-Manual022.html#sec671 and http://coq.inria.fr/refman/Reference-Manual004.html#implicit-generalization imply this, and am not succeeding.  Perhaps it is a bug, or the difference between a meta and an evar, or something.  Perhaps @mattam82 can explain?

In any case, if you replace "introduce a *new* subuniverse hypothesis rather than using the one you intend" with "introduce a *new* [UnitSubuniverse] hypothesis rather than picking up the one you intend by typeclass resolution", I think that would have been sufficient to unconfuse me; for some reason, I had read it at first as taking about the hypothesis of type `inO A` rather than the hypothesis of type `UnitSubuniverse`.