aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-11-24majfilliatr
2003-11-23MAJherbelin
2003-11-23MAJsherbelin
2003-11-23Prise en compte des definitions locales dans les (co-)points-fixesherbelin
2003-11-22Compatibiliteherbelin
2003-11-22Traitement plus clair, notamment pour Locate, de quand quoter les composantes...herbelin
2003-11-22Bug introduit avec le 'Simpl f'herbelin
2003-11-22majfilliatr
2003-11-22majfilliatr
2003-11-21Suppression des niveaux videsherbelin
2003-11-21ajout Pnat et Pcompare_antisymherbelin
2003-11-21Ajout 'Simpl f'herbelin
2003-11-21Simplification; ajout Zcompare_antisymherbelin
2003-11-21ajout Pnat (suite)herbelin
2003-11-21ajout Pnat (suite)herbelin
2003-11-21Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase e...herbelin
2003-11-21Ajout Print Implicitherbelin
2003-11-21Tri et typoherbelin
2003-11-21MAJ format et docherbelin
2003-11-21Pas d'entrees autres que les predefinies en v8herbelin
2003-11-21majfilliatr
2003-11-20Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons...herbelin
2003-11-20Code simplification in CCcorbinea
2003-11-20majfilliatr
2003-11-20majfilliatr
2003-11-19ajout de Znumtheory.v dans ZArithletouzey
2003-11-19Restauration compatibilite 7.4 pour le Hint Unfold Rgtherbelin
2003-11-19Prise en compte renommagesherbelin
2003-11-19Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...herbelin
2003-11-19Deplacement subst_rawconstr dans Rawtermherbelin
2003-11-19Protection contre l'effacement des niveaux vides de operconstr et pattern par...herbelin
2003-11-19majfilliatr
2003-11-18correction suite ajout nouvelles tactiquesclrenard
2003-11-18reparation bug moins unaire (erreur de PP)barras
2003-11-18.v8herbelin
2003-11-18tout clean-ide dans cleanherbelin
2003-11-18MAJherbelin
2003-11-18Bug: faut brancher la sortie des tactiques sur stdout pendant traductionherbelin
2003-11-18Mise en place systeme de qualification des noms renommes; Renommages dans Rin...herbelin
2003-11-18Code mortherbelin
2003-11-18Blindage vis a vis des constructeurs partiellement appliquesherbelin
2003-11-18Ajout mis_constructor_nargs_envherbelin
2003-11-18Ajout recarg_lengthherbelin
2003-11-18Un nouveau lemme redondant ...herbelin
2003-11-18Deplacement ZERO_le_inj dans Zorderherbelin
2003-11-18Utilisation de la date cvs dans l'en-tete si make.result existeherbelin
2003-11-18*** empty log message ***filliatr
2003-11-18majfilliatr
2003-11-17New tactics : econstructor, eleft, eright, esplitclrenard
2003-11-17Bug affichage Hint Externherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 14:37:59 +0000