aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 17:35:12 +0000