aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/PArith/BinPosDef.v
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* eta contractionsGravatar Pierre Boutillier2014-10-01
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Cbn reduces Pos.compare p~1 q~1 to Pos.compare p qGravatar Pierre Boutillier2014-05-26
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Pos.iter arguments in a better order for cbn.Gravatar Pierre Boutillier2014-05-02
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
* Pos.compare_cont takes the comparison as first argumentGravatar Pierre Boutillier2014-02-28
* "Boolean Equality" and "Case Analysis" are already off by default...Gravatar letouzey2013-07-17
* nat_iter n f x -> nat_rect _ x (fun _ => f) nGravatar pboutill2012-12-21
* Updating headers.Gravatar herbelin2012-08-08
* Functions *_beq aren't generated anymore, remove comments about themGravatar letouzey2012-05-30
* Cleanup of files related with power over Z.Gravatar letouzey2011-07-01
* Numbers: change definition of divide (compat with Znumtheory)Gravatar letouzey2011-06-24
* Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)Gravatar letouzey2011-05-05
* BinNatDef containing all functions of BinNat, misc adaptations in BinPosGravatar letouzey2011-05-05
* BinPosDef: a module with all code about positive, later Included in BinPosGravatar letouzey2011-05-05