The Coq mailing list

[Fr�d�ric Besson <fbesson AT irisa.fr>]

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