aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith/Zdiv.v
AgeCommit message (Expand)Author
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
2003-09-05Zdiv plus efficace: r+r -> 2*rletouzey
2003-04-09Ajout Open Scopeherbelin
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-21*** empty log message ***barras
2003-03-12*** empty log message ***barras
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
2002-06-05affaiblissement hyp de Zmult_reg_leftfilliatr
2002-05-14encore des lemmes sur Zdivfilliatr
2002-05-14nouveaux lemmes dans Zdiv (Claude Marche)filliatr
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-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