Should Ltac2 Unification.unify require a focused goal?

[SkySkimmer]

The implementation does Goal.enter https://github.com/coq/coq/blob/65ff3388b4076eed7720a45b21be13515deb54fc/tactics/tactics.ml#L3404 because it needs an env.
This means with no focused goals it does nothing which is usually a bad surprise. Also with multiple focused goals it is not very sensible.

[rlepigre]

Technically, we could use something like that (use tclENV when no focused goals). I thought we discussed this in #17777, but I can't find the discussion (maybe that was somewhere else).

[SkySkimmer]

Once #20206 is merged we can have unify_in taking an explicit env
#21654 now