aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural/BigN/BigN.v
Commit message (Expand)AuthorAge
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-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
* More dynamic argument scopesGravatar letouzey2013-07-17
* Updating headers.Gravatar herbelin2012-08-08
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* An automatic substitution of scope at functor applicationGravatar letouzey2011-02-11
* Annotations at functor applications:Gravatar letouzey2011-02-11
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Numbers : log2. Abstraction, properties and implementations.Gravatar letouzey2010-11-02
* Numbers : also axiomatize constants 1 and 2.Gravatar letouzey2010-10-14
* Numbers: new functions pow, even, odd + many reorganisationsGravatar letouzey2010-10-14
* NMake : another round of heavy reworkGravatar letouzey2010-09-09
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Ring31 : a ring structure and tactic for int31Gravatar letouzey2010-01-19
* More improvements of BigN, BigZ, BigQ:Gravatar letouzey2010-01-18
* BigN, BigZ, BigQ: presentation via unique module with both ops and propsGravatar letouzey2010-01-17
* Numbers: BigN and BigZ get instantiations of all properties about div and modGravatar letouzey2010-01-08
* BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)Gravatar letouzey2009-11-12
* Repair interpretation of numeral for BigQ, add a printer (close #2160)Gravatar letouzey2009-11-12
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* Fix bug #1899: no more strange notations for Qge and QgtGravatar letouzey2008-07-04
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
* In abstract parts of theories/Numbers, plus/times becomes add/mul, Gravatar letouzey2008-06-03
* In abstract parts of theories/Numbers, plus/times becomes add/mul, Gravatar letouzey2008-06-02
* Enhance the BigN and BigZ infrastructure: Gravatar letouzey2008-06-01
* Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurateGravatar letouzey2008-05-16
* BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZGravatar letouzey2008-05-16
* More BigNum cleanup: Gravatar letouzey2008-05-16
* Coq headers + $ in theories/Numbers filesGravatar letouzey2008-05-15
* Integration of theories/Ints into theories/Numbers, part 1: moving filesGravatar letouzey2008-05-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 12:16:27 +0000