aboutsummaryrefslogtreecommitdiffstats
path: root/backend/SelectDivproof.v
Commit message (Expand)AuthorAgeFilesLines
* Update ARM port. Not tested yet.Xavier Leroy2016-10-251-3/+4
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-5/+247
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-2/+117
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-27/+18
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-98/+98
* Merge of "newspilling" branch:xleroy2014-07-231-0/+16
* Add option -Os to optimize for code size rather than for execution speed.xleroy2014-02-191-17/+25
* Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms xleroy2013-09-141-0/+18
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+547