aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-10-04Reparation plus juste de l'inefficacite avec loaded_modules (respecte l'ordre)herbelin
2003-10-04NEW*VO doit apparaitre apres *VO + diversherbelin
2003-10-04majfilliatr
2003-10-03pr_vernac est paresseux; States.unfreeze seulement après que msgnl aitherbelin
2003-10-03Bug cible newtheories/Init + diversherbelin
2003-10-03Cacher les .v8herbelin
2003-10-03Correction bug explosion de la taille de la liste loaded_modulesherbelin
2003-10-03Nettoyage, simplification et compatibilite -jherbelin
2003-10-03oubli de deux flags -v7letouzey
2003-10-03*** empty log message ***barras
2003-10-02Pas de renommage des noms de sectionherbelin
2003-10-02as au niveau de appherbelin
2003-10-02Hypothesis mot-cleherbelin
2003-10-02Traduction des tests success et test en v8herbelin
2003-10-02Plus de nom commencant par '_' en V8herbelin
2003-10-02Le nom '_' n'est plus valable en v8 pour nommer les variablesherbelin
2003-10-01Retour sur la version non optimisee de 'add' pour compatibilite; renommage Un...herbelin
2003-10-01cosmetiqueherbelin
2003-10-01Implantation de l'option 'format' des Notationsherbelin
2003-10-01majfilliatr
2003-09-30'_ = _ = _' maintenant predefini, meme en V7herbelin
2003-09-30Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'herbelin
2003-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
2003-09-30code mortherbelin
2003-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
2003-09-30Ajout 'Close Scope'.herbelin
2003-09-30Ajout 'Close Scope'.herbelin
2003-09-30Ajout 'Close Scope'.herbelin
2003-09-29Oubli du type du terme a filtrer quand pas d'argument dans la traduction de caseherbelin
2003-09-29Prise en compte d'un inductif sans argument dans le 'in' des 'match'herbelin
2003-09-28oupsletouzey
2003-09-282 pbs de plus réglés concernant Setoid Ring:letouzey
2003-09-28une induction de moins dans lt_eq_lt_decletouzey
2003-09-28well_founded_induction de nouveau transparentletouzey
2003-09-27majfilliatr
2003-09-26Bug aboutherbelin
2003-09-26Syntaxe plus liberale pour le type des arguments de filtrage du 'match'herbelin
2003-09-26Syntaxe plus liberale pour le type des arguments de filtrage du 'match'; trad...herbelin
2003-09-26MAJherbelin
2003-09-26pa_ifdef.cmo redondantherbelin
2003-09-26Ajout now_showherbelin
2003-09-26About, Infixherbelin
2003-09-26'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...herbelin
2003-09-26Ajout 'About'herbelin
2003-09-26Induction -> NewInduction; '++' pour appherbelin
2003-09-26Nouvelle serie de traductionsherbelin
2003-09-26Re-possibilite changement chaine infixe en passant v7 a v8herbelin
2003-09-26Passage de Destruct a NewDestruct; '-' pour negbherbelin
2003-09-26Structuration de fast_integer en operations sur positive, proprietes des oper...herbelin
2003-09-26Un peu plus de souplesse dans la globalisation des noms utilises par les tact...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 17:08:05 +0000