| Commit message (Expand) | Author | Age |
|---|
| * | 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-18 |
| * | 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 |
| * | fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2... | letouzey | 2010-06-18 |
| * | fsetdec: clear dependent hypothesis before anything else (fix #2136). | letouzey | 2010-06-17 |
| * | Made option "Automatic Introduction" active by default before too many | herbelin | 2010-06-08 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | CompSpecType, a clone of CompSpec but in Type instead of Prop | letouzey | 2010-02-12 |
| * | Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders* | letouzey | 2010-01-07 |
| * | Include can accept both Module and Module Type | letouzey | 2010-01-07 |
| * | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey | 2009-12-09 |
| * | 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 |
| * | List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F... | letouzey | 2009-11-02 |
| * | Remove various useless {struct} annotations | letouzey | 2009-11-02 |
| * | FSetCompat: a compatibility wrapper between FSets and MSets | letouzey | 2009-10-20 |
| * | Merge SetoidList2 into SetoidList. | letouzey | 2009-10-19 |
| * | Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet... | letouzey | 2009-10-16 |
| * | MSets: a new generation of FSets | letouzey | 2009-10-13 |
| * | 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-10-08 |
| * | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey | 2009-09-28 |
| * | Delete trailing whitespaces in all *.{v,ml*} files |  glondu | 2009-09-17 |
| * | Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements | letouzey | 2009-09-09 |
| * | Fix the bug-ridden code used to choose leibniz or generalized |  msozeau | 2009-09-08 |
| * | OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith | letouzey | 2009-07-24 |
| * | Better comparison functions in OrderedTypeEx | letouzey | 2009-07-22 |
| * | Simplify eauto and fix it for compatibility, allowing full delta during | msozeau | 2009-07-14 |
| * | Use the proper unification flags in e_exact. This makes exact fail a bit | msozeau | 2009-07-09 |
| * | made several occurrences of (eapply ...; eauto) not rely on the lack of patte... |  barras | 2009-06-22 |
| * | Rename [Morphism] into [Proper] and [respect] into [proper] to comply | msozeau | 2009-04-21 |
| * | Just export RelationClasses for [Equivalence] through Setoid. | msozeau | 2009-04-18 |
| * | ZArith/Int: no need to load romega here (but rather in FullAVL) | letouzey | 2009-03-28 |
| * | FSet(Weak)List : eq_dec becomes Defined (and gets better proof) | letouzey | 2009-01-28 |
| * | Switched to "standardized" names for the properties of eq and | herbelin | 2009-01-01 |
| * | - Another bug in get_sort_family_of (sort-polymorphism of constants and | herbelin | 2008-12-28 |
| * | FMaps: various updates (mostly suggested by P. Casteran) | letouzey | 2008-12-26 |
| * | FMap: fold_rec + more permissive transpose hyp + various cleanup | letouzey | 2008-12-22 |
| * | FSets: integration of suggestions by P. Casteran and S. Lescuyer | letouzey | 2008-12-18 |
| * | Better compatibility after commit 11693 by adding an alias OrderedTypeFacts.e... | letouzey | 2008-12-17 |
| * | FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec... | letouzey | 2008-12-17 |
| * | Structural definition of PositiveMap.fold | glondu | 2008-12-11 |
| * | Make PositiveMap.xmapi structural | glondu | 2008-12-11 |
| * | integrate suggestions by B. Baydemir (see #1930) | letouzey | 2008-11-17 |
| * | Port [rewrite] tactics to open terms. Currently no check that evars | msozeau | 2008-11-05 |
| * | Add user syntax for creating hint databases [Create HintDb foo | msozeau | 2008-09-14 |
| * | Correction du bug #1937 |  notin | 2008-09-04 |
| * | Enhanced discrimination nets implementation, which can now work with | msozeau | 2008-06-27 |
| * | avoid duplicated creation of WFacts instances | letouzey | 2008-06-06 |
herbelin
letouzey
glondu
msozeau
barras
notin