Typing.sort_of does not leak evarmaps anymore.
Proofview refiner is now type-safe by default.

In order not to be too costly, there is an [unsafe] flag to be set if the
tactic does not have to check that the partial proof term is well-typed (to
be used with caution though).

This patch breaks one [fix]-based example in the refine test-suite, but a huge
development like CompCert still goes through.