The Coq mailing list

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

>     I'm wondering whether the new setoid implementation is powerful enough 
> to
>    handle arbitrary relations with equality being `same_relation' from
>    `Relation_Definitions' in Coq's standard library?

 Yes, it is. However, the type of union in the standard library is

 forall A, relation A -> relation A -> A -> A -> Prop

 To be handled correctly it should be

 forall A, relation A -> relation A -> relation A.

 You can do like this:

 Definition union: forall A, relation A -> relation A -> relation A := union.

 and now Add Relation works (tested in the current SVN version of Coq).

>      produces a <<Impossible to unify "Prop" with "relation ?XXX">> or
>    <<Impossible to unify "_UNBOUND_REL_X" with "relation ?X">> error message
>    (depending on whether I try to declare union or inclusion as a morphism).

 I agree that these error messages should definitely be improved.

                                                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
----------------------------------------------------------------