New option for hiding unification vars numbers (off by default)

Unification var numbers are highly volatile and make comparing logs a
complete pain in the ass. When this flag is set I'm just printing "U?"
One error message that made little sense with the new flags
Less spurious spaces when hiding implicits