aboutsummaryrefslogtreecommitdiff
path: root/theories/NArith
AgeCommit message (Expand)Author
2019-05-23Fixing typos - Part 3JPR
2019-04-02Remove -compat 8.7Jason Gross
2018-10-29NArith: implicit length argument for Bv2NYishuai Li
2018-10-29NArith: add lemmas about numbers and vectorsYishuai Li
2018-10-02Update compat notations to be compat 8.7Jason Gross
2018-09-07NArith: deprecate N2Bv_genYishuai Li
2018-08-31Make Numeral Notation follow Import, not RequireJason Gross
2018-08-31Numeral Notation for natPierre Letouzey
2018-07-26NArith: add sized N2BvYishuai Li
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-20Decimal: simple representation of base-10 numbersPierre Letouzey
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-07-31Remove some outdated files and fix permissions.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-10-01eta contractionsPierre Boutillier
2014-10-01Simpl less (so that cbn will not simpl too much)Pierre Boutillier
2014-08-05Testing a replacement of "cut" by "enough" on a couple of test files.Hugo Herbelin
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-05-02Pos.iter arguments in a better order for cbn.Pierre Boutillier
2014-05-02Eta contractions to please cbnPierre Boutillier
2014-02-08Less dependencies in Omega.Pierre-Marie Pédrot
2013-07-17More dynamic argument scopesletouzey
2013-01-18Unset Asymmetric Patternspboutill
2012-12-21nat_iter n f x -> nat_rect _ x (fun _ => f) npboutill
2012-08-08Updating headers.herbelin
2012-07-06BinPos/BinInt/BinNat : fix some argument scopesletouzey
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-05-30Functions *_beq aren't generated anymore, remove comments about themletouzey
2011-08-11SearchAbout and similar: add a customizable blacklistletouzey
2011-07-01Cleanup of files related with power over Z.letouzey
2011-06-30Cleanup of Ndigitsletouzey
2011-06-24Numbers: change definition of divide (compat with Znumtheory)letouzey
2011-06-20Arithemtic: more concerning compare, eqb, leb, ltbletouzey
2011-05-05BinNat: N.binary_rect is now a definition instead of an opaque proofletouzey
2011-05-05Peano recursion for positive: integration of Daniel Schepler's codeletouzey
2011-05-05Minimal lemmas about Z.gt, N.gt and coletouzey
2011-05-05Modularisation of Znat, a few name changed elsewhereletouzey
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
2011-05-05Modularization of Nnatletouzey
2011-05-05Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)letouzey
2011-05-05BinNatDef containing all functions of BinNat, misc adaptations in BinPosletouzey
2011-05-05Modularization of BinNat + fixes of stdlibletouzey
2011-05-05Modularization of BinPos + fixes in Stdlibletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 02:34:31 +0000