Use setoids from the standard library

[langston-barrett]

This definition:

Class Setoid A := {
  equiv : crelation A;
  setoid_equiv :> Equivalence equiv
}.

is identical to the one from the standard library:

Class Setoid A := {
  equiv : relation A ;
  setoid_equiv :> Equivalence equiv }.

Is there any reason not to use the standard library's definition?

[langston-barrett]

Ah, I see that the definition in this library uses crelation. Never mind!

[jwiegley]

Yes, exactly. :) One of the goals of this library is not to use Prop when there is a possibility (however slight) that you may need to use something in a computational context.

[langston-barrett]

Seems like the standard library could use some of the results included here about "computational setoids"!