aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2003-10-15Gestion encore plus affinee des implicitesherbelin
2003-10-15Pour eviter que newtheories/Lists/List.v soit refait quand PolyList.v est ref...herbelin
2003-10-15Nettoyage argument de nilherbelin
2003-10-14majfilliatr
2003-10-14Gestion affinee des implicitesherbelin
2003-10-14Nouvelles traductions de noms; mot-cle; affichage implicites par le traducteurherbelin
2003-10-14En v7 sans traducteur, une incoherence virtuelle de syntaxe V8 n'est pas une ...herbelin
2003-10-14Test obsoleteherbelin
2003-10-14identityT = identityherbelin
2003-10-14Changement 'as notation' en 'where notation'herbelin
2003-10-14Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...herbelin
2003-10-14Changement 'as notation' en 'where notation'; protection 'nat_scope'; afficha...herbelin
2003-10-14Changement 'as notation' en 'where notation'; Plus d'uniformite dans la gesti...herbelin
2003-10-14Argument de except, error implicite seulement en v8; Changement 'as notation'...herbelin
2003-10-14Argument de None implicite seulement en v8herbelin
2003-10-13majfilliatr
2003-10-13Ajout projections de tripletherbelin
2003-10-13Admitted rendu independant de Conjecture: plus pratique en mode interactifherbelin
2003-10-13Ground update changing left-arrow-arrow rule.corbinea
2003-10-13Export is_section_variableherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 19:45:55 +0000