aboutsummaryrefslogtreecommitdiffstats
path: root/x86/Op.v
Commit message (Expand)AuthorAgeFilesLines
* Add op for float max and min for x86.Bernhard Schommer2022-02-071-0/+36
* Implement a `Osel` operation for x86Xavier Leroy2019-05-201-9/+36
* In "symbol + ofs" addressing modes, limit the range of "ofs" in 64 bitsXavier Leroy2018-02-121-5/+21
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-0/+21
* Issues with invalid x86 addressing modes (Github issue #183)Xavier Leroy2017-05-171-14/+19
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-9/+9
* Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.vXavier Leroy2016-12-261-8/+8
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-0/+1452