The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

You need to specify an equality procedure for any use of that function, 
which the error message expresses quite nicely once you are expecting 
such things. :)  Try running "Check set_union" to see exactly what its 
type is.  Remember that, since set_union and others are defined inside a 
Section that declares a Variable and Hypothesis, these are extra 
arguments for all the Section's inhabitants.

Mateus Oliveira wrote:
> I'm having problems with the use of functions defined in
> the ListSet library. For example, the following definition
> causes an error:
>
> Require Export ListSet.
> Definition test_union(l1 l2:set nat):set nat:= set_union l1 l2.
>
> Error: In environment
> l1: set nat
> l2: set nat
> The term "l1" has type "set nat" while it is expected to have type
> "forall x y : ?1, {x=y} + {x<>y}"
>
> I don't understand why l1 must not have type "set nat" in this example.
> What should I do to make this simple definition be accepted?