aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/reduction.ml
Commit message (Expand)AuthorAge
* test: un boolean et une fonction check_for_interrupt inseree dans la conversi...Gravatar filliatr2003-04-08
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* 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
* Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)Gravatar herbelin2001-09-07
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* Depliage des let-in dans le test de gardeGravatar herbelin2001-07-03
* Nettoyage/restructuration des ensembles d'indicateurs de réductionsGravatar herbelin2001-07-02
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Changement de la structure des points fixesGravatar barras2001-05-03
* reduction des let in dans whd_programsGravatar filliatr2001-04-23
* réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...Gravatar filliatr2001-04-11
* réparation Correctness; options Extraction (changement de syntaxe)Gravatar filliatr2001-04-10
* amelioration de la structure des universGravatar barras2001-03-28
* 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
* retire profileGravatar mohring2001-02-28
* Changement de subst_metaGravatar mohring2001-02-28
* Déplacement du type stack de Reduction vers Closure et utilisation pour accÃ...Gravatar herbelin2000-12-26
* Bug mauvais environnement dans le test d'eta-conversionGravatar herbelin2000-12-20
* Ajout map_constr_with_full_binders et strong pour SimplGravatar herbelin2000-11-27
* deplacement poly_args; iterateurs sur les segmentsGravatar filliatr2000-11-22
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au moment ...Gravatar herbelin2000-10-26
* Bug réduction suite modifs let-inGravatar herbelin2000-10-24
* Simplifications/questionsGravatar herbelin2000-10-23
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Idem pour défs locales dans VarGravatar herbelin2000-10-11
* Delta des défs locales en de Bruijn toujours pas stableGravatar herbelin2000-10-11
* Bug splay_prod_assumGravatar herbelin2000-10-06
* Mise en conformité nouveau Simpl pour FixGravatar herbelin2000-10-04
* Touche finale à la réduction du let in dans conv et closureGravatar herbelin2000-10-04
* Renommage AppL en AppGravatar herbelin2000-10-01
* Code comateuxGravatar herbelin2000-10-01
* Retrait de whd_ise1_metasGravatar herbelin2000-09-26
* On laisse les LetIn dans les types des constructeurs et des éliminationsGravatar herbelin2000-09-15
* Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...Gravatar herbelin2000-09-14
* Vers la paramétrisation des fonctions de Reduction et vers la fusion deGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Retrait de decomp_prod non conforme à sa specGravatar herbelin2000-06-02
* Bug DLAM dans strongGravatar herbelin2000-06-02
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 15:36:29 +0000