The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 23/12/2015 10:40, Pierre Courtieu wrote:
> Hi,
> 
> I am not sure that Guillaume's suggestion has been understood
> completely here. In the following (the ".." is real syntax here)
> 
> tac;[> tac' | tac''..].
> 
> This will apply tac' to the first subgoal and tac' to *all others* ASFAIU.

Right, and just to make it even clearer, here is an example:

Require Import ssreflect.
Tactic Notation "\" tactic(t1) "by" tactic(t2) := t1 ; [| t2 ; fail ..].
Goal forall x, (0 = 0 -> 1 = 1 -> x = 2) -> 3 = 4.
move => x H.
\rewrite -{2}H by trivial.

Best regards,

Guillaume