The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

Hi.

I have a set [B] with and a Fixpoint [plus_B:B->B->B]. I also have a lot
of code written in two parts that are identical except that in one I am
using [nat] and [plus] and in the other I am using [B] and [plus_B]. Is
there any way of writing this polymorphically?

Cheers,

Bernard.