The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Coq.Structures.Orders uses module types.

It is advised to not use module types at 
http://coq.inria.fr/cocorico/RecordsNotModules

My question: Should we start to build on Coq.Structures.Orders or first 
rewrite it from scratch?

I studied a reasonably big subset of Coq and my now attempt to start writing 
formalizing mathematics, if it will happen that I will find time.

Should I first rewrite Coq.Structures.Orders?

-- 
Victor Porton - http://portonvictor.org