aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets
Commit message (Collapse)AuthorAge
* Extension of NArith: Nminus, Nmin, etcGravatar letouzey2007-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7
* * For uniformity, FSetAVL uses Implicit Arguments (a bit)Gravatar letouzey2007-06-07
| | | | | | | | | | | * Some additionnal properties: - two more induction principles on sets - some results about union, filter, etc - Subset is declared to be a Setoid Relation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9882 85f007b7-540e-0410-9357-904b9bb8a0f7
* comparison functions should be Defined not QedGravatar letouzey2007-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9867 85f007b7-540e-0410-9357-904b9bb8a0f7
* As suggested by Pierre Casteran, fold for FSets/FMaps now takes a Gravatar letouzey2007-05-27
| | | | | | | | (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
* fix for bug #1347 (no more Scope pollution by FSets)Gravatar letouzey2007-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9861 85f007b7-540e-0410-9357-904b9bb8a0f7
* PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only ↵Gravatar letouzey2007-03-26
| | | | | | OrderedType git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9730 85f007b7-540e-0410-9357-904b9bb8a0f7
* Transparence de eq_dec et lt_dec daans OrderedTypeFactsGravatar notin2007-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9690 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSetInterface: new item choose_equal in the spec S (request of P. Casteran)Gravatar letouzey2007-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9684 85f007b7-540e-0410-9357-904b9bb8a0f7
* oups, ne chargeait pas les bons fichiersGravatar letouzey2006-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9278 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
* incomplete and temporary fix for PR#1222: revert accepts up to 10 argsGravatar letouzey2006-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9156 85f007b7-540e-0410-9357-904b9bb8a0f7
* comparison functions should be Defined not QedGravatar letouzey2006-08-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9066 85f007b7-540e-0410-9357-904b9bb8a0f7
* Argument Scope de list déplacé dans List.vGravatar herbelin2006-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage des graphes de Function dans Type Gravatar jforest2006-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8985 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement Int.v dans ZArith, déplacement de DecidableType.v et ↵Gravatar herbelin2006-06-09
| | | | | | DecidableTypeEx.v dans Logic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8933 85f007b7-540e-0410-9357-904b9bb8a0f7
* + ameliorating the tactic "functional induction"Gravatar jforest2006-06-06
| | | | | | | | + 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
* Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome ↵Gravatar letouzey2006-06-05
| | | | | | d'extensionalite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8897 85f007b7-540e-0410-9357-904b9bb8a0f7
* petits ajoutsGravatar letouzey2006-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8882 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replacing the old version of "functional induction" with the new one. Gravatar jforest2006-05-31
| | | | | | | 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
* * suite de la revision des wrappers MakeGravatar letouzey2006-05-30
| | | | | | | * 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
* Suite changement précédence by de assertGravatar herbelin2006-05-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de précédence de l'argument du by de assert; ↵Gravatar herbelin2006-05-23
| | | | | | conséquences sur les .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
* un debut de propriétés concernant FMapGravatar letouzey2006-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8844 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite des marquages de types et opacifications de lemmes dans les wrappers MakeGravatar letouzey2006-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8843 85f007b7-540e-0410-9357-904b9bb8a0f7
* auto with zarith genere des sous-lemmes silencieusement, Gravatar letouzey2006-05-20
| | | | | | | | 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
* suite tentative pour permettre l'utilisation de modules de FSetsGravatar letouzey2006-05-20
| | | | | | | | | 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
* on cache autant que possible Raw dans FSet(Weak)List.MakeGravatar letouzey2006-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8833 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8829 ↵Gravatar letouzey2006-05-18
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* 3*rienGravatar letouzey2006-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8820 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout d'exemples de decidable typesGravatar letouzey2006-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8819 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparartion d'un petit oubli cassant PrecedenceGraphGravatar letouzey2006-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8815 85f007b7-540e-0410-9357-904b9bb8a0f7
* Duplication du fichier FSetProperties pour les ensembles Weak. Gravatar letouzey2006-05-11
| | | | | | | | | | 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
* suite de l'ajout des FSets/FMaps dans les theories standardsGravatar letouzey2006-04-29
| | | | | | | | | | | | | | | | | | -> 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
* meilleur nommage pour PairOrderedTypeGravatar letouzey2006-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8772 85f007b7-540e-0410-9357-904b9bb8a0f7
* un lemme de double inclusionGravatar letouzey2006-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8732 85f007b7-540e-0410-9357-904b9bb8a0f7
* on utilise explicitement Prop/iff pour certains morphismes pour eviter des ↵Gravatar letouzey2006-04-05
| | | | | | warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8681 85f007b7-540e-0410-9357-904b9bb8a0f7
* pour coqdocGravatar letouzey2006-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8671 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / ↵Gravatar letouzey2006-03-28
| | | | | | OrderedType.Lt,Eq,Gt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8667 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout d'un debut de proprietes pour les FSetWeakGravatar letouzey2006-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8641 85f007b7-540e-0410-9357-904b9bb8a0f7
* propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble ↵Gravatar letouzey2006-03-16
| | | | | | des fichiers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8639 85f007b7-540e-0410-9357-904b9bb8a0f7
* utilisation de removeA dans FSetPropertiesGravatar letouzey2006-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8636 85f007b7-540e-0410-9357-904b9bb8a0f7
* renommage NoRedun vers le plus joli NoDupGravatar letouzey2006-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8635 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réparation de FSet (back to 8628)Gravatar notin2006-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8631 85f007b7-540e-0410-9357-904b9bb8a0f7
* encore un essaiGravatar letouzey2006-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8630 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation des $Gravatar letouzey2006-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8629 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de theories/FSets contenant la partie "light" de FSets et FMap:Gravatar letouzey2006-03-15
| | | | | | | | | | | | | 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
* suppression de FSets (redevient une contrib)Gravatar filliatr2003-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4205 85f007b7-540e-0410-9357-904b9bb8a0f7
* docGravatar filliatr2003-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4204 85f007b7-540e-0410-9357-904b9bb8a0f7
* concat; debut splitGravatar filliatr2003-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4203 85f007b7-540e-0410-9357-904b9bb8a0f7
* joinGravatar filliatr2003-06-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4199 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-10 01:52:56 +0000