aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
Commit message (Expand)AuthorAge
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
* retour en arriere concernant la recherche d'occurence modulo expansion des le...Gravatar barras2002-10-09
* correction de bugs:Gravatar barras2002-08-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Mise au point de declare_red_exprGravatar herbelin2002-05-30
* Finalement un seul constr pour l'instant dans ExtraRedExprGravatar herbelin2002-05-30
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* Non dépliage des Fix non réductibles dans HnfGravatar herbelin2001-12-20
* compat ocaml 3.03Gravatar filliatr2001-12-13
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* TransparentGravatar barras2001-09-20
* Nettoyage reduce_to_ind et one_step_reduceGravatar herbelin2001-09-09
* Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)Gravatar herbelin2001-09-07
* Bug SimplGravatar herbelin2001-07-24
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* traitement du let dans red_product (tactique Red)Gravatar barras2001-06-29
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Changement de la structure des points fixesGravatar barras2001-05-03
* entetesGravatar filliatr2001-03-15
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 12:22:38 +0000