The Coq mailing list

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

On Thu, Dec 06, 2007 at 11:11:18PM +0100, Marko Malikovi? wrote:
> Intros work but even we know what name of introduced hypothesis will be we
> can not use it because system can not be sure it will be this name. And it
> is OK.
> But pattern matching also don't work (because of the same reason I think).
> And what is the possibility of using intro in Ltac definitions if you
> don't know is product exist? To combine it with some another tactics like
> you do?
> If it is only possibility I will use it but it also seems unnaturally.
> Furthermore, even this work:
> 
> Ltac test :=
> try (intro H1;idtac).
> Goal 2+3=5 -> 5=5.
> test.

I'm not sure what exactly you are trying to do, but if you need to
'search' for the hypothesis you need in the tactic, perhaps you could do
something like

Ltac test :=
  let H := fresh in
  intro H;
  (solve_using H || test).

Where solve_using is some tactic that uses H (note: not tested, don't
have access to Coq at the moment). This basically recursively tries to
introduce a new hpothesis, tries to use that hypothesis, and if that
fails, recursively tries the next. 
  
Edsko