The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Edward Z. Yang wrote:
> Suppose that I would like to run a tactic, but only if some hypothesis
> isn't present.  Namely, I would like to do a negated pattern match,
> i.e. a red cut.  It might seem that this would work OK:
>
> (**)
> match goal with
>     | [ H : P X | _ ] => fail 2
>     | _ => assert (P X); [eauto|]
> (**)
>
> Unfortunately, 'fail 2' is overzealous and escapes too far.

Did you try [fail 1]?  That's what I would have attempted first.