The Coq mailing list

[Coq Dev <coqletsgo AT yahoo.com>]

Thank you for the replies, they do work in most cases but there are still some situations where the suggested tactics do not seem to work:

Goal forall n, (forall (n : nat), ~ (n > 2)) -> (n < 3).
  intros.
  unfold not in *.
  fold_not.

I thought the "context" in the Ltacs would be able to capture such situations though. All I can manage to do are some ugly hacks, like adding specific Ltac rules:

 | H: forall x : ?t, ?p -> False |- _ => fold (forall x : t, not (p)) in H

But besides renaming the variable, it is not elegant and extensible.

There is also the fact that one of the proposed Ltacs does match in the following case, but the 'fold' does not actually do anything.

Goal forall n, (exists n' : nat, ~ (n' > 2)) -> (n < 3).
  intros.
  unfold not in *.


Is it possibly my Coq version (8.3pl1) that is buggy? Or did I misunderstand the 'context' keyword in Ltac?