Several changes:

- added a "fast" unification procedure, which is used to perform simple unifications.
Possible regressions.

- trivial and sub_mvar act on the whole goal list at once.

- cleaned and improved the constraint solving tactic