Major speed-up:

Major speed-up:

 1) bug fixed: the fo_unif applied to a metavariable in the subst made a
    recursive call using unify. Thus, in case of failure of the unify
    (after hints, reduction, etc.), fo_unif failed and hints, reduction,
    etc. was tried again. This resulted in an exponential blow-up in the
    worst case.
 2) bug fixed: in the case  ? args == ?pattern, the ?pattern was delifted
    w.r.t. args, but during the delift the special unification case with
    a pattern was considered again. This was costly since reduction was
    used on the first argument of the unification.
 3) semantics of fo_unif "fixed": it is now succesfull on every pair of
    terms whose rigid prefix is equal and whose arguments are unifiable.
    Before it used to fail for example on (x args == x args) where x is
    a Rel.
 4) BEHAVIOUR OF DELIFT CHANGED: it no longer matches terms in the local
    context up to full unification, but only up to fo_unif. Some tactics
    that used to be accepted could now fail and the user needs to change
    the terms by hand before applying the tactic. On the other hand, the
    speed up is really significant.