Two bugs fixed in the apply tactic:

Two bugs fixed in the apply tactic:
 1. an application of a term of type t where t reduces to a product does not
    fail any longer: t is unfolded as required to produce enough products.
    E.g. apply (t: ~A) when the goal is False
 2. the apply tactic does not fail any longer when the goal is a product.
    When the head of the type of the term is flexible, the type is a product
    and the goal is a product (e.g. t: A -> ? vs A' -> B) the less instantiated
    term (i.e. t) is tried first; in case of failure (e.g. A not unifiable with
    A') t is instantiated adding one metavariable after another.