aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
AgeCommit message (Collapse)Author
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-07Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1928 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-21Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ↵herbelin
par le nombre d'args inutiles + vérification dans le noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1860 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-03Depliage des let-in dans le test de gardeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1822 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-02Nettoyage/restructuration des ensembles d'indicateurs de réductionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1819 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-03Changement de la structure des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-23reduction des let in dans whd_programsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1664 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-11réparation d'un bug de Correctness: whd_programs ne doit pas réduire les ↵filliatr
terms contenant des Evar pas des Metas; mise à jour des exemples git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1577 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10réparation Correctness; options Extraction (changement de syntaxe)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1571 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28amelioration de la structure des universbarras
elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23amelioration de la consommation memoire de la conversion en eta-expansantbarras
les definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1483 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01nouvelle implantation de la reductionbarras
suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28retire profilemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1413 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28Changement de subst_metamohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1412 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Déplacement du type stack de Reduction vers Closure et utilisation pour ↵herbelin
accélérer la réduction dans Closure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1221 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Bug mauvais environnement dans le test d'eta-conversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1170 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Ajout map_constr_with_full_binders et strong pour Simplherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@973 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22deplacement poly_args; iterateurs sur les segmentsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@917 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-02suppression des (* open Generic *)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au moment ↵herbelin
de l'instanciation des Meta dans plain_instance git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@769 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Bug réduction suite modifs let-inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@750 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23Simplifications/questionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@737 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec ↵herbelin
sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18Renommage canonique :herbelin
declaration = definition | assumption mode de reference = named | rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifier*constr*typed_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Idem pour défs locales dans Varherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@701 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11Delta des défs locales en de Bruijn toujours pas stableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@696 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06Bug splay_prod_assumherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@668 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Mise en conformité nouveau Simpl pour Fixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@654 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Touche finale à la réduction du let in dans conv et closureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@647 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Renommage AppL en Appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@634 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Code comateuxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@628 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-26Retrait de whd_ise1_metasherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@616 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-15On laisse les LetIn dans les types des constructeurs et des éliminationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@612 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Nouvelle version de frterm; ajout des contextes dans l'enviornnement de ↵herbelin
réduction de Closure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@602 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-12Vers la paramétrisation des fonctions de Reduction et vers la fusion deherbelin
Closure.stack avec une nouvelle abstraction des 'stacks' de Reduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@596 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Correction pour make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Suppression de Abstherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02Retrait de decomp_prod non conforme à sa specherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@496 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02Bug DLAM dans strongherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@490 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-31Nettoyage de Genericherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-25Bug existential_value au lieu de existential_type + divers sur existentialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@476 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-22suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@464 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 18:35:19 +0000