diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-02-12 13:32:23 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-02-12 14:38:59 +0100 |
| commit | d2c5701fb538ec175b3fa2266d795ba63d795b3b (patch) | |
| tree | 12e1b0b2aa0929f5bec4f8d8d2e0e8f90c10ed7a /x86 | |
| parent | 26a4436b9d1b6916d67ee35d00a7120603a3bc9c (diff) | |
| download | compcert-kvx-d2c5701fb538ec175b3fa2266d795ba63d795b3b.tar.gz compcert-kvx-d2c5701fb538ec175b3fa2266d795ba63d795b3b.zip | |
Switching the cases seems to work on x86_32
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/Asmgenproof1.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v index 86a5218a..c5b03426 100644 --- a/x86/Asmgenproof1.v +++ b/x86/Asmgenproof1.v @@ -498,8 +498,8 @@ Proof. intros; destruct am as [base ofs [n|[id delta]]]; simpl. - destruct (offset_in_range n); auto; simpl. rewrite ! Val.addl_assoc. apply f_equal. apply f_equal. simpl. rewrite Int64.add_zero_l; auto. -- destruct (ptroffset_in_range delta); auto. - destruct Archi.ptr64 eqn:SF; auto; simpl. +- destruct Archi.ptr64 eqn:SF; auto; simpl; + destruct (ptroffset_in_range delta); auto. simpl. rewrite ! Val.addl_assoc. apply f_equal. apply f_equal. rewrite <- Genv.shift_symbol_address_64 by auto. f_equal. rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto. |