aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets/FMapFacts.v
AgeCommit message (Expand)Author
2012-05-15Intuition: temporary(?) restore the unconditional unfolding of notletouzey
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-01-31Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...msozeau
2012-01-28Tentative to fix bug #2628 by not letting intuition break records. Might be t...msozeau
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-10-14MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightletouzey
2011-02-16Fix compilation issues.msozeau
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
2010-12-17Cosmetic : let's take advantage of the n-ary exists notationletouzey
2010-10-22FMapFacts: typo noticed by Aaronletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
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