aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural/BigN
AgeCommit message (Expand)Author
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
2016-09-15Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Hugo Herbelin
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-16In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Hugo Herbelin
2016-04-27Revert "In NMake_gen, giving to tactic do_size a grammar rule which respects ...Hugo Herbelin
2016-04-27In NMake_gen, giving to tactic do_size a grammar rule which respects the levels.Hugo Herbelin
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-10Give the same argument name for the record binder of type classMatthieu Sozeau
2014-10-01Simpl less (so that cbn will not simpl too much)Pierre Boutillier
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-07-17More dynamic argument scopesletouzey
2013-03-22NMake*: avoid some warning about Let outside sectionsletouzey
2012-12-21nat_iter n f x -> nat_rect _ x (fun _ => f) npboutill
2012-08-11fast bitwise operations (lor,land,lxor) on int31 and BigNletouzey
2012-08-08Updating headers.herbelin
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-12-18Granted legitimate wish #2607 (not exposing crude fixpoint body ofherbelin
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-06-30Cleanup in SpecViaZletouzey
2011-06-30Cleanup of Ndigitsletouzey
2011-06-28Deletion of useless Zdigits_defletouzey
2011-06-28Deletion of useless Zlog_defletouzey
2011-06-28Deletion of useless Zsqrt_defletouzey
2011-06-20Arithemtic: more concerning compare, eqb, leb, ltbletouzey
2011-04-18Fix generated script for NMake, a rewrite necessitates full conversion formsozeau
2011-02-11An automatic substitution of scope at functor applicationletouzey
2011-02-11Annotations at functor applications:letouzey
2011-01-04Ndigits: a Pshiftl_nat used in BigN (was double_digits there)letouzey
2010-12-09ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2letouzey
2010-12-06Numbers and bitwise functions.letouzey
2010-11-02Numbers : log2. Abstraction, properties and implementations.letouzey
2010-11-02Numbers: specs about sqrt and pow of neg numbers, even in NZletouzey
2010-10-19Add sqrt in Numbersletouzey
2010-10-14Numbers : also axiomatize constants 1 and 2.letouzey
2010-10-14Numbers: new functions pow, even, odd + many reorganisationsletouzey
2010-09-28Minor fixes of 'make doc'pboutill
2010-09-09NMake : another round of heavy reworkletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-08Fixing commit r13090 (forgot to commit the file generating Nmake_gen.v).herbelin
2010-05-19Discontinue support for ocaml 3.09.*letouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-10NMake: remove useless tactics abstract_pair, nicer commentsletouzey
2010-03-10NMake: Reorganization, interface for NMake_gen, explicit View, tactic destr_t...letouzey
2010-03-10NMake_gen.ml: robustness w.r.t size, remove old commented stuff about shiftlletouzey
2010-02-09Numbers: properties of min/max with respect to 0,S,P,add,sub,mulletouzey