first [ a; idtac "a did it!" | b; idtac "b did!" | idtac "nope"; fail ]

Goal True / True.
  split; idtac "Split did it!".

Goal True / True.
  split; [ idtac "Split did it!" | .. ].

Goal True / True.
  tauto; [ idtac "Tauto did it!" | .. ].

Goal True / True.
  split; idtac "Split did it!".

$ ~/.local64/coq/coq-8.5pl3/bin/coqtop
Welcome to Coq 8.5pl3 (November 2016)

Coq < Goal True / True.
1 subgoal

  ============================
    True / True

Unnamed_thm < split; idtac "Split did it!".
Split did it!
2 subgoals

  ============================
    True

subgoal 2 is:
 True

Unnamed_thm <