| Age | Commit message (Expand) | Author |
|---|
| 2014-07-09 | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2013-07-17 | More dynamic argument scopes | letouzey |
| 2013-03-22 | NMake*: avoid some warning about Let outside sections | letouzey |
| 2012-12-21 | nat_iter n f x -> nat_rect _ x (fun _ => f) n | pboutill |
| 2012-08-11 | fast bitwise operations (lor,land,lxor) on int31 and BigN | letouzey |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2011-12-18 | Granted legitimate wish #2607 (not exposing crude fixpoint body of | herbelin |
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
| 2011-06-30 | Cleanup in SpecViaZ | letouzey |
| 2011-06-30 | Cleanup of Ndigits | letouzey |
| 2011-06-28 | Deletion of useless Zdigits_def | letouzey |
| 2011-06-28 | Deletion of useless Zlog_def | letouzey |
| 2011-06-28 | Deletion of useless Zsqrt_def | letouzey |
| 2011-06-20 | Arithemtic: more concerning compare, eqb, leb, ltb | letouzey |
| 2011-04-18 | Fix generated script for NMake, a rewrite necessitates full conversion for | msozeau |
| 2011-02-11 | An automatic substitution of scope at functor application | letouzey |
| 2011-02-11 | Annotations at functor applications: | letouzey |
| 2011-01-04 | Ndigits: a Pshiftl_nat used in BigN (was double_digits there) | letouzey |
| 2010-12-09 | ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2 | letouzey |
| 2010-12-06 | Numbers and bitwise functions. | letouzey |
| 2010-11-02 | Numbers : log2. Abstraction, properties and implementations. | letouzey |
| 2010-11-02 | Numbers: specs about sqrt and pow of neg numbers, even in NZ | letouzey |
| 2010-10-19 | Add sqrt in Numbers | letouzey |
| 2010-10-14 | Numbers : also axiomatize constants 1 and 2. | letouzey |
| 2010-10-14 | Numbers: new functions pow, even, odd + many reorganisations | letouzey |
| 2010-09-28 | Minor fixes of 'make doc' | pboutill |
| 2010-09-09 | NMake : another round of heavy rework | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-08 | Fixing commit r13090 (forgot to commit the file generating Nmake_gen.v). | herbelin |
| 2010-05-19 | Discontinue support for ocaml 3.09.* | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-03-10 | NMake: remove useless tactics abstract_pair, nicer comments | letouzey |
| 2010-03-10 | NMake: Reorganization, interface for NMake_gen, explicit View, tactic destr_t... | letouzey |
| 2010-03-10 | NMake_gen.ml: robustness w.r.t size, remove old commented stuff about shiftl | letouzey |
| 2010-02-09 | Numbers: properties of min/max with respect to 0,S,P,add,sub,mul | letouzey |
| 2010-02-08 | DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generation | letouzey |
| 2010-01-25 | NMake (and hence BigN): shiftr, shiftl now in the signature NSig | letouzey |
| 2010-01-25 | NMake: several things need not be macro-generated | letouzey |
| 2010-01-19 | Ring31 : a ring structure and tactic for int31 | letouzey |
| 2010-01-19 | NMake_gen: fix previous commit (some spaces were critical), remove some more ... | letouzey |
| 2010-01-19 | NMake_gen: no more spaces at end of lines | letouzey |
| 2010-01-18 | More improvements of BigN, BigZ, BigQ: | letouzey |
| 2010-01-17 | BigN, BigZ, BigQ: presentation via unique module with both ops and props | letouzey |
| 2010-01-08 | Numbers: BigN and BigZ get instantiations of all properties about div and mod | letouzey |
| 2009-11-12 | BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504) | letouzey |
| 2009-11-12 | Repair interpretation of numeral for BigQ, add a printer (close #2160) | letouzey |
| 2009-11-10 | SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMax | letouzey |
| 2009-11-10 | Simplification of Numbers, mainly thanks to Include | letouzey |
