The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Ltac variables cannot bind open terms.  Because your [P] would mention [n], Ltac does not match.  If you do "context[False -> _]", that should work fine.  Alternatively, remove the reference to [n] from your theorem statement, so it's just [nat -> False -> exists m, m = m] or something.

On Fri Nov 21 2014 at 1:38:23 PM Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

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)