aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Introduce and use the type fp_comparison for floating-point comparisonsXavier Leroy2019-03-261-12/+0
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-011-2/+2
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+1028