[New prelude repository Matthieu Sozeau **20080621163132] [New monads/comonads based on join/duplicate and derivation of bind/cobind. Highly generic versions using Equivalences. Matthieu Sozeau **20080623153131] [Update to new Functor/Pointed/... hierarchy Matthieu Sozeau **20080630105035] [A try at PERs... Matthieu Sozeau **20080828145251] [Add some standard modules I reused in other places Matthieu Sozeau **20080828222040] [Use setoids in structures and generalize laws to arbitrary (not just equivalence) relations Matthieu Sozeau **20080903073331] [Update up to Monad.v to use setoids Matthieu Sozeau **20090721125546] [Add properties Matthieu Sozeau **20090908135425] [Comment out problematic instance mkMap_morph2 in Basics Samuel Bronson **20090909021239 Ignore-this: 84a3270f01e9758823faab17c718bfaa ] [Fix up do_return_eta in Monad Samuel Bronson **20090909022337 Ignore-this: 893961bd492ec1626d0faa55d603a0e9 ] [Fix up Properties.v for the coq 8.2 typeclass syntax Samuel Bronson **20090909023602 Ignore-this: 3efe4ab68b5b3061ad35bb3d0769f4e5 ] [Fix up most of Product; comment the rest. Samuel Bronson **20090909033815 Ignore-this: 7716abddf77c979f4df7c6b6054efb95 ] [Update Properties, fix Sum & Product; start Monoid Samuel Bronson **20090909220919 Ignore-this: ee0156f48bd37f04e5000ae64c37c1d7 ] [Make Monad, CoMonad, Monoid and Product go through Matthieu Sozeau **20090910213429] [Attempt at making option_eq inductive -> bug Samuel Bronson **20090914205254 Ignore-this: cb91c878a4b968c7a186a8fd7b113952 ] [Start of update to current coq Matthieu Sozeau **20100129160856]