| Age | Commit message (Expand) | Author |
|---|
| 2016-10-12 | Little addition to 6eede071 for consistency of style in OrdersFacts.v. | Hugo Herbelin |
| 2016-09-17 | Further "decide equality" tests on demand of Jason. | Hugo Herbelin |
| 2016-09-15 | Extending "contradiction" so that it recognizes statements such as "~x=x" or ... | Hugo Herbelin |
| 2016-04-27 | Revert "Temporary hack to compensate missing comma while re-printing tactic" | Hugo Herbelin |
| 2016-04-27 | Temporary hack to compensate missing comma while re-printing tactic | Hugo Herbelin |
| 2016-01-13 | MMaps: remove it from final 8.5 release, since this new library isn't mature ... | Pierre Letouzey |
| 2015-12-31 | Put implicits back as in 8.4. | Matthieu Sozeau |
| 2015-12-07 | Fix some typos. | Guillaume Melquiond |
| 2015-03-06 | MMapPositive: another implementation of MMaps | Pierre Letouzey |
| 2015-03-05 | MMaps again : adding MMapList, an implementation by ordered list | Pierre Letouzey |
| 2015-03-04 | Introducing MMaps, a modernized FMaps. | Pierre Letouzey |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-07-09 | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey |
| 2014-06-01 | Making those proofs which depend on names generated for the arguments | Hugo Herbelin |
| 2014-05-09 | Restore implicit arguments of irreflexivity (fixes bug #3305). | Matthieu Sozeau |
| 2014-05-06 | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2012-12-18 | Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904) | letouzey |
| 2012-07-09 | induction/destruct : nicer syntax for generating equations (solves #2741) | letouzey |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-04-15 | Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680). | herbelin |
| 2012-01-31 | Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi... | msozeau |
| 2012-01-28 | Tentative to fix bug #2628 by not letting intuition break records. Might be t... | msozeau |
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
| 2011-08-11 | SearchAbout and similar: add a customizable blacklist | letouzey |
| 2011-07-26 | All the parameters of Compare are implicits. | pboutill |
| 2011-06-21 | Follow-up concerning eqb / ltb / leb comparisons | letouzey |
| 2011-06-20 | Arithemtic: more concerning compare, eqb, leb, ltb | letouzey |
| 2011-05-05 | Modularization of BinInt, related fixes in the stdlib | letouzey |
| 2011-05-05 | Modularization of BinNat + fixes of stdlib | letouzey |
| 2011-05-05 | Modularization of BinPos + fixes in Stdlib | letouzey |
| 2011-03-17 | CompareSpec: a slight generalization/reformulation of CompSpec | letouzey |
| 2011-03-13 | - Add modulo_delta_types flag for unification to allow full | msozeau |
| 2011-02-16 | Fix compilation issues. | msozeau |
| 2011-02-14 | - Fix treatment of globality flag for typeclass instance hints (they | msozeau |
| 2011-01-31 | A fine-grain control of inlining at functor application via priority levels | letouzey |
| 2010-12-06 | Numbers and bitwise functions. | letouzey |
| 2010-11-10 | Integer division: quot and rem (trunc convention) in addition to div and mod | letouzey |
| 2010-11-02 | Numbers: NZPowProp as a Module Type, some module variable renaming | letouzey |
| 2010-07-18 | Reverted 13293 commited mistakenly. Sorry for the noise. | herbelin |
| 2010-07-18 | Tentative de suppression de l'import automatique des hints et coercions. | herbelin |
| 2010-07-16 | FSetPositive: sets of positive inspired by FMapPositive. | letouzey |
| 2010-07-10 | Bool: iff lemmas about or, a reflect inductive, an is_true function | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-02-16 | Uniformisation Sorting/Mergesort and Structures/Orders | letouzey |
| 2010-02-12 | CompSpecType, a clone of CompSpec but in Type instead of Prop | letouzey |
| 2010-02-09 | NPeano improved, subsumes NatOrderedType | letouzey |
| 2010-02-09 | NBinary improved, contains more, subsumes NOrderedType | letouzey |
| 2010-02-09 | ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType | letouzey |
| 2010-01-17 | BigN, BigZ, BigQ: presentation via unique module with both ops and props | letouzey |
