diff options
Diffstat (limited to 'riscV/Machregs.v')
| -rw-r--r-- | riscV/Machregs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/Machregs.v b/riscV/Machregs.v index c7d558ed..c21ea97a 100644 --- a/riscV/Machregs.v +++ b/riscV/Machregs.v @@ -151,7 +151,7 @@ Definition register_names := ("F16", F16) :: ("F17", F17) :: ("F18", F18) :: ("F19", F19) :: ("F20", F20) :: ("F21", F21) :: ("F22", F22) :: ("F23", F23) :: ("F24", F24) :: ("F25", F25) :: ("F26", F26) :: ("F27", F27) :: - ("F27", F27) :: ("F28", F28) :: ("F29", F29) :: ("F30", F30) :: + ("F28", F28) :: ("F29", F29) :: ("F30", F30) :: ("F31", F31) :: nil. Definition register_by_name (s: string) : option mreg := |