[change ... in *] picks universes once, which unifies universes too eagerly (polyproj)

[JasonGross]

Here is some code that works in 8.4pl3 and HoTT/coq, but fails in trunk-polyproj

(* File reduced by coq-bug-finder from original input, then from 3329 lines to 153 lines, then from 118 lines to 49 lines, then from \
55 lines to 38 lines, then from 46 lines to 16 lines *)

Generalizable All Variables.
Set Universe Polymorphism.
Class Foo (A : Type) := {}.
Definition Bar {A B} `{Foo A, Foo B} : True.
Proof.
  Set Printing Universes.
  change Foo with Foo in *.
  admit.
Defined.
Definition foo := @Bar nat.
Check @foo Set.
(* Toplevel input, characters 26-29:
Error:
The term "Set" has type "Type (* Set+1 *)" while it is expected to have type
 "Set" (Universe inconsistency: Cannot enforce Set < Set because Set = Set)). *)

I believe this is the same bug as #107.