aboutsummaryrefslogtreecommitdiff
path: root/theories/MSets/MSetRBT.v
AgeCommit message (Expand)Author
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2014-10-01Simpl less (so that cbn will not simpl too much)Pierre Boutillier
2014-07-10MSetRBT: unfortunate typo in compare_height (fix #3413)Pierre Letouzey
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-06-26Avoid using a deprecated lemma in the standard library.Guillaume Melquiond
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-07-17"Boolean Equality" and "Case Analysis" are already off by default...letouzey
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-08-06MSetRBT: a tail-recursive plengthletouzey
2012-07-05MSetRBT : elementary arith proofs instead of calls to lialetouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-04-13MSetRBT : implementation of MSets via Red-Black treesletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 10:29:07 +0000