From d2c5701fb538ec175b3fa2266d795ba63d795b3b Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 12 Feb 2018 13:32:23 +0100 Subject: Switching the cases seems to work on x86_32 --- x86/Asmgenproof1.v | 4 ++-- 1 file 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. -- cgit