aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/closure.mli
Commit message (Expand)AuthorAge
* Changement des named_contextGravatar gregoire2005-12-02
* petites corrections + contournement bug projectionsGravatar barras2005-11-18
* *** empty log message ***Gravatar barras2005-07-13
* test du tag de reductionGravatar barras2005-07-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* Ajout de l'opti des fermeture (mais debranche pour l'instant)Gravatar barras2003-08-06
* Improved reduction machine with closure: should use less memoryGravatar barras2003-08-05
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* cosmetiqueGravatar herbelin2002-01-30
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* MAJ pour make docGravatar herbelin2001-11-09
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* TransparentGravatar barras2001-09-20
* Nettoyage des commentairesGravatar herbelin2001-09-20
* Version de la reduction dans Closure plus econome en memoire:Gravatar barras2001-09-05
* Nettoyage/restructuration des ensembles d'indicateurs de réductionsGravatar herbelin2001-07-02
* option -qualityGravatar filliatr2001-05-28
* Changement de la structure des points fixesGravatar barras2001-05-03
* to_constr renvoie directement un constr pour contourner l'ancien Term.mk_cons...Gravatar herbelin2001-04-15
* amelioration de la consommation memoire de la conversion en eta-expansantGravatar barras2001-03-23
* entetesGravatar filliatr2001-03-15
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Mise en place de la possibilite d'unfolder des variables locales et des const...Gravatar filliatr2001-01-31
* Déplacement du type stack de Reduction vers Closure et utilisation pour accÃ...Gravatar herbelin2000-12-26
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Utilisation de Let In pour les constantes locales, prise en compte des Let In...Gravatar herbelin2000-11-27
* Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabGravatar filliatr2000-11-24
* Ajout d'une fonction pour recuperer la liste des constantesGravatar delahaye2000-11-21
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Bug réduction suite modifs let-inGravatar herbelin2000-10-24
* La réduction du Let s'appelle maintenant zeta comme dans le lambda-mu-calculGravatar herbelin2000-10-23
* Touche finale à la réduction du let in dans conv et closureGravatar herbelin2000-10-04
* Minor correction for Ocamlweb + doc updateGravatar coq2000-09-14
* Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...Gravatar herbelin2000-09-14
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* - environment -> safe_environmentGravatar filliatr1999-12-01
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* deplacements des var. ex. hors du noyauGravatar filliatr1999-10-08
* - un effort sur la doc (ocamlweb)Gravatar filliatr1999-09-19
* - abstractionGravatar filliatr1999-08-26
* mise en place programmation literaire (generation de doc/coq.tex)Gravatar filliatr1999-08-19
* module Reduction (debut)Gravatar filliatr1999-08-18
* module ClosureGravatar filliatr1999-08-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-21 13:29:31 +0000