aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets/MSetPositive.v
Commit message (Expand)AuthorAge
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* MMapPositive: another implementation of MMapsGravatar Pierre Letouzey2015-03-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Cbn is happier when ?SetPositive fixpoints have the set as recursive argumentGravatar Pierre Boutillier2014-05-02
* "Boolean Equality" and "Case Analysis" are already off by default...Gravatar letouzey2013-07-17
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* MSetPositive: mention MSetInterface instead of FSetInterfaceGravatar letouzey2010-07-16
* FSetPositive: sets of positive inspired by FMapPositive.Gravatar letouzey2010-07-16