aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FMapFacts.v
Commit message (Expand)AuthorAge
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...Gravatar letouzey2009-11-02
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* Simplify eauto and fix it for compatibility, allowing full delta duringGravatar msozeau2009-07-14
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* Rename [Morphism] into [Proper] and [respect] into [proper] to complyGravatar msozeau2009-04-21
* Just export RelationClasses for [Equivalence] through Setoid.Gravatar msozeau2009-04-18
* FMaps: various updates (mostly suggested by P. Casteran)Gravatar letouzey2008-12-26
* FMap: fold_rec + more permissive transpose hyp + various cleanupGravatar letouzey2008-12-22
* FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...Gravatar letouzey2008-12-17
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* Correction du bug #1937Gravatar notin2008-09-04
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
* Add the ability to specify what to do with free variables in instanceGravatar msozeau2008-04-12
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* repair FSets/FMap after the change in setoid rewriteGravatar letouzey2008-03-07
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
* A fix for compilation of FMapFacts (a story of impl arg for Logic.eq)Gravatar letouzey2008-03-02
* Some suggestions about FMap by P. Casteran: Gravatar letouzey2008-02-28
* cardinal is promoted to the rank of primitive member of the FMap interfaceGravatar letouzey2008-02-28
* Reorganization of FSet+FMap : no more files specific to Weak Sets/MapsGravatar letouzey2008-02-04
* more user-friendly versions of some properties lemmas in FSets/FMapGravatar letouzey2008-01-04
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
* Cleanup attempt of Hints in *Interface.v files.Gravatar letouzey2007-10-21
* - Extensions of FMap(Weak)Facts: Gravatar letouzey2007-06-27
* additional properties for FMap (and slight rework of SetoidList and FSetPrope...Gravatar letouzey2007-06-26
* Rework of FSetProperties, in order to add more easily a Properties functor Gravatar letouzey2007-06-14
* petits ajoutsGravatar letouzey2006-05-31
* un debut de propriétés concernant FMapGravatar letouzey2006-05-22