diff options
Diffstat (limited to 'powerpc/eabi/Stacklayout.v')
-rw-r--r-- | powerpc/eabi/Stacklayout.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/eabi/Stacklayout.v b/powerpc/eabi/Stacklayout.v index 48e26a76..0de1ccd6 100644 --- a/powerpc/eabi/Stacklayout.v +++ b/powerpc/eabi/Stacklayout.v @@ -45,7 +45,7 @@ the boundaries between areas in the frame part. Definition fe_ofs_arg := 8. -Record frame_env : Set := mk_frame_env { +Record frame_env : Type := mk_frame_env { fe_size: Z; fe_ofs_link: Z; fe_ofs_retaddr: Z; |