aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetEqProperties.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...Gravatar msozeau2012-01-31
* Tentative to fix bug #2628 by not letting intuition break records. Might be t...Gravatar msozeau2012-01-28
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsGravatar letouzey2009-09-09
* FMaps: various updates (mostly suggested by P. Casteran)Gravatar letouzey2008-12-26
* FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...Gravatar letouzey2008-12-17
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
* avoid duplicated creation of WFacts instancesGravatar letouzey2008-06-06
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
* 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
* 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
* Rework of FSetProperties, in order to add more easily a Properties functor Gravatar letouzey2007-06-14
* * For uniformity, FSetAVL uses Implicit Arguments (a bit)Gravatar letouzey2007-06-07
* Changement de précédence de l'argument du by de assert; conséquences...Gravatar herbelin2006-05-23
* Duplication du fichier FSetProperties pour les ensembles Weak. Gravatar letouzey2006-05-11
* propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble d...Gravatar letouzey2006-03-16
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 04:57:46 +0000