diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-26 11:39:16 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-26 11:39:16 +0100 |
| commit | 0e439055e450d63ace2366653cd558de1a073bed (patch) | |
| tree | 232c947434da9c6a372af487e47ce21c4f552656 /aarch64/Asm.v | |
| parent | 02a86fb0cd2dcb63b8346c48ca78056b30c7fef6 (diff) | |
| download | compcert-kvx-0e439055e450d63ace2366653cd558de1a073bed.tar.gz compcert-kvx-0e439055e450d63ace2366653cd558de1a073bed.zip | |
Fine tuning for Pfmovimm
- Functions to check a float logical immediate were translated from ocaml target printer in coq Asmblock
- Some proof are admitted for now (we'll see if it is a good idea after some tests)
Diffstat (limited to 'aarch64/Asm.v')
0 files changed, 0 insertions, 0 deletions