unification+pullback fix. It used to saturate a coercion (generating new metas)

unification+pullback fix. It used to saturate a coercion (generating new metas)
but not do any unification steps on them nor using them to build a new term,
thus they were left in the metasenv with no chance to be closed by subsequent
calls to unification. The meets function has been specialized takin in input a
boolean for every direction (left/right) to state if the graph can grow in this
direction and it returns saturated coercions and augmented metasenv only for
the requested directions. Still unclear to me what does it mean to search a non
triangular pullback with a boolean set to false....