When defining a monomorphic Program, do not allow arbitrary instantiations
of the universe context in the obligations, it gets gradually fixed
globally by each one of them.
Fixes bug found in Misc/Overloading.
More efficient implementation of Ltac match, by inlining a stream map.