sync with stable:

sync with stable:

patches for hints & unification:

1)
===========
It is an old and know issue. The check_stack calls fo_unif_w_hints only
on a prefix of applications, leaving some arguments on the stack. This
prevents hints to be found. Example

 Hint: And A B === fun_of_morph And_morphism A B

If the problem

  And A B =?= fun_of_morph ? A B

is found immediately (before entering the KAM) the it is solved, but if
it shows up inside the KAM, A and B are left on the stack and a
fo_unif_w_hints has to solve

  And =?= fun_of_morph ?

While one could declare hints multiple times, varying the number of
actual arguments, I believe that the right solution is to make the
KAM code pass more information to fo_unif_w_hints, like the remaining
arguments. Nevertheless, the new fo_unif_w_hints is hard to factor with
the old one (that is used elsewere) so I wrote a new one called
fo_unif_heads_and_cont_or_unwind_and_hints. It first tries fo_unif on
the heads, and if successfull call a continuation (that will unify
all stack arguments pairwise) or unwinds the machine and looks for hints
on the complete terms, not just a prefix.

2)
===========
The fo_unif function does some clever higher order unification in the
case

    (? x1 ... xn)    =?=  (t y1 ... ym)

but in the very similar case

  K (? x1 ... xn) _  =?=  (t y1 ... ym)

it does not.

K has to be reduced away, and afterwards the KAM configuration
has ? and t as heads, xs and ys on the stack. Assume m-n=l, the
unification problems generated by the check_stack function are

  ?   =?=  t y1 .. yl
  xi  =?=  yl+i            for i in 1 .. n

That is clearly suboptimal, since xn and ym could differ, but a clever
instantiation of the flexible head could drop or move around xm.

Moreover one expects the two unification problems to be solved in the
same way by the system, but it does not, and in my case the second one
actually fails. The KAM code should just be a speedup over a naive
unfolding of constants, beta-iota-zeta reduction and fo_unif, but in
this (unfortunate) case it is weaker.

3)
============
The delift function does a lot of work even if the metavariable is being
instantiated with a closed term. This is very often the case when the
term is suggested by hints. Hints may suggest constants in partially
unfolded form (see paper submitted to Type09), that can thus be very
big. This simple patch speeds up delift in this case.