The Coq mailing list

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

Dear Frédéric,

thank you, but anyway I know which tactic is applied to which subgoal (for
example, I have expression1, expression2, ... already in subgoals). I need
conversely think: number of subgoal for every application of tactics
tactic1, tactic2,... etc. It is because I will after tactic1, tactic2,...
apply another tactics to every subgoal, but which is another tactics it
depends on subgoal number. Fpr example:

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

Greetings,

Marko Malikoviæ

Frédéric Besson reèe:
>
> On 24 août 07, at 14:46, Marko Maliković wrote:
>
>> 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.
> Maybe you could tag subgoals with a string.
> (It does not provide the subgoal number but each subgoal is annotated
> with the tactic that applied to it.)
> Require Import String. Open Scope string_scope.
>
> Ltac example :  let tag := fresh "tag" in
>       match goal with
>       | [ |- expression1 ] => tactic1 ; set (tag := "tactic1")
>       | [ |- expression2 ] => tactic2 ; set (tag := "tactic2")
>       ...
>       | [ |- expressionN ] => tacticN ;set (tag := "tacticN")
>       | [ |- _ ] => idtac
>       end.
>
> Regards,
> --
> Frédéric Besson
>
>