aboutsummaryrefslogtreecommitdiff
path: root/contrib/recdef
AgeCommit message (Expand)Author
2006-02-09Minor bugs fixesbertot
2006-02-08Changing Set to Type for iter.bertot
2006-02-08One can use a measure {mes f x} instead of a well-founded relation in GenFixp...bertot
2006-02-08Julien:bertot
2006-02-03+ Adding an error message when the function cannot be definedbertot
2006-01-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
2006-01-21Messages de idtac et fail peuvent maintenant être des listes de string, int ...herbelin
2006-01-18Recursive Definition now supports functions with more than one argument.coq
2006-01-12Changing well founded induction to fix on accessibility proof in orderbertot
2006-01-11removes several warnings in contrib/interfacebertot
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...herbelin
2005-12-02Changement des named_contextgregoire
2005-11-14avoids warnings about unused variablesbertot
2005-11-07Adds tools to help in defining new general recursive functionsbertot