aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/closure.ml
Commit message (Expand)AuthorAge
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* argument inutilisé de zip: toujours l'identitéGravatar letouzey2005-08-22
* reactivation de l optim des fermeturesGravatar barras2005-07-13
* backtrack modif de knh...Gravatar barras2005-07-13
* test du tag de reductionGravatar barras2005-07-12
* 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
* 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
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* pattern-matching avec cas inutilise dans closureGravatar barras2002-10-15
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* open Univ inutileGravatar courant2002-03-12
* cosmetiqueGravatar herbelin2002-01-30
* compat ocaml 3.03Gravatar filliatr2001-12-13
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* 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
* TransparentGravatar barras2001-09-20
* Version de la reduction dans Closure plus econome en memoire:Gravatar barras2001-09-05
* NettoyageGravatar herbelin2001-07-21
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* Nettoyage/restructuration des ensembles d'indicateurs de réductionsGravatar herbelin2001-07-02
* 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
* corrections de bug de la reductionGravatar barras2001-03-08
* 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
* Les params d'inductif deviennent en même temps propre à chaque inductif d'u...Gravatar herbelin2000-12-14
* Faut-il mettre la réduction let-in dans la réduction unfold ?Gravatar herbelin2000-11-27
* 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
* Introduction constant_path = section_pathGravatar herbelin2000-11-20
* 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
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Touche finale à la réduction du let in dans conv et closureGravatar herbelin2000-10-04
* Renommage AppL en AppGravatar herbelin2000-10-01
* Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...Gravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Suppression de AbstGravatar herbelin2000-09-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 14:34:14 +0000