The Coq mailing list

[Lo�c Pottier <Loic.Pottier AT sophia.inria.fr>]

Bonjour, y-a-t-il une tactiquelle qui applique t0, puis t1 sur le premier but et t2 sur les autres?

la syntaxe pourrait être

 

t0;[t1|t2...]

 

 

Loïc

 

---------------------

Hi,

 

is there a tactical which applies t0, then t1 on the first subgoal and t2 on the others?

the syntax should be

 

t0;[t1|t2...]

 

Loïc