aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2003-10-23Commentairesherbelin
2003-10-22Documentation/Structurationherbelin
2003-10-22Documentation/Structurationherbelin
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
2003-10-21Redondance de dec_eq_natherbelin
2003-10-21Type relation dans Datatypesherbelin
2003-10-21Maintenant avant Datatypesherbelin
2003-10-21ajoutsherbelin
2003-10-20R passe dans Set !herbelin
2003-10-1720 est uniquement associatif a gaucheherbelin
2003-10-17Des implicites plus 'naturels' pour eq_ind, identity_ind and coherbelin
2003-10-16nouvelle syntaxe de ltacbarras
2003-10-16lettac -> setbarras
2003-10-16Syntax errorherbelin
2003-10-16Suppression des surcharge de regles de grammaire en v7herbelin
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-15Affichage = au lieu de == en v7herbelin
2003-10-15Nettoyage argument de nilherbelin
2003-10-14Changement 'as notation' en 'where notation'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-13Argument implicite pour None, error, exceptherbelin
2003-10-13Notations pour l'exponentiationherbelin
2003-10-13Enregistrement '^' en v8herbelin
2003-10-11mise a jour nouvelle syntaxebarras
2003-10-10nat_scope ouvert par defautherbelin
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
2003-10-10type_scopeherbelin
2003-10-10Suppression de definitions equivalentesherbelin
2003-10-10Notation '^'herbelin
2003-10-10Plus d'Eval Computeherbelin
2003-10-10MAJ commentairesherbelin
2003-10-10Delimiters N devient 'nat'herbelin
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
2003-10-03Cacher les .v8herbelin
2003-10-01Retour sur la version non optimisee de 'add' pour compatibilite; renommage Un...herbelin
2003-09-30'_ = _ = _' maintenant predefini, meme en V7herbelin
2003-09-28une induction de moins dans lt_eq_lt_decletouzey
2003-09-28well_founded_induction de nouveau transparentletouzey
2003-09-26'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...herbelin
2003-09-26Induction -> NewInduction; '++' pour appherbelin
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-25add_x_x de fast_integer vers auxiliaryherbelin
2003-09-25Retour provisoire a une sectionherbelin
2003-09-24Suppression section, ce qui evite de repliquer les declarations d'Infixherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 22:15:53 +0000