aboutsummaryrefslogtreecommitdiff
path: root/theories/Wellfounded
AgeCommit message (Expand)Author
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...letouzey
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-03-16Reorganize Program and Classes theories. Requiring Setoid no longer setsmsozeau
2008-03-06Plug the new setoid implemtation in, leaving the original one commentedmsozeau
2007-02-12Autres passages de Set à Type dans Relations et Wellfoundedherbelin
2007-02-07Backtrack sur le passage de Set à Type pour l'ordre lexicographiqueherbelin
2007-02-06Passage de Set à Type dans Relations et Wellfoundedherbelin
2006-12-12Dépendence inutileherbelin
2006-10-17Mise en forme des theoriesnotin
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...notin
2004-07-16Nouvelle en-têteherbelin
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-03Cacher les .v8herbelin
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
2003-05-09ajout inverse relation bien fondeemohring
2003-03-12*** empty log message ***barras
2002-11-24Remplacement de Syntactic Definition par Notationherbelin
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-02-14option -dump-glob pour coqdocfilliatr
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-04-20Library doc adjustments (until page 140)coq
2001-04-19remplace Zarith par ZArithmohring
2001-04-11documentation automatique de la bibliothèque standardfilliatr
2001-03-15entetesfilliatr
2001-02-14Renommage des variables dans les schémas d'inductionherbelin
2000-11-27Changement du parseur par défaut dans Syntaxherbelin
2000-11-21Nettoyageherbelin
2000-11-21ajout de theories/Wellfoundedfilliatr