aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2003-11-13Niveau V8herbelin
2003-11-13Fermeture de la section maintenant necessaireherbelin
2003-11-13factorisation et generalisation des clausesbarras
2003-11-13Passage a un SStream predicatifherbelin
2003-11-13MAJherbelin
2003-11-13Requireherbelin
2003-11-13qq petit ajouts à Zdivletouzey
2003-11-13majfilliatr
2003-11-12MAJ INZherbelin
2003-11-12MAJherbelin
2003-11-12Bug TacIdherbelin
2003-11-12Ajout lemme projectionsherbelin
2003-11-12%type au lieu de %Therbelin
2003-11-12Lemmes dans un sens plus naturelherbelin
2003-11-12Suppression du "..." final !herbelin
2003-11-12Restructuration ZArithherbelin
2003-11-12Cosmetiqueherbelin