1 files changed, 1 insertions, 1 deletions
diff --git a/x86/Op.v b/x86/Op.v
index 136c900b..02b04574 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -1311,7 +1311,7 @@ Remark weak_valid_pointer_no_overflow_extends:
   Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
   0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
 Proof.
-  intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2.
+  intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2.
 Qed.
 
 Remark valid_different_pointers_extends: