diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 22:26:06 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 22:26:06 +0200 |
| commit | 487fc42595bb43450f2b0b5a49b4edbc22892b9f (patch) | |
| tree | eb671c210dd1e09651003c4f0add4cca118519a2 /mppa_k1c/Machregs.v | |
| parent | 677771949bd62f7f5bbcf99bba6b6f816f07a6c2 (diff) | |
| download | compcert-kvx-487fc42595bb43450f2b0b5a49b4edbc22892b9f.tar.gz compcert-kvx-487fc42595bb43450f2b0b5a49b4edbc22892b9f.zip | |
rm old select/selectl/selectf/selectfs
Diffstat (limited to 'mppa_k1c/Machregs.v')
| -rw-r--r-- | mppa_k1c/Machregs.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index db3dfe64..4e8eedda 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -216,7 +216,6 @@ Definition two_address_op (op: operation) : bool := | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Omsub | Omsubl - | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ | Oinsf _ _ | Oinsfl _ _ => true | _ => false end. |