The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

On Fri, Jun 13, 2008 at 01:00:11PM -0400, Samuel Bronson wrote:
> Is anyone doing any work on this? I'm getting tired of having to do
> everything manually because setoid_ring expects all rings to be
> pre-registered...

Yes, Matthias Puech is a student of us at INRIA who is precisely
working on this kind of automatic recognition and registration of
mathematical structures. It will not be available in Coq 8.2 though.

By the way, a beta version of Coq 8.2 is available for download at
http://coq.inria.fr/V8.2beta. It still has a few known bugs and is
intended for testing and evaluation purpose. We thank volunteer users
in advance for their feedback.

Hugo Herbelin