Ensuring the invariant that hypotheses and named context of the environment of
Proofview goals coincide by always using the named context and discarding the
hypotheses.
Only using filtered hyps in Goal.enter.

This was probably a bug. A user-side code should never be able to observe
the difference between filtered and unfiltered hypotheses.