aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith
AgeCommit message (Expand)Author
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
2003-01-22Bug precedenceherbelin
2003-01-21Adaptation à la nouvelle sémantique plus uniforme de "Match term"herbelin
2003-01-06bit vectorsfilliatr
2002-12-28Re-installation nombres dans les motifs sur Zherbelin
2002-12-15Ajout syntaxe '>'herbelin
2002-12-10Compatibilite times1 (suite)herbelin
2002-12-09Nouvelle preuve de times_convert pour nouvelle définition de timesherbelin
2002-12-07Compatibilité times1herbelin
2002-12-06Un axiome en attendant la mise a jour de la preuve de times_convertherbelin
2002-12-06Amélioration sensible de l'efficacité de la multiplicationherbelin
2002-12-02Z_scope doit annuler l'affichage de = entreherbelin
2002-11-26Correction affichage entiers en cas d'échecherbelin
2002-11-25Rétablissement affichage des entiers de natherbelin
2002-11-24Traitement des parenthèses de nat au niveau du printerherbelin
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...herbelin
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
2002-10-22Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...herbelin
2002-10-13Mise en place d'ensembles de notations symboliques pour nat, Z et Rherbelin
2002-09-25Affaiblissement de l'ordre sur Z on demande x < y et seulementmohring
2002-07-09Making the sumbool functions transparent, so that they can used tobertot
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
2002-06-19deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwffilliatr
2002-06-07Adding file theories/ZArith/Zsqrt.v that contains a square root function.bertot
2002-06-06Correction non reconnaissance des variables de section dans les afficheurs de...herbelin
2002-06-05affaiblissement hyp de Zmult_reg_leftfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 16:28:11 +0000