aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asmgenproof1.v
Commit message (Expand)AuthorAgeFilesLines
* Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-221-2/+2
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-1/+1
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-10/+10
* Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-4/+4
* AArch64 portXavier Leroy2019-08-081-16/+0
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-8/+8
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+1411