aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/NatInt/NZAxioms.v
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2012-08-08Updating headers.herbelin
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-07-01Cleanup of files related with power over Z.letouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2010-10-14Numbers : also axiomatize constants 1 and 2.letouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-01-08NZAxioms plus a compare allows to build an OrderedTypeletouzey
2010-01-07Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*letouzey
2010-01-07Numbers: separation of funs, notations, axioms. Notations via module, without...letouzey
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey
2009-12-17Division in Numbers : more properties, new filenames based on a paper by R. B...letouzey
2009-12-15A generic euclidean division in Numbers (Still Work-In-Progress)letouzey
2009-11-18Diamond-shape instead of linear hiearchy in Numbers/NatIntletouzey
2009-11-16New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))letouzey
2009-11-16Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsletouzey
2009-11-10Simplification of Numbers, mainly thanks to Includeletouzey
2009-11-03Numbers: start using Classes stuff, Equivalence, Proper, Instance, etcletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-06-03In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
2008-06-02In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
2008-05-22switch theories/Numbers from Set to Type (both the abstract and the bignum pa...letouzey
2008-05-15Coq headers + $ in theories/Numbers filesletouzey
2007-11-22An update on Numbers. Added two files dealing with recursion, for information...emakarov
2007-11-14Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder...emakarov
2007-11-07Replaced BinNat with a new version that is based on theories/Numbers/Natural/...emakarov
2007-10-23Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natu...emakarov
2007-10-01Added the compilation of theories/Numbers to Makefile.common. The following t...emakarov
2007-09-25An update on theories/Numbers.emakarov
2007-09-21Update on theories/Numbers. Natural numbers are mostly complete,emakarov