New tactics: w, printtac, variants of mp, lapply, apply (now working).
New tactics: w, printtac, variants of mp, lapply, apply (now working).

As usual, to fix the behaviour of tactics we need to make more deterministic
versions of them. Because we do not have names for hypotheses yet, we pass
the arguments. Moreover, we introduce _last versions of the various tactics
that work only on the last introduced hypothesis. This is a weak form of focusing.

NOTE: weakening (w) used to remove spurious tt hypotheses.

QUESTION: what should we do with the additional hypothesis generated by
lapply? It is quite counter-intuitive, but an hypothesis is an hypothesis.

LPCIC/elpi