aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets/FMapFacts.v
AgeCommit message (Expand)Author
2009-11-02List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...letouzey
2009-10-19Merge SetoidList2 into SetoidList.letouzey
2009-10-08Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'letouzey
2009-10-08Implicit argument of Logic.eq become maximally insertedletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-08Fix the bug-ridden code used to choose leibniz or generalizedmsozeau
2009-07-14Simplify eauto and fix it for compatibility, allowing full delta duringmsozeau
2009-07-09Use the proper unification flags in e_exact. This makes exact fail a bitmsozeau
2009-04-21Rename [Morphism] into [Proper] and [respect] into [proper] to complymsozeau
2009-04-18Just export RelationClasses for [Equivalence] through Setoid.msozeau
2008-12-26FMaps: various updates (mostly suggested by P. Casteran)letouzey
2008-12-22FMap: fold_rec + more permissive transpose hyp + various cleanupletouzey
2008-12-17FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...letouzey
2008-09-14Add user syntax for creating hint databases [Create HintDb foomsozeau
2008-09-04Correction du bug #1937notin
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
2008-04-12Add the ability to specify what to do with free variables in instancemsozeau
2008-04-08- A little cleanup in Classes/*. Separate standard morphisms onmsozeau
2008-03-16Reorganize Program and Classes theories. Requiring Setoid no longer setsmsozeau
2008-03-07f_equal, revert, specialize in ML, contradict in better Ltac (+doc)letouzey
2008-03-07repair FSets/FMap after the change in setoid rewriteletouzey
2008-03-06Plug the new setoid implemtation in, leaving the original one commentedmsozeau
2008-03-04migration from Set to Type of FSet/FMap + some dependencies...letouzey
2008-03-02A fix for compilation of FMapFacts (a story of impl arg for Logic.eq)letouzey
2008-02-28Some suggestions about FMap by P. Casteran: letouzey
2008-02-28cardinal is promoted to the rank of primitive member of the FMap interfaceletouzey
2008-02-04Reorganization of FSet+FMap : no more files specific to Weak Sets/Mapsletouzey
2008-01-04more user-friendly versions of some properties lemmas in FSets/FMapletouzey
2007-11-06small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is letouzey
2007-10-21Cleanup attempt of Hints in *Interface.v files.letouzey
2007-06-27- Extensions of FMap(Weak)Facts: letouzey
2007-06-26additional properties for FMap (and slight rework of SetoidList and FSetPrope...letouzey
2007-06-14Rework of FSetProperties, in order to add more easily a Properties functor letouzey
2006-05-31petits ajoutsletouzey
2006-05-22un debut de propriétés concernant FMapletouzey