aboutsummaryrefslogtreecommitdiff
path: root/theories/Lists
AgeCommit message (Expand)Author
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...notin
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-03-17Modification des propriétés (svn:executable)notin
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-15Ajout de theories/FSets contenant la partie "light" de FSets et FMap:letouzey
2006-02-22MAJherbelin
2005-11-30changement parametres inductifs dans les theoriesmohring
2005-03-16MAJ PolyList -> Listherbelin
2004-12-19In_dec transparent (wish #902)herbelin
2004-07-16Nouvelle en-têteherbelin
2004-03-28Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...herbelin
2003-12-24Ajout delimiteur et arguments de scope pour listherbelin
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-10-23Commentairesherbelin
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
2003-10-15Nettoyage argument de nilherbelin
2003-10-10MAJ commentairesherbelin
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
2003-10-03Cacher les .v8herbelin
2003-09-26Induction -> NewInduction; '++' pour appherbelin
2003-09-24Destruct/Induction -> NewDestruct/NewInductionherbelin
2003-09-22Implicits maintenant au courant pour l'affichageherbelin
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
2003-09-19'::' est deja pris en V7herbelin
2003-09-19Ajout notation :: pour consherbelin
2003-04-10Calcul automatique de l'implicite de nil pour que l'affichage sache le traiterherbelin
2003-04-09cast de nilherbelin
2003-04-09nil en implicite dans la v8herbelin
2003-04-07Cosmetiqueherbelin
2003-03-12*** empty log message ***barras
2002-04-17*** empty log message ***werner
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-03-13Ajout de lemmesmohring
2002-02-22Doc + ajout fold_symmetric et nth_Inherbelin
2002-02-14option -dump-glob pour coqdocfilliatr
2001-11-03interversion de deux Elim dans In_dec pour que la fonction extraite soit effi...letouzey
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
2001-08-13Rétablissement nom de section Map après résolution bugs surcharge de nomsherbelin
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-07-16modif Map sectionmohring
2001-04-20Library doc adjustments (until page 140)coq
2001-04-19Ajout de fonctions proposees par Cuiht Alvaradomohring