The Coq mailing list

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

Dear Coq users and developers,

if I have Ltac like this:

Ltac example :=
match goal with
| [ |- expression1 ] => tactic1
| [ |- expression2 ] => tactic2
| [ |- expression3 ] => tactic3
...
| [ |- expressionN ] => tacticN
| [ |- _ ] => idtac
end.

and I apply this matching on all before generated subgoals (with ;example
tactical), how I can know which tactic is applied on which subgoal.
Exactly I need ordinal number of subgoal.
Concrete, if after ";example", tactic3 is applied on i-th subgoal than I
need what number i is.

Thanx in advance,

Marko Malikoviæ