| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2009-09-09 | Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements | letouzey |
| 2009-09-08 | Fix the bug-ridden code used to choose leibniz or generalized | msozeau |
| 2009-07-24 | OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith | letouzey |
| 2009-07-22 | Better comparison functions in OrderedTypeEx | letouzey |
| 2009-07-14 | Simplify eauto and fix it for compatibility, allowing full delta during | msozeau |
| 2009-07-09 | Use the proper unification flags in e_exact. This makes exact fail a bit | msozeau |
| 2009-06-22 | made several occurrences of (eapply ...; eauto) not rely on the lack of patte... | barras |
