aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets
AgeCommit message (Collapse)Author
2007-03-26PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only ↵letouzey
OrderedType git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9730 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-08Transparence de eq_dec et lt_dec daans OrderedTypeFactsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9690 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-10-25oups, ne chargeait pas les bons fichiersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9278 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-21incomplete and temporary fix for PR#1222: revert accepts up to 10 argsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9156 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-14comparison functions should be Defined not Qedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9066 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-09Argument Scope de list déplacé dans List.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9035 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Passage des graphes de Function dans Type jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8985 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Déplacement Int.v dans ZArith, déplacement de DecidableType.v et ↵herbelin
DecidableTypeEx.v dans Logic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8933 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06+ ameliorating the tactic "functional induction"jforest
+ bug correction in proof of structural principles + up do to date test-suite/success/Funind.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8899 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-05Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome ↵letouzey
d'extensionalite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8897 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-31petits ajoutsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8882 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-31Replacing the old version of "functional induction" with the new one. jforest
The old version is, for now, still available by prefixing any command/tactic with Old/old (eg. old functional induction ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8881 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-30* suite de la revision des wrappers Makeletouzey
* quelques unfold E.eq en cas de changement de la semantique des foncteurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8876 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-24Suite changement précédence by de assertherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8860 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Changement de précédence de l'argument du by de assert; ↵herbelin
conséquences sur les .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-22un debut de propriétés concernant FMapletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8844 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-22suite des marquages de types et opacifications de lemmes dans les wrappers Makeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8843 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-20auto with zarith genere des sous-lemmes silencieusement, letouzey
et ... <: ... with E:=Z_as_OT n'aime pas ca git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8836 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-05-18git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8829 ↵letouzey
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-15ajout d'exemples de decidable typesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8819 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-14reparartion d'un petit oubli cassant PrecedenceGraphletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8815 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-04-29suite de l'ajout des FSets/FMaps dans les theories standardsletouzey
-> OrderedTypeEx: des exemples de OrderedType -> OrderedTypeAlt: une definition alternative de OrderedType -> FSetAVL et FMapAVL: realisation a coup d'AVL -> FMapPositive: realisation a coup d'arbre binaire (selon les chiffres binaires de la cle) -> FMapIntMap : realisation en utilisant IntMap -> FSetToFiniteSet: un ensemble de FSet est un ensemble de Ensemble.v FSetAVL et FMapAVL prenent 30 secondes chacuns sur ma machine: on peut ne pas les compiler en passant l'option "-fsets no" a configure, de facon similaire a "-reals no" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8773 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-29meilleur nommage pour PairOrderedTypeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8772 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-25un lemme de double inclusionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8732 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-05on utilise explicitement Prop/iff pour certains morphismes pour eviter des ↵letouzey
warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8681 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-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-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-16utilisation de removeA dans FSetPropertiesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8636 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-15renommage NoRedun vers le plus joli NoDupletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8635 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-15encore un essailetouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8630 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-24docfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4204 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-24concat; debut splitfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4203 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23joinfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4199 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23add_tree : sur type tree plutot que sur type tfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4198 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23merge_bis et debug joinfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4197 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20removfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4191 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20mergefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4190 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-20remove_min, remove_maxfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4189 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 02:13:14 +0000