Don't abstract inside of Qed; also another change that speeds things up in trunk

Trunk inlines [abstract] in [Qed]ed proofs, so we might as well not
[abstract] things in the first place.

No idea why this change speeds up
theories/categories/Pseudofunctor/RewriteLaws.v in trunk (though not
HoTT/coq); why are [constructor] and [reflexivity] fast while [exact
idpath] is slow...?