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