aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/BinInt.v
Commit message (Expand)AuthorAge
* - Modification de la déf de minus et pred conformément aux remarques deGravatar herbelin2008-05-28
* Cyclic31: migrate auxiliary lemmas to their legitimate filesGravatar letouzey2008-05-27
* - Changement du code de Zplus pour accomoder ring qui sinon prend uneGravatar herbelin2008-05-11
* Proposal of a nice notation for constructors xI and xO of type positiveGravatar letouzey2008-02-10
* setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. Gravatar letouzey2007-11-08
* In agreement with Laurent Thery, start migration of auxiliary results Gravatar letouzey2007-11-01
* Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.vGravatar emakarov2007-08-08
* A generic preprocessing tactic zify for (r)omegaGravatar letouzey2007-07-18
* Mise en forme des theoriesGravatar notin2006-10-17
* ajout de QArith dans les theories standardsGravatar letouzey2006-05-31
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* Nouvelle en-têteGravatar herbelin2004-07-16
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Report de lemmes de Znumtheory dans Zabs ou BinIntGravatar herbelin2003-11-29
* ajout Pnat (suite)Gravatar herbelin2003-11-21
* cosmetiqueGravatar herbelin2003-11-14
* Restructuration ZArithGravatar herbelin2003-11-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 23:11:17 +0000