diff options
Diffstat (limited to 'ia32/Asmgenproof1.v')
| -rw-r--r-- | ia32/Asmgenproof1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 00b706c..0bf030c 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -550,7 +550,7 @@ Proof. simpl. fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *. fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *. - destruct (zeq b0 b1). + destruct (eq_block b0 b1). destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i) && Mem.weak_valid_pointer m b1 (Int.unsigned i0)); inversion H1. destruct c; simpl; auto. |