aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/reduction.ml
Commit message (Expand)AuthorAge
* 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
* Nettoyage de GenericGravatar herbelin2000-05-31
* Bug existential_value au lieu de existential_type + divers sur existentialGravatar herbelin2000-05-25
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Restructuration des outils pour les inductifs.Gravatar herbelin2000-05-18
* Ajout d'un strong 'light'Gravatar herbelin2000-05-05
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04
* Retrait fullmind de inductive_summary pour simplicitéGravatar herbelin2000-04-27
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Plus besoin de env dans reduce_mind_case; make_arity et make_constructor sort...Gravatar herbelin2000-03-21
* Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'Gravatar herbelin2000-03-17
* Ajout du test d'égalité des vecteurs dans convert_forall2.Gravatar herbelin2000-03-08
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* clarification du codeGravatar filliatr1999-12-14
* debug discharge et inductifsGravatar filliatr1999-12-10
* - environment -> safe_environmentGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* portage modules Evarconv et EvarutilGravatar filliatr1999-11-29
* Modification pour faire compiler pretyping.ml qui maintenant compileGravatar herbelin1999-11-26
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
* module WcclausenvGravatar filliatr1999-11-22
* - module Redinfo dans library/ pour les constantes d'éliminationGravatar filliatr1999-10-22
* modules Evar_refiner et Typing_evGravatar filliatr1999-10-20
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* module LogicGravatar filliatr1999-10-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 20:27:31 +0000