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.
Rather than commenting `(* Not Global! *)`, do you want to explicitly prepend `Local`?  I'm a fan of self-documenting code, and have gotten in the habit of prepending all of my `Instance`s with `Global` or `Local`, in part because Coq decides to do different things depending on whether or not your instance is in a section, making it hard to remember which is which.