Check for undeclared universe doesn't happen at the right time in tactics #21616
Description
Ltac doit := exact Type@{u}.
Fail Definition foo := ltac:(doit).
(* undeclared univ u, error should be on the Ltac command instead of here *)
(* also in ltac2 *)
Require Import Ltac2.Ltac2.
Ltac2 doit () := exact Type@{u}.
Fail Definition foo := ltac2:(doit()).
(* undeclared univ u, error should be on the Ltac2 command instead of here *)