The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

I tried to use "context" in tactics. Here's example that I tried (unsuccesfully). Somehow "context" doesn't work like I had imagined although in very many cases it's okay.


Require Import Classical_Prop Setoid.

Theorem T (P: Prop): (False -> P) <-> True.
 tauto. Qed.

Theorem T0: forall n, (False -> exists m, m = S n).
 match goal with
 | [ |- context[False -> ?P] ] => setoid_rewrite T
 | _ => idtac
 end.
 setoid_rewrite T. auto.
Qed.

How can I fix it? (I read about it in adam.chlipala.net/cpdt/html/Match.html)