The Coq mailing list

[Fr�d�ric Gava <frederic.gava AT wanadoo.fr>]

Merci beacoup,

j'ai réussi avec vos commandes:

Intros A B l1.
NewInduction l1;Simpl;Intros;Auto.
NewInduction l2;Simpl;Auto.
NewDestruct l2;Simpl;Auto.
Elim (IHl1 l);Simpl;Intros;Auto with zarith.
Qed


----- Original Message -----
From: "Hugo Herbelin" 
<hugo.herbelin AT inria.fr>
To: "Frédéric Gava" 
<frederic.gava AT wanadoo.fr>
Sent: Friday, January 23, 2004 12:16 PM
Subject: Re: [Coq-Club] Problem with length of list


>
> > Thanks for your answer. I have try your solution bu now I have the
error:
> >
> > "Error: l is used in conclusion"
> >
> > What is "l" ?
>
>   Double Induction est buggé dans la V7.4 (cf rapport de bug numéro
> 356). Utilisez la V7.4bugfix (via le cvs anonyme), la V8.0beta ou
> rabattez-vous sur "NewInduction l1; NewDestruct l2" qui est moins
> puissant mais plus convivial.
>
>   Bon courage,
>
>   Hugo Herbelin