(* Reported in #12152 *)
Goal True.
intros H; auto.
Abort.