Commit d2c5701f authored by Bernhard Schommer's avatar Bernhard Schommer Committed by Xavier Leroy
Browse files

Switching the cases seems to work on x86_32

parent 26a4436b
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment