aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/closure.ml
Commit message (Expand)AuthorAge
* 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
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* - environment -> safe_environmentGravatar filliatr1999-12-01
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* deplacements des var. ex. hors du noyauGravatar filliatr1999-10-08
* - abstractionGravatar filliatr1999-08-26
* modules Instantiate, Constant et InductiveGravatar filliatr1999-08-25
* mach et himsg; typage sans extractionGravatar filliatr1999-08-24
* module Reduction (debut)Gravatar filliatr1999-08-18
* module ClosureGravatar filliatr1999-08-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-31 01:40:55 +0000