The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Thu, Dec 06, 2007 at 07:51:40PM +0100, Marko Malikovi? wrote:
> 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.

The scope of the 'try' is only the 'intro H1', so it is not guaranteed
that it will succeed. Therefore, H1 may or may not be in scope when the
rest of the tactic is executed. This works:

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?

'intros' introduces all of them, but of course you won't be able to
apply them in the tactic because you won't know their name. 

Edsko