aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural/Abstract
AgeCommit message (Expand)Author
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-09-16Modify Numbers/Natural/Abstract/NBits.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NLcm.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NGcd.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NDiv.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NPow.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NParity.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NMaxMin.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NSub.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NAddOrder.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NOrder.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NAdd.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NBase.v to compile with -mangle-namesJasper Hugunin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-12-05Added Nat.bezout_comm.Daniel de Rauglaudre
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-08-22Fix typo of caracterisation -> c*h*aracterisationSiddharth Bhat
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-12-07Fix some typos.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-08-25"allows to", like "allowing to", is improperJason Gross
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
2012-10-01Ltac repeat is in fact already doing progressletouzey
2012-08-08Updating headers.herbelin
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-08-11SearchAbout and similar: add a customizable blacklistletouzey
2011-07-01Cleanup of files related with power over Z.letouzey
2011-06-24Numbers: a particular case of div_uniqueletouzey
2011-06-24Numbers: change definition of divide (compat with Znumtheory)letouzey
2011-06-20Some migration of results from BinInt to Numbersletouzey
2011-06-20Arithemtic: more concerning compare, eqb, leb, ltbletouzey
2011-02-17- Use transparency information all the way through unification andmsozeau
2011-01-20Numbers: simplier spec for testbitletouzey
2011-01-04f_equiv : a clone of f_equal that handles setoid equivalencesletouzey
2011-01-03Numbers: some improvements in proofsletouzey
2010-12-17Cosmetic : let's take advantage of the n-ary exists notationletouzey
2010-12-06Numbers and bitwise functions.letouzey
2010-11-18NZSqrt: we define sqrt_up, a square root that rounds up instead of down as sqrtletouzey
2010-11-18NZLog: we define log2_up, a base-2 logarithm that rounds up instead of down a...letouzey
2010-11-10Integer division: quot and rem (trunc convention) in addition to div and modletouzey
2010-11-05Numbers: axiomatization, properties and implementations of gcdletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:44:34 +0000