| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2010-01-17 | Simplification of OrdersTac thanks to the functor application ! with no inline | letouzey |
| 2010-01-13 | Try to avoid re-declaring Equivalence, especially for Logic.eq | letouzey |
| 2010-01-12 | GenericMinMax: still a min_case_strong with hypothesis in the wrong order | letouzey |
| 2010-01-07 | Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders* | letouzey |
| 2010-01-07 | Include can accept both Module and Module Type | letouzey |
| 2010-01-07 | Numbers: separation of funs, notations, axioms. Notations via module, without... | letouzey |
| 2010-01-07 | Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni... | letouzey |
| 2010-01-07 | OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with... | letouzey |
| 2010-01-07 | DecidableType2+OrderedType2 : notations in specific Module Type, slicing of O... | letouzey |
| 2010-01-07 | misc improvements in some Structures files | letouzey |
| 2010-01-05 | Avoid declaring hints about refl/sym/trans of eq in DecidableType2 | letouzey |
| 2010-01-04 | Specific syntax for Instances in Module Type: Declare Instance | letouzey |
| 2009-12-18 | RelationPairs: stop loading it in all Numbers, stop maximal args with fst/snd | letouzey |
| 2009-12-17 | Reverse order of arguments in min_case_strong for better uniformity (and comp... | letouzey |
