aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-10-21Type relation dans Datatypesherbelin
2003-10-21Construction des chemins de constantes plus robusteherbelin
2003-10-21Optimisation de gen_constant_in_modulesherbelin
2003-10-21Extension de Locateherbelin
2003-10-21Nouvelle fonction cherchant tous les noms d'un suffixe donneherbelin
2003-10-21Bug Abstract en presence de LetIn; essai d'un Assumption d'abord avec alpha-c...herbelin
2003-10-21*** empty log message ***barras
2003-10-21Bug Locate Notationherbelin
2003-10-21Correction bug FreshIdherbelin
2003-10-21MAJherbelin
2003-10-21Maintenant avant Datatypesherbelin
2003-10-21ajoutsherbelin
2003-10-20majfilliatr
2003-10-20Globalisation des hints autorewriteherbelin
2003-10-20R passe dans Set !herbelin
2003-10-20bug traduction de auto.(simpl). en auto.simpl.barras
2003-10-20*** empty log message ***barras
2003-10-19Extension de l'utilisation de contradictionherbelin
2003-10-18Extension de Contradiction au cas d'hypotheses ~A et A dans le contexteherbelin
2003-10-1720 est uniquement associatif a gaucheherbelin
2003-10-17majfilliatr
2003-10-17On n'autorise plus les niveaux doubles L/R en v8herbelin
2003-10-17Des implicites plus 'naturels' pour eq_ind, identity_ind and coherbelin
2003-10-17Re-desactivation de l'affichage des projectionsherbelin
2003-10-17Bug mot-cle TYPESherbelin
2003-10-17Bug des terminaux quotésherbelin
2003-10-17Divers bugs d'affichageherbelin
2003-10-17Traduction des idents aussi dans le printer generique des tactiquesherbelin
2003-10-17subst marche dans les deux sensfilliatr
2003-10-16majfilliatr
2003-10-16nouvelle syntaxe de ltacbarras
2003-10-16print_projections a true juste pour le bench nocturneherbelin
2003-10-16lettac -> setbarras
2003-10-16Marge presqu'a 80, maximum indentation a 50 pour une meilleure lisibiliteherbelin
2003-10-16*** empty log message ***barras
2003-10-16oups! ca compile maintenantbarras
2003-10-16translator avoids printing a . followed by a ( by inserting a spacebarras
2003-10-16Ground update + Linear removalcorbinea
2003-10-16Syntax errorherbelin
2003-10-16Message d'erreurherbelin
2003-10-16Debranchement de l'affichage systematique des projections avec la notation po...herbelin
2003-10-16Suppression des surcharge de regles de grammaire en v7herbelin
2003-10-16Debranchement de l'affichage systematique des projections avec la notation po...herbelin
2003-10-16Branchement sur RIneqherbelin
2003-10-16Pour eviter des regles redondantes en v7herbelin
2003-10-16FTC_P2 maintenant dans RIneqherbelin
2003-10-16Ajout de quelques lemmes clesherbelin
2003-10-16Bug Searchherbelin
2003-10-15Mise en conformite return_type en fonction de la docherbelin
2003-10-15Affichage = au lieu de == en v7herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 04:22:59 +0000