coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Benjamin Gregoire <Benjamin.Gregoire AT sophia.inria.fr>
- To: Lo�c Pottier <Loic.Pottier AT sophia.inria.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] tactical
- Date: Thu, 07 Oct 2004 10:50:32 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
ou alors [i1,...in : Ti | j1....jp : Tj | ..... | _ : Tdefault]
avec i*, j* les numeros des buts.
Benjamin
Loïc Pottier wrote:
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
- [Coq-Club] tactical, Loïc Pottier
- Re: [Coq-Club] tactical, Benjamin Gregoire
Archive powered by MhonArc 2.6.16.