| Age | Commit message (Expand) | Author |
|---|
| 2013-07-17 | "Boolean Equality" and "Case Analysis" are already off by default... | letouzey |
| 2013-01-18 | Unset Asymmetric Patterns | pboutill |
| 2012-12-18 | No more constant named "int" in Coq theories (cf bug #2878) | letouzey |
| 2012-10-01 | Ltac repeat is in fact already doing progress | letouzey |
| 2012-07-05 | Kills the useless tactic annotations "in |- *" | letouzey |
| 2012-07-05 | Open Local Scope ---> Local Open Scope, same with Notation and alii | letouzey |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-05-15 | Intuition: temporary(?) restore the unconditional unfolding of not | letouzey |
| 2012-04-15 | Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680). | herbelin |
| 2012-03-14 | Final part of moving Program code inside the main code. Adapted add_definitio... | msozeau |
| 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-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-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-02-16 | Fix compilation issues. | msozeau |
| 2011-02-14 | - Fix treatment of globality flag for typeclass instance hints (they | msozeau |
| 2011-01-06 | s/appartness/membership/g (Closes: #2470) | glondu |
| 2010-12-17 | Cosmetic : let's take advantage of the n-ary exists notation | letouzey |
| 2010-10-22 | FMapFacts: typo noticed by Aaron | letouzey |
| 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-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-05 | FSets/Msets: some renaming of module params to simplify the task of the extra... | letouzey |
| 2010-06-18 | fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2... | letouzey |
| 2010-06-17 | fsetdec: clear dependent hypothesis before anything else (fix #2136). | 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-02-12 | CompSpecType, a clone of CompSpec but in Type instead of Prop | letouzey |
| 2010-01-07 | Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders* | letouzey |
| 2010-01-07 | Include can accept both Module and Module Type | letouzey |
| 2009-12-09 | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey |
| 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-11-02 | List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F... | letouzey |
| 2009-11-02 | Remove various useless {struct} annotations | letouzey |
| 2009-10-20 | FSetCompat: a compatibility wrapper between FSets and MSets | letouzey |
| 2009-10-19 | Merge SetoidList2 into SetoidList. | letouzey |
| 2009-10-16 | Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet... | letouzey |
| 2009-10-13 | MSets: a new generation of FSets | letouzey |
| 2009-10-08 | Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False' | letouzey |
| 2009-10-08 | Implicit argument of Logic.eq become maximally inserted | letouzey |
| 2009-09-28 | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
