aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith
AgeCommit message (Expand)Author
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
2002-05-29Contournement des My_special_variableherbelin
2002-05-16suppression de inf_decidable dans ZArith_dec (pour SeachPattern)filliatr
2002-05-14encore des lemmes sur Zdivfilliatr
2002-05-14nouveaux lemmes dans Zdiv (Claude Marche)filliatr
2002-05-06Cosmétiqueherbelin
2002-04-19lemmes sur Zdiv/Zmodfilliatr
2002-04-19un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F...filliatr
2002-04-17Quelques bugs avec inject_natherbelin
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-04-08Zdiv -> Export ZArithfilliatr
2002-04-08syntaxe pour Zdiv et Zmodfilliatr
2002-04-05simplification preuvefilliatr
2002-04-05nouveau module Zdivfilliatr
2002-03-22Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...herbelin
2002-03-05petits changements afin de profiter du nouveau Rewrite/inbarras
2002-02-14option -dump-glob pour coqdocfilliatr
2002-02-14Syntaxe IF then else au lieu de either and_then or_elsebarras
2002-01-25Bug affichage de O (de nat) dans une expression sur Zherbelin
2002-01-25Zdiv et Zmod dans Zcomplementsfilliatr
2002-01-18Bug commentaire (*i i*)herbelin
2002-01-18amadouage de coqwebletouzey
2002-01-18ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contr...letouzey
2001-09-12Rustine pour gérer inject_natherbelin
2001-09-11Du bon usage des commentaires coqwebherbelin
2001-09-11Conformité des commentaires au format coqwebherbelin
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
2001-08-13Protection des commentaires pour coqtex et coqwebherbelin
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-05-31Creation du fichier Zhints.v repertoriant les thms de ZArith et definissant l...herbelin
2001-04-23Minor layout adjustments for Library doccoq
2001-04-20Library doc adjustments (until page 140)coq
2001-04-19remplace Zarith par ZArithmohring
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-14 06:59:26 +0000