Commit message (Expand) | Author | Age | |
---|---|---|---|
* | MSetRBT: unfortunate typo in compare_height (fix #3413) | Pierre Letouzey | 2014-07-10 |
* | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey | 2014-07-09 |
* | Avoid using a deprecated lemma in the standard library. | Guillaume Melquiond | 2014-06-26 |
* | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | "Boolean Equality" and "Case Analysis" are already off by default... | letouzey | 2013-07-17 |
* | Change Hint Resolve, Immediate to take a global reference as argument | msozeau | 2012-10-26 |
* | MSetRBT: a tail-recursive plength | letouzey | 2012-08-06 |
* | MSetRBT : elementary arith proofs instead of calls to lia | letouzey | 2012-07-05 |
* | ZArith + other : favor the use of modern names instead of compat notations | letouzey | 2012-07-05 |
* | MSetRBT : implementation of MSets via Red-Black trees | letouzey | 2012-04-13 |