diff options
Diffstat (limited to 'powerpc/macosx/Stacklayout.v')
| -rw-r--r-- | powerpc/macosx/Stacklayout.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/macosx/Stacklayout.v b/powerpc/macosx/Stacklayout.v index 0e9be224..c57f3f92 100644 --- a/powerpc/macosx/Stacklayout.v +++ b/powerpc/macosx/Stacklayout.v @@ -42,7 +42,7 @@ the boundaries between areas in the frame part. Definition fe_ofs_arg := 24. -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; |