aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets/FSetList.v
AgeCommit message (Collapse)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2016-11-24Fix some documentation typos.Guillaume Melquiond
Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*letouzey
Old stuff DecidableType.v and OrderedType.v stay there and keep their names for the moment, for compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12641 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-20FSetCompat: a compatibility wrapper between FSets and MSetsletouzey
Thanks to the functors in FSetCompat, the three implementations of FSets (FSetWeakList, FSetList, FSetAVL) are just made of a few lines adapting the corresponding MSets implementation to the old interface. This approach breaks FSetFullAVL. Since this file is of little use for stdlib users, we migrate it into contrib Orsay/FSets. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12402 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-28FSet(Weak)List : eq_dec becomes Defined (and gets better proof)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11867 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-17FSet/OrderedType now includes an eq_dec, and hence become an extension of ↵letouzey
DecidableType After lots of hesitations, OrderedType now requires this "eq_dec" field, which is redundant (can be deduced from "compare"), but allows the subtyping relation DecidableType <= OrderedType, and hence WS <= S : ordered sets are now truly extensions of weak sets. Of course this change introduces a last-minute incompatibility, but: - There is a clear gain in term of functionnality / simplicity. - FSets 8.2 already needs some adaptations when compared with 8.1, so it's the right time to push such incompatible changes. - Transition shouldn't be too hard: the old OrderedType still exists under the name MiniOrderedType, and functor MOT_to_OT allows to convert from one to the other. Beware, for a FSetInterface.WS (resp. S) to be coercible to a DecidableType (resp. OrderedType), an eq_dec on sets is now required in these interfaces and in the implementations. In pratice, it is really easy to build from equal and equal_1 and equal_2. Some name changes : in FSetFacts, old WFacts now correspond to WFacts_fun, while WFacts now expects only one argument (WFacts M := WFacts_fun M.E M). Idem with WDecide, WProperties and WEqProperties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11693 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-04migration from Set to Type of FSet/FMap + some dependencies...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Nicer third spec of choose. letouzey
The old version is now a properties in FSetProperties.OrdProperties git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10601 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05kill some useless module aliases E:=X (for better name printing, see Elie's ↵letouzey
14097) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10511 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-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
2007-02-28FSetInterface: new item choose_equal in the spec S (request of P. Casteran)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9684 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-20suite tentative pour permettre l'utilisation de modules de FSetsletouzey
avec <: au lieu de : sans surprise de modules genre Raw partout ou autres alias dépliés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8834 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-19on cache autant que possible Raw dans FSet(Weak)List.Makeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8833 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-28reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / ↵letouzey
OrderedType.Lt,Eq,Gt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8667 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
2003-06-24suppression de FSets (redevient une contrib)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4205 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13changement de spécif du foldletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4159 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13fcts tail-recursivesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4153 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13FSets, mais pas compile' par make worldfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4150 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:11:43 +0000