aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2000-10-10Plus d'échec sur les globaux lorsque prterm est appelé par le débuggerherbelin
2000-10-10Bug ordre dans push_relsherbelin
2000-10-10Finalement, encore un Simpl inutileherbelin
2000-10-10Messages d'erreurs Casesherbelin
2000-10-06MAJherbelin
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
2000-10-06MAJ pour nouvelle syntaxe des membres droits des grammairesherbelin
2000-10-06Parenthèses pour les tactiquesherbelin
2000-10-06Mise en page de Print Hintherbelin
2000-10-06Changement dans la stratégie de réduction du Fix par Simplherbelin
2000-10-06Bug splay_prod_assumherbelin
2000-10-06MAJherbelin
2000-10-06MAJ pr_uniherbelin
2000-10-06Un usage en moins de l'axiome eq_rec_eqherbelin
2000-10-06correction bug univers (dummy_univ)filliatr
2000-10-05Code mort (2ème)herbelin
2000-10-05Code mortherbelin
2000-10-05Bugs de la réduction de Fix dans Simplherbelin
2000-10-05Suppression d'un Cast inutileherbelin
2000-10-05Remplacement de la tactique Program (partiel)herbelin
2000-10-05Bug affichage des implicites; bug de compatibilité LAMBDA/LAMBDALISTherbelin
2000-10-05Bug de conflit de nommage d'hyp d'induction dans l'Induction fonctionnant dan...herbelin
2000-10-04Utilisation de local_strong plutôt que strong buggé avec défs locales (2ème)herbelin
2000-10-04Commit malencontreux sur précédente versionherbelin
2000-10-04Mise en conformité nouveau Simpl pour Fixherbelin
2000-10-04Nouvelle stratégie de nommage dans Simpl pour Fixherbelin
2000-10-04Utilisation de local_strong plutôt que strong buggé avec défs localesherbelin
2000-10-04Code mortherbelin
2000-10-04MAJherbelin
2000-10-04Ajout LetIn dans prim_extractorherbelin
2000-10-04Nouveau bug dans la réduction de Fix par red_elim_constherbelin
2000-10-04Touche finale à la réduction du let in dans conv et closureherbelin
2000-10-04Elimination des coupures sur le type constantherbelin
2000-10-04code mortherbelin
2000-10-03Renommage tactique Let en LetTacherbelin
2000-10-03Ajout castedopenconstrargherbelin
2000-10-03Ajout de globpr dans tacprherbelin
2000-10-03MAJherbelin
2000-10-03Ajout castedopenconstrarg; Renommage tactique Let en LetTacherbelin
2000-10-03Reorganisation des interp_constrherbelin
2000-10-03Rebranchement de la tactique Letherbelin
2000-10-03L'argument de Refine est un terme ouvertherbelin
2000-10-03mise en pageherbelin
2000-10-01Renommage AppL en Appherbelin
2000-10-01Renommage AppL en Appherbelin
2000-10-01Renommage AppL en App; Suppression castherbelin
2000-10-01whd_castapp_stack va de Term dans Reductionherbelin
2000-10-01Suppression de ensure_applherbelin
2000-10-01Bug message erreurherbelin
2000-10-01MAJherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 01:08:23 +0000