aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
Commit message (Expand)AuthorAge
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Reparation reduce_to_mindGravatar mohring2001-02-01
* - coqc : option -imageGravatar filliatr2001-02-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
* Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...Gravatar herbelin2000-12-20
* Debut de nettoyage de SimplGravatar mohring2000-12-18
* PrinterGravatar mohring2000-12-15
* LetIn dans SimplGravatar mohring2000-12-14
* Hint Unfold Local + commentairesGravatar mohring2000-12-12
* Debut de reparation de simplGravatar mohring2000-12-11
* La table de pré-évaluation des constantes ne doit pas persister au dischargeGravatar herbelin2000-11-27
* Prise en compte des let-in dans les fonctions de réduction pour les tactiquesGravatar herbelin2000-11-27
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Tables des eval_constant devient une CstmapGravatar herbelin2000-11-20
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Bug Simpl avec Cases cache sous plusieurs constantesGravatar herbelin2000-10-26
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Bugs de la réduction de Fix dans SimplGravatar herbelin2000-10-05
* Nouvelle stratégie de nommage dans Simpl pour FixGravatar herbelin2000-10-04
* Nouveau bug dans la réduction de Fix par red_elim_constGravatar herbelin2000-10-04
* Renommage AppL en AppGravatar herbelin2000-10-01
* Plus de whd_castappGravatar herbelin2000-10-01
* Déplacement de fonctions de Reduction vers TacredGravatar 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
* index devenu list_index échoue maintenant avec Not_found et plus FailureGravatar herbelin2000-07-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Plus besoin de env dans reduce_mind_caseGravatar herbelin2000-03-21
* BroutillesGravatar herbelin2000-01-20
* Plus d'unfold inutile des Fix dans SimplGravatar herbelin2000-01-13
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* - états fabriqués avec -silentGravatar filliatr1999-12-13
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-19 07:24:09 +0000