Fix huge performance issue due to last patch.
Now Hints can be declared polymorphic or not. In the first case they
must be "refreshed" (undefined universes are renamed) at each application.