aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/BinInt.v
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Pos.iter arguments in a better order for cbn.Gravatar Pierre Boutillier2014-05-02
* More dynamic argument scopesGravatar letouzey2013-07-17
* Updating headers.Gravatar herbelin2012-08-08
* BinPos/BinInt/BinNat : fix some argument scopesGravatar letouzey2012-07-06
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* BinInt: a forgotten scope for a notationGravatar letouzey2012-06-19
* SearchAbout and similar: add a customizable blacklistGravatar letouzey2011-08-11
* BinInt: more structured scripts thanks to bullets and { }Gravatar letouzey2011-08-09
* Cleanup of files related with power over Z.Gravatar letouzey2011-07-01
* Deletion of useless Zdigits_defGravatar letouzey2011-06-28
* Numbers: change definition of divide (compat with Znumtheory)Gravatar letouzey2011-06-24
* Some more cleanup of ZorderGravatar letouzey2011-06-23
* Some migration of results from BinInt to NumbersGravatar letouzey2011-06-20
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* Minimal lemmas about Z.gt, N.gt and coGravatar letouzey2011-05-05
* BinInt: Z.add become the alternative Z.add'Gravatar letouzey2011-05-05
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* Modularization of BinPos + fixes in StdlibGravatar letouzey2011-05-05
* Definitions of positive, N, Z moved in Numbers/BinNums.vGravatar letouzey2011-05-05
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* In passing, very quick uniformization of coqdoc headers in a few files.Gravatar herbelin2010-12-09
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* Add small utility lemmas about nat/P/Z/Q arithmetic.Gravatar letouzey2010-11-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedTypeGravatar letouzey2010-02-09
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - 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-11-07 22:30:15 +0000