The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Hello.

I think that this is an interesting idea to have a kind of open standard 
library that could be contributed by anyone following some guidelines.

Le 10/03/2011 13:39, Tom Prince a écrit :
> Also, there is the issue of compatibility. There needs to be a balance
> between improving the library, and supporting code that worked against
> older versions. It wouldn't surprise me if a number of the perceived
> deficiencies of the standard library are due to the requirement to be
> backwards compatible. I think to a certain extent, both the goals that I
> outlined above run counter to maintaining backward compatibility. I
> don't think this is an insurmountable challenge, but certainly, at
> points it will lead to non-perfect code.
But I don't think we need to worry too much about backward 
compatibilities with old contributions or the current standard lib, 
because we can simply use new name spaces.

Frederic.