aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2006-05-18git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8829 85f007b7-540e-04...letouzey
2006-05-17Typo dans List.vnotin
2006-05-17Ajout de [count_occ] dans List.vnotin
2006-05-16etoffage des notions de permutations (a la fois List.Permutation et Permutati...letouzey
2006-05-153*rienletouzey
2006-05-15ajout d'exemples de decidable typesletouzey
2006-05-15petit ajout concernant InAletouzey
2006-05-14On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_posletouzey
2006-05-14In_dec de nouveau transparentletouzey
2006-05-14reparartion d'un petit oubli cassant PrecedenceGraphletouzey
2006-05-13typoletouzey
2006-05-13un Zgcd calculant dans coqletouzey
2006-05-11une fonction pouvant calculer le gcd en coqletouzey
2006-05-11quelques ajouts venant des fichiers de Evelyne C. letouzey
2006-05-11decidabilite de InA letouzey
2006-05-11Duplication du fichier FSetProperties pour les ensembles Weak. letouzey
2006-05-11 r9089@thot: notin | 2006-05-10 14:40:51 +0200notin
2006-05-05un Zgcd general gardant trace des coefsletouzey
2006-04-29suite de l'ajout des FSets/FMaps dans les theories standardsletouzey
2006-04-29meilleur nommage pour PairOrderedTypeletouzey
2006-04-29qq proprietes de plus sur Ncompareletouzey
2006-04-28Standardisation du nom des méthodes de Evdherbelin
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...notin
2006-04-272-3 lemmes en plus pour que les Bvectors soient effectivement utilisablesletouzey
2006-04-26suite du pont entre Bvector et Nletouzey
2006-04-25Un gros coup de lifting pour IntMap: letouzey
2006-04-25un lemme de double inclusionletouzey
2006-04-10New unification can solve the problem without eta-expansion, msozeau
2006-04-06versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesletouzey
2006-04-06versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesletouzey
2006-04-06ouverture du bon scope (positive_scope) derriere le constructeur Npos de Nletouzey
2006-04-05on utilise explicitement Prop/iff pour certains morphismes pour eviter des wa...letouzey
2006-03-30Réajout de eq_rec_eq oublié lors de la modularisation de Eqdepherbelin
2006-03-29pour coqdocletouzey
2006-03-28Nommage explicite de certains "intro" pour préserver la compatibilitéherbelin
2006-03-28reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / Ordere...letouzey
2006-03-17Modification des propriétés (svn:executable)notin
2006-03-17ajout d'un debut de proprietes pour les FSetWeakletouzey
2006-03-16deux tags $ mal formesletouzey
2006-03-16propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble d...letouzey
2006-03-16utilisation de removeA dans FSetPropertiesletouzey
2006-03-15renommage NoRedun vers le plus joli NoDupletouzey
2006-03-15Typoletouzey
2006-03-15Typoletouzey
2006-03-15Ajout de fonctions sur les listesnotin
2006-03-15Réparation de FSet (back to 8628)notin
2006-03-15encore un essailetouzey
2006-03-15reparation des $letouzey
2006-03-15Ajout de theories/FSets contenant la partie "light" de FSets et FMap:letouzey
2006-03-05Modularisation des preuves concernant la logique classique, l'indiscernabilit...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:56:56 +0000