aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetProperties.v
Commit message (Expand)AuthorAge
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Intuition: temporary(?) restore the unconditional unfolding of notGravatar letouzey2012-05-15
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightGravatar letouzey2011-10-14
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* made several occurrences of (eapply ...; eauto) not rely on the lack of patte...Gravatar barras2009-06-22
* FMaps: various updates (mostly suggested by P. Casteran)Gravatar letouzey2008-12-26
* FMap: fold_rec + more permissive transpose hyp + various cleanupGravatar letouzey2008-12-22
* FSets: integration of suggestions by P. Casteran and S. LescuyerGravatar letouzey2008-12-18
* FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...Gravatar letouzey2008-12-17
* avoid duplicated creation of WFacts instancesGravatar letouzey2008-06-06
* repair FSets/FMap after the change in setoid rewriteGravatar letouzey2008-03-07
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
* cardinal is promoted to the rank of primitive member of the FMap interfaceGravatar letouzey2008-02-28
* Nicer third spec of choose. Gravatar letouzey2008-02-28
* Reorganization of FSet+FMap : no more files specific to Weak Sets/MapsGravatar letouzey2008-02-04
* factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...Gravatar letouzey2008-02-02
* 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
* Revision of the FSetWeak Interface, so that it becomes a precise Gravatar letouzey2007-10-29
* 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
* some more properties of fold and elements in FSetPropertiesGravatar letouzey2007-06-08
* * For uniformity, FSetAVL uses Implicit Arguments (a bit)Gravatar letouzey2007-06-07
* As suggested by Pierre Casteran, fold for FSets/FMaps now takes a Gravatar letouzey2007-05-27
* Changement de précédence de l'argument du by de assert; conséquences...Gravatar herbelin2006-05-23
* reparartion d'un petit oubli cassant PrecedenceGraphGravatar letouzey2006-05-14
* Duplication du fichier FSetProperties pour les ensembles Weak. Gravatar letouzey2006-05-11
* un lemme de double inclusionGravatar letouzey2006-04-25
* propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble d...Gravatar letouzey2006-03-16
* utilisation de removeA dans FSetPropertiesGravatar letouzey2006-03-16
* renommage NoRedun vers le plus joli NoDupGravatar letouzey2006-03-15
* Réparation de FSet (back to 8628)Gravatar notin2006-03-15
* reparation des $Gravatar letouzey2006-03-15
* Ajout de theories/FSets contenant la partie "light" de FSets et FMap:Gravatar letouzey2006-03-15
* suppression de FSets (redevient une contrib)Gravatar filliatr2003-06-24
* changement de spécif du foldGravatar letouzey2003-06-13
* FSets, mais pas compile' par make worldGravatar filliatr2003-06-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 21:13:42 +0000