aboutsummaryrefslogtreecommitdiff
path: root/kernel/cooking.mli
AgeCommit message (Expand)Author
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-07-16Nouvelle en-têteherbelin
2002-10-07Lazy manuelles dans le codecoq
2002-10-05Lazy experimentale temporaire...coq
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-09-21repare la perte d'opacite a la fermeture de sectionbarras
2001-09-09Mécanisme pour faire remonter les contraintes de typage sur les variables de...herbelin
2001-08-10Parsingherbelin
2001-03-15entetesfilliatr
2000-11-20Tables séparées pour chaque type de globalherbelin
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...filliatr