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