aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/ConstpropOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-1/+1
|\
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
* | maketotal mod & divDavid Monniaux2020-09-211-40/+112
|/
* Improve strength reduction of unsigned comparisons x ==u 0, x !=u 0, etc (#59)Xavier Leroy2018-02-161-9/+31
* Optimization for division by one during constant propagation (#39)Michael Schmidt2017-12-051-0/+8
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+715