aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets/FSetWeakInterface.v
AgeCommit message (Collapse)Author
2008-02-04Reorganization of FSet+FMap : no more files specific to Weak Sets/Mapsletouzey
Thanks to Elie's work and especially "Include Type ...", full sets can be simply expressed as extensions of weak sets. Moreover, Facts and Properties functors can be factorized almost completely. As a result, things like FSetWeakAAA.BBB can now be found as FSetAAA.WBBB, Same with maps / weak maps ... No backward compatibility intended for weak sets / maps, but porting scripts should mostly amounts to name changes (see above). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10505 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-29Revision of the FSetWeak Interface, so that it becomes a precise letouzey
subtype of the FSet Interface (and idem for FMapWeak / FMap). 1) No eq_dec is officially required in FSetWeakInterface.S.E (EqualityType instead of DecidableType). But of course, implementations still needs this eq_dec. 2) elements_3 differs in FSet and FSetWeak (sort vs. nodup). In FSetWeak we rename it into elements_3w, whereas in FSet we artificially add elements_3w along to the original elements_3. Initial steps toward factorization of FSetFacts and FSetWeakFacts, and so on... Even if it's not required, FSetWeakList provides a eq_dec on sets, allowing weak sets of weak sets. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10271 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-21Cleanup attempt of Hints in *Interface.v files.letouzey
See recent discussion in coq-club. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10243 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-14Rework of FSetProperties, in order to add more easily a Properties functor letouzey
for FMap (for the moment in FMapFacts). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9890 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-27As suggested by Pierre Casteran, fold for FSets/FMaps now takes a letouzey
(A:Type) instead of a (A:Set). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9863 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-153*rienletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8820 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-11Duplication du fichier FSetProperties pour les ensembles Weak. letouzey
Du coup, factorisation d'une partie dans SetoidList. Ajout de lemmes suggeres par Evelyne C. Un oubli dans FSetWeakInterface concernant elements. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8804 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-17ajout d'un debut de proprietes pour les FSetWeakletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8641 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-16propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble ↵letouzey
des fichiers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8639 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-15Réparation de FSet (back to 8628)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8631 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-15reparation des $letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8629 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-15Ajout de theories/FSets contenant la partie "light" de FSets et FMap:letouzey
pas d'implementations par AVL, mais celles par lists, ainsi que les foncteurs de proprietes. Au passage, ajout de MoreList (complements de List) et SetoidList (quelques relations sur des listes considerees modulo un eq ou lt non standard. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8628 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 05:37:04 +0000