aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2003-10-13Bug introduit dans start_proof par le commit precedentherbelin
2003-10-13Argument implicite pour None, error, exceptherbelin
2003-10-13MAJherbelin
2003-10-13Notations pour l'exponentiationherbelin
2003-10-13Enregistrement '^' en v8herbelin
2003-10-13Cleaningherbelin
2003-10-13Ameliration affichage inductifsherbelin
2003-10-13Un Try supplementaire utile pour la compatibilite, car bring_hyps dans genera...herbelin
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
2003-10-13Petits bugsherbelin
2003-10-13Deplacement next_global_ident_away dans Termopsherbelin
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
2003-10-13Deplacement pr_subgoal and co vers Pfeditherbelin
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
2003-10-13Protection contre les noms de lemmes existant dejaherbelin
2003-10-13Deplacement pr_subgoal and co vers Pfedit; Ajout SearchNamedherbelin
2003-10-13Deplacement next_global_ident_away dans Termopsherbelin
2003-10-12majfilliatr
2003-10-11reparation Undo suiteherbelin
2003-10-11Uniformisation comportement decompEq pour corriger un bug introduit dans le I...herbelin
2003-10-11Bug calcul du nom de la premiere equationherbelin
2003-10-11translate_file etait abusivement positionneherbelin
2003-10-11Ajout fnl() dans Aboutherbelin
2003-10-11Logic_TypeSyntax disparuherbelin
2003-10-11Death of 'a somewhat cryptic module'herbelin
2003-10-11Death of 'a somewhat cryptic module'herbelin
2003-10-11mise a jour nouvelle syntaxebarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 22:00:15 +0000