aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Zbits.v
Commit message (Expand)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-133/+133
* Simplify two scripts in Zbits (#369)Maxime Dénès2020-09-181-2/+2
* More lemmas about powers of 2Xavier Leroy2019-08-071-0/+14
* Define integer sign extension for zero bitsXavier Leroy2019-08-071-28/+30
* Zbits.v: add bit extraction and bit insertionXavier Leroy2019-08-071-0/+57
* More efficient test for powers of twoXavier Leroy2019-05-091-0/+83
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-0/+945