aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cooking.ml
Commit message (Expand)AuthorAge
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* Lazy manuelles dans le codeGravatar coq2002-10-07
* Lazy experimentale temporaire...Gravatar coq2002-10-05
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* repare la perte d'opacite a la fermeture de sectionGravatar barras2001-09-21
* Mécanisme pour faire remonter les contraintes de typage sur les variables de...Gravatar herbelin2001-09-09
* ParsingGravatar herbelin2001-08-10
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* entetesGravatar filliatr2001-03-15
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* On déplie les locaux dans les types plutôt que de les quantifier par un LetGravatar herbelin2000-11-27
* Tables séparées pour chaque type de globalGravatar herbelin2000-11-20
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06