The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Benedict Kavanagh wrote:
> What is the current status of the 8.0 documentation, specifically as 
> regards the tutorial. Is there a tutorial available for 8.0 and if not, 
> how usable will the 7.4 tutorial be for 8.0?
>
> I looked for a FAQ and couldn't find one. Is there one? all links I 
> found in the mailing list archive were dead ends.
>
> Cheers,
> Ben
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


Although it is not really a tutorial, you can consult the following site,
made by Yves Bertot and myself, which contains 170 solved exercises and 
proof scripts (written in V8.0beta)


http://www.labri.fr/Perso/~casteran/CoqArt/index.html

Pierre


--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran