| Age | Commit message (Expand) | Author |
|---|
| 2013-07-17 | "Boolean Equality" and "Case Analysis" are already off by default... | letouzey |
| 2012-12-18 | No more constant named "int" in Coq theories (cf bug #2878) | letouzey |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-01 | Ltac repeat is in fact already doing progress | letouzey |
| 2012-08-06 | MSetRBT: a tail-recursive plength | letouzey |
| 2012-07-09 | induction/destruct : nicer syntax for generating equations (solves #2741) | letouzey |
| 2012-07-05 | 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-04-13 | MSetRBT : implementation of MSets via Red-Black trees | letouzey |
| 2012-01-17 | MSetAVL: better implementation of filter suggested by X. Leroy | letouzey |
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
| 2011-10-14 | MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right | letouzey |
| 2011-10-07 | fsetdec : non-atomic elements are now transformed as variables first (fix #2464) | letouzey |
| 2011-10-07 | Improved handling of element equalities in fsetdec (fix #2467) | letouzey |
| 2011-05-05 | Modularization of BinInt, related fixes in the 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-17 | - Use transparency information all the way through unification and | msozeau |
| 2011-01-06 | s/appartness/membership/g (Closes: #2470) | glondu |
| 2010-09-20 | Extraction: re-introduce some eta-expansions in rare situations leading to '_... | letouzey |
| 2010-09-17 | For the moment, two small manual eta-expansions to avoid '_a after extraction | letouzey |
| 2010-07-22 | Made notations for exists, exists! and notations of Utf8.v recursive notations | herbelin |
| 2010-07-16 | MSetPositive: mention MSetInterface instead of FSetInterface | letouzey |
| 2010-07-16 | FSetPositive: sets of positive inspired by FMapPositive. | letouzey |
| 2010-07-05 | FSets/Msets: some renaming of module params to simplify the task of the extra... | letouzey |
| 2010-06-18 | Report fixes from FSetDecide to MSetDecide | letouzey |
| 2010-06-16 | MSetInterface: no induction principle about a Record (nicer extraction) | letouzey |
| 2010-06-15 | MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and tre... | letouzey |
| 2010-06-08 | Made option "Automatic Introduction" active by default before too many | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-09 | Change definition of FSetList so that equality is Leibniz | glondu |
| 2010-02-12 | CompSpecType, a clone of CompSpec but in Type instead of Prop | letouzey |
| 2010-01-12 | MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu) | 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 | MSetInterface: more modularity | letouzey |
| 2010-01-07 | MSetAVL: hints made local since some of them are quite violent (transitivity) | 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-09 | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey |
| 2009-12-08 | integrate MSetToFiniteSet into the compilation (and fix it) | letouzey |
| 2009-11-30 | Fix backtracking heuristic in typeclass resolution. | msozeau |
| 2009-11-15 | Fix [Instance: forall ..., C args := t] declarations to behave as | msozeau |
| 2009-11-08 | Use generalizable variables info when internalizing arbitrary bindings, | msozeau |
| 2009-11-03 | Better visibility of the inductive CompSpec used to specify comparison functions | letouzey |
| 2009-11-03 | OrderedType implementation for various numerical datatypes + min/max structures | letouzey |
| 2009-10-27 | Add a new vernacular command for controling implicit generalization of | msozeau |
| 2009-10-21 | MSetInterface: some explicit types to avoid Raw.t-instead-of-t effect | letouzey |
| 2009-10-16 | OrderedType2 : trivial lemmas are turned into tests for order. | letouzey |
| 2009-10-16 | Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet... | letouzey |
