aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith
AgeCommit message (Expand)Author
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-29ground->firstorder, cc-> congruence, CC final commitcorbinea
2003-11-29Report de lemmes de Znumtheory dans Zabs ou BinIntherbelin
2003-11-24Renoncement de la compatibilite des noms qualifies au profit de la compatibil...herbelin
2003-11-22Compatibiliteherbelin
2003-11-21Simplification; ajout Zcompare_antisymherbelin
2003-11-21ajout Pnat (suite)herbelin
2003-11-19ajout de Znumtheory.v dans ZArithletouzey
2003-11-18Un nouveau lemme redondant ...herbelin
2003-11-18Deplacement ZERO_le_inj dans Zorderherbelin
2003-11-14Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_baseherbelin
2003-11-14cosmetiqueherbelin
2003-11-14Quelques oublis pour que les notations marchent bienherbelin
2003-11-14Bug implicit argumentsherbelin
2003-11-13Oubli report Nul/Posherbelin
2003-11-13Requireherbelin
2003-11-13qq petit ajouts à Zdivletouzey
2003-11-12Restructuration ZArithherbelin
2003-11-12Ajout lemmes; independance vis a vis noms variables liees; restructurationherbelin
2003-11-12Ajout partie sur bool anciennement dans Zmischerbelin
2003-11-12Ajout lemmes; independance vis a vis noms variables lieesherbelin
2003-11-09Ajout quelques lemmes; noms des variables lieesherbelin
2003-11-07Oubli BinNatherbelin
2003-11-07Oubli d'un Set Implicit Argumentsherbelin
2003-11-06Des oublisherbelin
2003-11-06Report des definitions sorties de fast_integer pour compatibiliteherbelin
2003-11-05Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...herbelin
2003-11-03Exporting ^; utilisation arg scope impliciteherbelin
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...herbelin
2003-10-28Retour en arriere sur d'autres renommages de variablesherbelin
2003-10-27Retour a un nommage non standard des variables pour compatibilite; report 're...herbelin
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-16Suppression des surcharge de regles de grammaire en v7herbelin
2003-10-13Notations pour l'exponentiationherbelin
2003-10-10Plus d'Eval Computeherbelin
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-26'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...herbelin
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
2003-09-24Destruct -> NewDestructherbelin
2003-09-22Deplacement de lemmes de IntMap vers ZArithherbelin
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
2003-09-21Conflit de nom Pplus dans positive et dans polynomial (de ring)herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 06:03:30 +0000