The Coq mailing list

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

Of sure, this is a nonsense:

> Furthermore, even this work:
>
> Ltac test :=
> try (intro H1;idtac).
> Goal 2+3=5 -> 5=5.
> test.

because we did not try to use H1 (what is impossible because it's not
introduced in context).

Marko