Fixing TACTIC EXTEND for arguments-free tactics that may modify the whole
proof. Indeed, computing an empty list of arguments triggered a
Proofview.Goal.enter, which broke tactics like [shelve_unifiable].

This does not fix this particular tactic though, because the Ltac
interpreter still enters the goal when calling a Ltac reference.