diff options
Diffstat (limited to 'mppa_k1c/Machregs.v')
| -rw-r--r-- | mppa_k1c/Machregs.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index ed582c98..bed3c040 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -208,11 +208,11 @@ Global Opaque integers as their 64-bit sign extension; and [Ocast32unsigned], because it builds on the same magic no-op. *) -Definition two_address_op (op: operation) : bool := false. - (* match op with - | Ocast32signed | Ocast32unsigned => true +Definition two_address_op (op: operation) : bool := + match op with + | Ocast32unsigned => true | _ => false - end. *) + end. (** Constraints on constant propagation for builtins *) |