aboutsummaryrefslogtreecommitdiffstats
path: root/x86/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-5/+5
* Implement a `Osel` operation for x86Xavier Leroy2019-05-201-2/+13
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-011-2/+2
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-4/+4
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-0/+916