Fix handling of universes at the end of proofs, esp. for async proof processing.
Thanks to E. Tassi for the initial patch.