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