diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-29 14:32:06 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-29 14:32:06 +0200 |
| commit | 138f4fb80d3dc6cce396dc57e64c28dc949ab94a (patch) | |
| tree | dbd40874c6ca5b74b1063b3140193ce3c3473b1d /mppa_k1c/Asmblockdeps.v | |
| parent | 9dadf82c52a9ad11b31b21986bc88a108b845d0b (diff) | |
| download | compcert-kvx-138f4fb80d3dc6cce396dc57e64c28dc949ab94a.tar.gz compcert-kvx-138f4fb80d3dc6cce396dc57e64c28dc949ab94a.zip | |
removed fake ops for int32 -> double
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index ff625bdd..2e83fb44 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1237,9 +1237,7 @@ Definition string_of_name_rr (n: arith_name_rr): pstring := | Pfloatwrnsz => "Pfloatwrnsz" | Pfloatuwrnsz => "Pfloatuwrnsz" | Pfloatudrnsz => "Pfloatudrnsz" - | Pfloatudrnsz_i32 => "Pfloatudrnsz_i32" | Pfloatdrnsz => "Pfloatdrnsz" - | Pfloatdrnsz_i32 => "Pfloatdrnsz_i32" | Pfixedwrzz => "Pfixedwrzz" | Pfixeduwrzz => "Pfixeduwrzz" | Pfixeddrzz => "Pfixeddrzz" |