aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zcompare.v
Commit message (Expand)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | Remove the deprecation for some 8.2-8.5 compatibility aliases.Gravatar Théo Zimmermann2018-03-02
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* 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
* 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
* Some more cleanup of ZorderGravatar letouzey2011-06-23
* Zcompare.destr_zcompare subsumed by case Z.compare_specGravatar letouzey2011-06-20
* Clean-up of Zcompare and ZorderGravatar letouzey2011-06-20
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* Modularization of BinPos + fixes in StdlibGravatar letouzey2011-05-05
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedTypeGravatar letouzey2010-02-09
* Better visibility of the inductive CompSpec used to specify comparison functionsGravatar letouzey2009-11-03
* 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
* OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithGravatar letouzey2009-07-24
* Fix bug #1899: no more strange notations for Qge and QgtGravatar letouzey2008-07-04
* Mise en forme des theoriesGravatar notin2006-10-17
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
* 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
* Simplification; ajout Zcompare_antisymGravatar herbelin2003-11-21
* Restructuration ZArithGravatar herbelin2003-11-12