index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
theories
/
ZArith
/
Znat.v
Age
Commit message (
Expand
)
Author
2021-04-02
Remove the omega tactic and related options
Jim Fehrle
2020-10-11
Modify ZArith/Znat.v to compile with -mangle-names
Jasper Hugunin
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2018-10-10
[coqlib] Rebindable Coqlib namespace.
Emilio Jesus Gallego Arias
2018-03-05
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-02
Remove the deprecation for some 8.2-8.5 compatibility aliases.
Théo Zimmermann
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-01-12
Update headers.
Maxime Dénès
2014-07-09
Arith: full integration of the "Numbers" modular framework
Pierre Letouzey
2012-08-08
Updating headers.
herbelin
2012-07-05
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
Notation: a new annotation "compat 8.x" extending "only parsing"
letouzey
2011-07-01
Cleanup of files related with power over Z.
letouzey
2011-06-28
Deletion of useless Zdigits_def
letouzey
2011-06-23
cleanup of Zsgn
letouzey
2011-06-20
Arithemtic: more concerning compare, eqb, leb, ltb
letouzey
2011-05-05
Modularisation of Znat, a few name changed elsewhere
letouzey
2011-05-05
BinInt: Z.add become the alternative Z.add'
letouzey
2010-12-10
First release of Vector library.
pboutill
2010-12-06
Numbers and bitwise functions.
letouzey
2010-11-18
Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits
letouzey
2010-11-10
Integer division: quot and rem (trunc convention) in addition to div and mod
letouzey
2010-07-24
Updated all headers for 8.3 and trunk
herbelin
2010-04-29
Remove the svn-specific $Id$ annotations
letouzey
2010-03-28
Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)
herbelin
2009-10-08
Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'
letouzey
2009-09-28
Fix the stdlib doc compilation + switch all .v file to utf8
letouzey
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2008-03-28
Correction du bug 1816 (ajout d'un lemme dans Znat) et suppression
notin
2007-11-06
Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...
letouzey
2007-07-18
A generic preprocessing tactic zify for (r)omega
letouzey
2006-10-27
simplif de la partie ML de ring/field
barras
2006-10-17
Mise en forme des theories
notin
2004-07-16
Nouvelle en-tête
herbelin
2003-12-15
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
barras
2003-11-29
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-12
Restructuration ZArith
herbelin