aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Znat.v
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Updating headers.Gravatar herbelin2012-08-08
* 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
* Cleanup of files related with power over Z.Gravatar letouzey2011-07-01
* Deletion of useless Zdigits_defGravatar letouzey2011-06-28
* cleanup of ZsgnGravatar letouzey2011-06-23
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* Modularisation of Znat, a few name changed elsewhereGravatar letouzey2011-05-05
* BinInt: Z.add become the alternative Z.add'Gravatar letouzey2011-05-05
* First release of Vector library.Gravatar pboutill2010-12-10
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* Integer division: quot and rem (trunc convention) in addition to div and modGravatar letouzey2010-11-10
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)Gravatar herbelin2010-03-28
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* 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
* Correction du bug 1816 (ajout d'un lemme dans Znat) et suppressionGravatar notin2008-03-28
* Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...Gravatar letouzey2007-11-06
* A generic preprocessing tactic zify for (r)omegaGravatar letouzey2007-07-18
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
* Mise en forme des theoriesGravatar notin2006-10-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Restructuration ZArithGravatar herbelin2003-11-12