The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

----- Mail original -----
> > These modules are already given in the standard library, look in
> > theories/Structures/OrderedTypeEx.v for Nat_as_OT for example.
> 
> Thanks. That answers the problem of getting a Nat_as_OT suitable for
> FMap.
> 
> It doesn't seem to provide a general conversion functor, which might
> not be that useful overall, but would at least be applicable for cases such
> as Q (maybe for an FSet).

Such conversion functors already exist : in theories/Structures/OrdersAlt.v,
look for Update_OT and Backport_OT.

My apologies for the current situation which is rather complex.
the transition between old-style OrderedType and the new one isn't
finished yet (some work remain to be done on FMaps for instance),
and we cannot simply remove the old-style OrderedType. Moreover,
the documentation of all these structures is clearly not sufficient yet.
Sorry for that...

Best regards,
Pierre Letouzey