The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Dear Edward,

According to your description, idtac instead of fail should be also OK:

match goal with
     | id : P X |- _ => idtac
     | _ => assert (P X); [eauto|]
end

(if you do not have some needs for which it does not match)

Best regards

Marko Malikoviæ

> 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|]
> (**)

-----------------------
Dr. Sc. Marko Malikoviæ
Filozofski fakultet
Sveuèili¹te u Rijeci
---------------------
Ph.D. Marko Malikoviæ
Faculty of Humanities and Social Sciences
University of Rijeka, Croatia
-----------------------------
marko AT ffri.hr
http://www.ffri.hr/~marko
-------------------------