aboutsummaryrefslogtreecommitdiffstats
path: root/x86/CombineOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-201-0/+1
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-2/+2
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-0/+179