aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* suite tentative pour permettre l'utilisation de modules de FSetsGravatar letouzey2006-05-20
* 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@8829 85f007b7-540e-04...Gravatar letouzey2006-05-18
* Typo dans List.vGravatar notin2006-05-17
* Ajout de [count_occ] dans List.vGravatar notin2006-05-17
* etoffage des notions de permutations (a la fois List.Permutation et Permutati...Gravatar letouzey2006-05-16
* 3*rienGravatar letouzey2006-05-15
* ajout d'exemples de decidable typesGravatar letouzey2006-05-15
* petit ajout concernant InAGravatar letouzey2006-05-15
* On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_posGravatar letouzey2006-05-14
* In_dec de nouveau transparentGravatar letouzey2006-05-14
* reparartion d'un petit oubli cassant PrecedenceGraphGravatar letouzey2006-05-14
* typoGravatar letouzey2006-05-13
* un Zgcd calculant dans coqGravatar letouzey2006-05-13
* une fonction pouvant calculer le gcd en coqGravatar letouzey2006-05-11
* quelques ajouts venant des fichiers de Evelyne C. Gravatar letouzey2006-05-11
* decidabilite de InA Gravatar letouzey2006-05-11
* Duplication du fichier FSetProperties pour les ensembles Weak. Gravatar letouzey2006-05-11
* r9089@thot: notin | 2006-05-10 14:40:51 +0200Gravatar notin2006-05-11
* un Zgcd general gardant trace des coefsGravatar letouzey2006-05-05
* suite de l'ajout des FSets/FMaps dans les theories standardsGravatar letouzey2006-04-29
* meilleur nommage pour PairOrderedTypeGravatar letouzey2006-04-29
* qq proprietes de plus sur NcompareGravatar letouzey2006-04-29
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* 2-3 lemmes en plus pour que les Bvectors soient effectivement utilisablesGravatar letouzey2006-04-27
* suite du pont entre Bvector et NGravatar letouzey2006-04-26
* Un gros coup de lifting pour IntMap: Gravatar letouzey2006-04-25
* un lemme de double inclusionGravatar letouzey2006-04-25
* New unification can solve the problem without eta-expansion, Gravatar msozeau2006-04-10
* versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesGravatar letouzey2006-04-06
* versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesGravatar letouzey2006-04-06
* ouverture du bon scope (positive_scope) derriere le constructeur Npos de NGravatar letouzey2006-04-06
* on utilise explicitement Prop/iff pour certains morphismes pour eviter des wa...Gravatar letouzey2006-04-05
* Réajout de eq_rec_eq oublié lors de la modularisation de EqdepGravatar herbelin2006-03-30
* pour coqdocGravatar letouzey2006-03-29
* Nommage explicite de certains "intro" pour préserver la compatibilitéGravatar herbelin2006-03-28
* reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / Ordere...Gravatar letouzey2006-03-28
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
* ajout d'un debut de proprietes pour les FSetWeakGravatar letouzey2006-03-17
* deux tags $ mal formesGravatar letouzey2006-03-16
* propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble d...Gravatar letouzey2006-03-16
* utilisation de removeA dans FSetPropertiesGravatar letouzey2006-03-16
* renommage NoRedun vers le plus joli NoDupGravatar letouzey2006-03-15
* TypoGravatar letouzey2006-03-15
* TypoGravatar letouzey2006-03-15
* Ajout de fonctions sur les listesGravatar notin2006-03-15
* Réparation de FSet (back to 8628)Gravatar notin2006-03-15
* encore un essaiGravatar letouzey2006-03-15
* reparation des $Gravatar letouzey2006-03-15