The Coq mailing list

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

Greetings,

can somebody give me a reason why first example work, but second not:

Ltac test :=
intro H1;
compute in H1;
assumption.
Goal 2+3=5 -> 5=5.
test.


Ltac test :=
try intro H1;
compute in H1;
assumption.
Goal 2+3=5 -> 5=5.
test.

I need to build Ltac but I don't know how many intros are possible to do
in particular subgoal. Is it some solution?

Thank you very much,

Marko Malikoviæ