aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith
AgeCommit message (Expand)Author
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
2003-06-14Deplacement de le_minus de fast_integer vers Minusherbelin
2003-06-13FSets, mais pas compile' par make worldfilliatr
2003-06-13suite changements ZArith en vu de librairie FSetletouzey
2003-06-13quelques adaptations de Zarith en vu de la nouvelle librarie FSetletouzey
2003-06-13Deplacement d'un lemme sur nat de ZArith vers Arithherbelin
2003-06-10Import nat_scopeherbelin
2003-05-29niveau 49 devient nextherbelin
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ...herbelin
2003-05-07coqide: toolbar/autosavemonate
2003-04-09Ajout Open Scopeherbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".herbelin
2003-03-28Pas d'associativité gauche au niveau 3 en vieille syntaxe !herbelin
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
2003-03-21*** empty log message ***barras
2003-03-12*** empty log message ***barras
2003-02-13Modifications dans une tactique topleveldelahaye
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:26:06 +0000