The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

No, the point is that I'll have to re-write it using hProp instead of Prop, 
so I needed the original.

V.






On May 19, 2011, at 3:00 PM, Tom Prince wrote:

> On 2011-05-19, Vladimir Voevodsky wrote:
>> where can I find the source (.v file ) for the basic library e.g.
>> Init/Peano.v ? It does not appear to be in the usual sources.
> 
> I see in an other reply, that you found this file. However, if you
> were asking so that you could include it in your repo, there is no
> need to include anything in the coq stdlib. Anybody wanting to use
> your repo will already have them installed.
> 
>  Tom