The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

François Garillot wrote:
> 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 ?
>
>
>   
Are you talking to me?

For now, I only found the time to make a few experiments, but I am not 
sure I understood enough to write a documentation yet.  I have no hope 
of finishing anything before the end of the summer.

Yves