diff options
Diffstat (limited to 'mips/mips_extras.lem')
| -rw-r--r-- | mips/mips_extras.lem | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem index 2e07586c..86e78586 100644 --- a/mips/mips_extras.lem +++ b/mips/mips_extras.lem @@ -90,7 +90,6 @@ let shift_bits_right_arith v n = maybe_fail "shift_bits_right_arith" r (* Use constants for undefined values for now *) -let internal_pick vs = return (head vs) let undefined_string () = return "" let undefined_unit () = return () let undefined_int () = return (0:ii) |