aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/Op.v
Commit message (Expand)AuthorAgeFilesLines
* update op_valid_pointer_eq proof on the KVXSylvain Boulmé2020-10-171-22/+4
* Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-09-291-244/+240
|\
| * simpl -> cbnDavid Monniaux2020-09-291-244/+240
* | Characterizing Op dependency on memorySylvain Boulmé2020-07-081-0/+39
|/
* k1c -> kvx changesDavid Monniaux2020-05-261-0/+1975