aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith/BinInt.v
AgeCommit message (Expand)Author
2010-02-09ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedTypeletouzey
2009-11-10DecidableType: A specification via boolean equality as an alternative to eq_decletouzey
2009-09-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-05-28- Modification de la déf de minus et pred conformément aux remarques deherbelin
2008-05-27Cyclic31: migrate auxiliary lemmas to their legitimate filesletouzey
2008-05-11- Changement du code de Zplus pour accomoder ring qui sinon prend uneherbelin
2008-02-10Proposal of a nice notation for constructors xI and xO of type positiveletouzey
2007-11-08setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. letouzey
2007-11-01In agreement with Laurent Thery, start migration of auxiliary results letouzey
2007-08-08Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.vemakarov
2007-07-18A generic preprocessing tactic zify for (r)omegaletouzey
2006-10-17Mise en forme des theoriesnotin
2006-05-31ajout de QArith dans les theories standardsletouzey
2004-11-12Changement dans les boxed values .gregoire
2004-07-16Nouvelle en-têteherbelin
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-29Report de lemmes de Znumtheory dans Zabs ou BinIntherbelin
2003-11-21ajout Pnat (suite)herbelin
2003-11-14cosmetiqueherbelin
2003-11-12Restructuration ZArithherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 18:47:34 +0000