The Coq mailing list

[Claudio Sacerdoti Coen <sacerdot AT cs.unibo.it>]

> > les Setoids
> ils ne me conviennent pas car: 
> - pas de "polymorphisme": je dois enregistrer un Type, 
> et "forall A B: Type, A-> B -> Prop" n'en est pas un,
> ce qui me force à appeler "Add Setoid" à chaque fois je j'instancie...

 This will change in the next version of the system.
 The CVS version already accepts polymorphic relations
 (a feature still under testing).

> - de ce que j'en ai compris, il me faut prouver tous les morphismes
> que j'utilise, et c'est à ce niveau que je suis "fainéant" !

 Oui, il faut.

                                        Regards,
                                        C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: 
sacerdot AT cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------