The Coq mailing list

["Edward Z. Yang" <ezyang AT mit.edu>]

Hmm, it looks like I was misdiagnosing the infinite loop.  Thanks!

Edward

Excerpts from Adam Chlipala's message of Sat Dec 10 14:48:56 -0500 2011:
> 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.