The Coq mailing list

[francois.garillot AT inria.fr (Fran�ois Garillot)]

On Thu, 18 Mar 2010 15:37:12 +0000, Georges Gonthier
(gonthier AT microsoft.com)
 said in
gmane.science.mathematics.logic.coq.club:4636 :

>   Like most of the rest of Coq, there is no real documentation of the
>   inner workings of Canonical Structures, other than the system code;
>   they are not covered in Coq'art, but I know Yves is cooking up some
>   kind of tutorial going over some of the design patterns that have
>   emerged from our work.

By the way, is there something looking like a rough (possibly 'hoped')
timeframe on this work ?


-- 
FG