aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2003-11-17Inteprétation des idents filtrés liants dans constrintern.ml (plus robuste)herbelin
2003-11-17Un ident filtre est liant seulement si une variable deja liee (sinon bug dans...herbelin
2003-11-17majfilliatr
2003-11-16Bug filtrage pour inversion notationherbelin
2003-11-15Amelioration du message d'erreur en cas de tentative d'instanciationclrenard
2003-11-15Bug nommage destructherbelin
2003-11-15Meilleure solution pour la compatibiliteherbelin
2003-11-15Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammarherbelin
2003-11-15Ajout Print Implicit avec depliage du typeherbelin
2003-11-14MAJ dateherbelin
2003-11-14Pour les .v8herbelin
2003-11-14Move des hyps de NewInduction: retour a situation V7.4 a defaut d'etre robusteherbelin
2003-11-14MAJherbelin
2003-11-14Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_baseherbelin
2003-11-14Conflit renommageherbelin
2003-11-14cosmetiqueherbelin
2003-11-14Presentationherbelin
2003-11-14Oublis dans les rennomagesherbelin
2003-11-14Check bavard meme en mode silencieux, car on l'a vouluherbelin
2003-11-14Ordre standard pour l'associativiteherbelin
2003-11-14Quelques oublis pour que les notations marchent bienherbelin
2003-11-14Compatibilite %Therbelin
2003-11-14Bug implicit argumentsherbelin
2003-11-14Correction chemin de Zherbelin
2003-11-14Automatisation de la traduction de iff_trans; renommage IFherbelin
2003-11-14Backtrack sur Peanoherbelin
2003-11-14Nouveaux lemmes 'canoniques'; compatibiliteherbelin
2003-11-14Suppression renommages dans Peanoherbelin
2003-11-14Bug parsing castherbelin
2003-11-14majfilliatr
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...barras
2003-11-13Traduction Print Grammarherbelin
2003-11-13Oubli report Nul/Posherbelin