aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets/FSetPositive.v
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-05-06Fix after merge.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-05-02Cbn is happier when ?SetPositive fixpoints have the set as recursive argumentPierre Boutillier
2013-07-17"Boolean Equality" and "Case Analysis" are already off by default...letouzey
2010-07-16FSetPositive: sets of positive inspired by FMapPositive.letouzey