aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets/FSetInterface.v
AgeCommit message (Collapse)Author
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
By default Coq stdlib warnings raise an error, so this is really required.
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-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
Previously, hints added without a specified database where implicitly put in the "core" database, which was discouraged by the user manual (because of the lack of modularity of this approach).
2018-02-27Update headers following #6543.Théo Zimmermann
2013-01-18Unset Asymmetric Patternspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-17- Use transparency information all the way through unification andmsozeau
conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
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-07Include can accept both Module and Module Typeletouzey
Syntax Include Type is still active, but deprecated, and triggers a warning. The syntax M <+ M' <+ M'', which performs internally an Include, also benefits from this: M, M', M'' can be independantly modules or module type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 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
2008-12-18FSets: integration of suggestions by P. Casteran and S. Lescuyerletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11698 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-08better comments in FSetInterfaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10535 85f007b7-540e-0410-9357-904b9bb8a0f7
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
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-153*rienletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8820 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-29pour coqdocletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8671 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-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-01-31 21:41:27 +0000