Factoring 2ee213b824dda48c3fe60e95316daf09f07e8075.

I can't say I condone having unsafe primitives which are not used anywhere. But if they are to be there, let's make sure they don't duplicate code.
Better implementation of 4a858a51322f2dd488b02130ca82ebcc4dc9ca35.

Instead of filtering over the goals we have just creating and running through the evar_map, fetching the evar_info (that we've just created), and marking it as unresolvable, the goals are just created unresolvable. Which is probably what I should have done from the beginning, but it had escaped my notice during my code-cleaning session.
Some refactoring following previous commit.

Just hoisted a definition out of a loop. Not that this part of the code is time critical at all. I just feel it's cleaner.
Refine primitive: [unsafe] is now true by default.

Generally, tactics build type-correct terms. A safe refine is hence a waste of time (somtimes a significant one). The safe option is kept for specific purposes such as debugging, or some weird interaction with the pretyper and universes which still seemed to hold last time I checked (used by the user-level refine tactic).
Occur-check in refine.

The occur check is done even if the flag [unsafe] is set to true. The rational is that a tactic cannot control where it takes pieces of terms from (and hence will not generally make terms which pass the occur-check), and it would be painful to ask every tactic which takes a term as an argument to do an occur check before [refine].

I reused the same error than used by unification. It gives a pretty nice error message. An alternative would be to have a dedicated error with pretty much the same error message. I'm not sure which is best, so I went for the simplest one.

The same check is done in the compatibility layer.

Fixes a reported bug which I cannot locate for some reason.