aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
AgeCommit message (Expand)Author
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-05GROS COMMIT:barras
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-09-07Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)herbelin
2001-07-21Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...herbelin
2001-07-03Depliage des let-in dans le test de gardeherbelin
2001-07-02Nettoyage/restructuration des ensembles d'indicateurs de réductionsherbelin
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-03Changement de la structure des points fixesbarras
2001-04-23reduction des let in dans whd_programsfilliatr
2001-04-11réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...filliatr
2001-04-10réparation Correctness; options Extraction (changement de syntaxe)filliatr
2001-03-28amelioration de la structure des universbarras
2001-03-23amelioration de la consommation memoire de la conversion en eta-expansantbarras
2001-03-15entetesfilliatr
2001-03-01nouvelle implantation de la reductionbarras
2001-02-28retire profilemohring
2001-02-28Changement de subst_metamohring
2000-12-26Déplacement du type stack de Reduction vers Closure et utilisation pour accÃ...herbelin
2000-12-20Bug mauvais environnement dans le test d'eta-conversionherbelin
2000-11-27Ajout map_constr_with_full_binders et strong pour Simplherbelin
2000-11-22deplacement poly_args; iterateurs sur les segmentsfilliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-26Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au moment ...herbelin
2000-10-24Bug réduction suite modifs let-inherbelin
2000-10-23Simplifications/questionsherbelin
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-10-11Idem pour défs locales dans Varherbelin
2000-10-11Delta des défs locales en de Bruijn toujours pas stableherbelin
2000-10-06Bug splay_prod_assumherbelin
2000-10-04Mise en conformité nouveau Simpl pour Fixherbelin
2000-10-04Touche finale à la réduction du let in dans conv et closureherbelin
2000-10-01Renommage AppL en Appherbelin
2000-10-01Code comateuxherbelin
2000-09-26Retrait de whd_ise1_metasherbelin
2000-09-15On laisse les LetIn dans les types des constructeurs et des éliminationsherbelin
2000-09-14Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...herbelin
2000-09-12Vers la paramétrisation des fonctions de Reduction et vers la fusion deherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-06-02Retrait de decomp_prod non conforme à sa specherbelin
2000-06-02Bug DLAM dans strongherbelin
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-31Nettoyage de Genericherbelin
2000-05-25Bug existential_value au lieu de existential_type + divers sur existentialherbelin
2000-05-22suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:56:11 +0000