aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2000-10-01Code comateuxherbelin
2000-10-01Plus de whd_castappherbelin
2000-10-01Chasse aux de-cast inutilesherbelin
2000-10-01renommage map_constr_with_named_bindersherbelin
2000-10-01Plus de whd_castappherbelin
2000-10-01Plus de whd_castapp_stackherbelin
2000-10-01renommage map_constr_with_named_bindersherbelin
2000-10-01Passage de la structure DOPN, DOP2, ... à une structure exprimant directemen...herbelin
2000-10-01Disparition du type oper mais nouveau type global_referenceherbelin
2000-10-01Déplacement 'a reference et binder_kind de Term vers Rawtermherbelin
2000-10-01Code mortherbelin
2000-10-01Elimination de coupures...herbelin
2000-09-26Retrait de whd_ise1_metasherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 02:24:41 +0000