aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith
AgeCommit message (Expand)Author
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
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...herbelin
2003-09-19Section et report Infix hors sectionherbelin
2003-09-19Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...herbelin
2003-09-12Bind et Delimit pour positive et Z (hors section)herbelin
2003-09-05principes de récurrences plus efficaces pour l'extractionletouzey
2003-09-05Zdiv plus efficace: r+r -> 2*rletouzey
2003-09-05Zabs_Zsgnletouzey
2003-08-10Un peu d'aide pour le traducteurherbelin
2003-07-18Coq.Init.Logic.eq au lieu de eqfilliatr
2003-07-08recursion bien fondee sur des pairsfilliatr
2003-06-18Arguments superflus pour Zlength_nilherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-08 00:32:37 +0000