The Coq mailing list

[Freek Wiedijk <freek AT cs.ru.nl>]

Hi Bas,

>Some parts of the library are not used anymore.

Does that mean that the Coq proof of the Fundamental Theorem
of Algebra that was the start of the CoRN library finally has
succumbed to bit rot?  Or has it been/will it be salvaged?
Of course the thing computes voor geen meter, and it is a
minor result (it only took a single phd thesis to prove
it :-)), but still I'm kind of attached to that ancient
formalization for sentimental reasons.

Freek