aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Integers.v
Commit message (Expand)AuthorAgeFilesLines
* Improved auto goal selection (#443)Andrej Dudenhefner2022-09-081-2/+2
* Add [#global] qualifier on Hint Rewrite (#439)Pierre-Marie Pédrot2022-07-051-0/+8
* Native support for bit fields (#400)Xavier Leroy2021-08-221-0/+112
* Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-221-2/+2
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-22/+25
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-520/+520
* More robust proof of `size_and` (#320)Frédéric Besson2019-10-301-4/+5
* AArch64 portXavier Leroy2019-08-081-24/+136
* Added Int.same_if_eqXavier Leroy2019-08-071-0/+5
* Properties of combinations of shifts and zero-/sign-extensionXavier Leroy2019-08-071-0/+249
* Define integer sign extension for zero bitsXavier Leroy2019-08-071-14/+27
* More efficient test for powers of twoXavier Leroy2019-05-091-26/+22
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-835/+33
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-10/+10
* Integers.v: add modulus_gt_one (#259)Xavier Leroy2019-03-251-1/+7
* Make the checker happy (#272)Vincent Laporte2019-02-121-8/+8
* Removed deprecated lemma.Bernhard Schommer2018-03-121-1/+1
* Added simple div_one Theorem variants.Bernhard Schommer2017-12-011-0/+6
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-57/+57
* Some lemmas.Bernhard Schommer2017-09-211-0/+14
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-43/+134
* RISC-V port and assorted changesXavier Leroy2017-04-281-3/+23
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-1/+108
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-0/+37
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-3/+454
* IA32: model integer division and modulus closer to the machineXavier Leroy2016-09-181-0/+92
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-4/+4
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-618/+618
* Tweaks to support defunctorization.xleroy2014-07-231-9/+19
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ove...xleroy2014-04-091-0/+10
* Merge of branch value-analysis.xleroy2013-12-201-0/+13
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+28
* Add another expansion of shrx in terms of shifts and adds (from Hacker's Deli...xleroy2013-07-281-42/+72
* More properties about subtraction and borrow.xleroy2013-07-151-18/+59
* More accurate model of condition register flags for ARM and IA32.xleroy2013-07-131-8/+119
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-35/+59
* Decomposing 64-bit "less than" comparisons.xleroy2013-04-291-9/+70
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-34/+430
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-2/+2
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-091-0/+4
* Forgot theorem "sign_ext_narrow".xleroy2013-02-121-0/+12
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-101-1285/+1593
* Some more properties. Refactored some proofs.xleroy2013-02-041-21/+107
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-5/+5
* Integers: specialized function to compute x mod 2^N; used in "repr" toxleroy2012-12-211-114/+177
* Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.xleroy2012-07-091-0/+46
* Changelog: updatedxleroy2012-06-281-0/+40
* More properties on mul/div/modxleroy2012-06-091-0/+39
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-231-0/+50
generated by cgit (git 2.34.1) at 2024-06-02 19:45:20 +0000