aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural/BigN
Commit message (Expand)AuthorAge
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Granted legitimate wish #2607 (not exposing crude fixpoint body ofGravatar herbelin2011-12-18
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Cleanup in SpecViaZGravatar letouzey2011-06-30
* Cleanup of NdigitsGravatar letouzey2011-06-30
* Deletion of useless Zdigits_defGravatar letouzey2011-06-28
* Deletion of useless Zlog_defGravatar letouzey2011-06-28
* Deletion of useless Zsqrt_defGravatar letouzey2011-06-28
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* Fix generated script for NMake, a rewrite necessitates full conversion forGravatar msozeau2011-04-18
* An automatic substitution of scope at functor applicationGravatar letouzey2011-02-11
* Annotations at functor applications:Gravatar letouzey2011-02-11
* Ndigits: a Pshiftl_nat used in BigN (was double_digits there)Gravatar letouzey2011-01-04
* ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2Gravatar letouzey2010-12-09
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Numbers : log2. Abstraction, properties and implementations.Gravatar letouzey2010-11-02
* Numbers: specs about sqrt and pow of neg numbers, even in NZGravatar letouzey2010-11-02
* Add sqrt in NumbersGravatar letouzey2010-10-19
* Numbers : also axiomatize constants 1 and 2.Gravatar letouzey2010-10-14
* Numbers: new functions pow, even, odd + many reorganisationsGravatar letouzey2010-10-14
* Minor fixes of 'make doc'Gravatar pboutill2010-09-28
* NMake : another round of heavy reworkGravatar letouzey2010-09-09
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fixing commit r13090 (forgot to commit the file generating Nmake_gen.v).Gravatar herbelin2010-06-08
* Discontinue support for ocaml 3.09.*Gravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* NMake: remove useless tactics abstract_pair, nicer commentsGravatar letouzey2010-03-10
* NMake: Reorganization, interface for NMake_gen, explicit View, tactic destr_t...Gravatar letouzey2010-03-10
* NMake_gen.ml: robustness w.r.t size, remove old commented stuff about shiftlGravatar letouzey2010-03-10
* Numbers: properties of min/max with respect to 0,S,P,add,sub,mulGravatar letouzey2010-02-09
* DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generationGravatar letouzey2010-02-08
* NMake (and hence BigN): shiftr, shiftl now in the signature NSigGravatar letouzey2010-01-25
* NMake: several things need not be macro-generatedGravatar letouzey2010-01-25
* Ring31 : a ring structure and tactic for int31Gravatar letouzey2010-01-19
* NMake_gen: fix previous commit (some spaces were critical), remove some more ...Gravatar letouzey2010-01-19
* NMake_gen: no more spaces at end of linesGravatar 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
* SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMaxGravatar letouzey2009-11-10
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 17:33:17 +0000