diff options
Diffstat (limited to 'powerpc/Stacklayout.v')
| -rw-r--r-- | powerpc/Stacklayout.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/Stacklayout.v b/powerpc/Stacklayout.v index 2b78fd11..17104b33 100644 --- a/powerpc/Stacklayout.v +++ b/powerpc/Stacklayout.v @@ -93,7 +93,7 @@ Local Opaque Z.add Z.mul sepconj range. apply range_drop_right with 8. omega. apply range_split. omega. apply range_split_2. fold ol; omega. omega. - apply range_split. omega. + apply range_split. omega. apply range_split. omega. apply range_drop_right with ostkdata. omega. eapply sep_drop2. eexact H. |