diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 286ea584cc95f7c21832b6fcea3cdb71398ee660..754a49bdc27c72fd6c9afe40eec85b765113e89f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -33,6 +33,7 @@ build-coq.8.17.0:
   variables:
     OPAM_PINS: "coq version 8.17.0"
     DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
   tags:
   - fp-timing
 
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index 4df0f9c53206a57173a62d7a37c74b1ba73a5b96..dc60165b24657a89a3f83f96ee438b6caaba645a 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -32,7 +32,6 @@ Proof.
   - destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || lia).
     revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !own_loc_na_vec_cons. subst n.
     iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
-    Local Opaque Zminus.
     wp_read; wp_write. do 3 wp_op. iApply ("IH" with "[%] [%] Hl1 Hl2"); [lia..|].
     iIntros "!> [Hl1 Hl2]"; iApply "HΦ"; by iFrame.
 Qed.