diff --git a/src/ecMatching.ml b/src/ecMatching.ml
index 73e8b3aa5d..85ce3270cb 100644
--- a/src/ecMatching.ml
+++ b/src/ecMatching.ml
@@ -34,9 +34,12 @@ module Position = struct
   type codepos    = (codepos1 * int) list * codepos1
   type codeoffset1 = [`ByOffset of int | `ByPosition of codepos1]
 
-  let shift ~(offset : int) ((o, p) : codepos1) : codepos1 =
+  let shift1 ~(offset : int) ((o, p) : codepos1) : codepos1 =
     (o + offset, p)
 
+  let shift ~(offset : int) ((outp, p) : codepos) : codepos =
+    (outp, shift1 ~offset p)
+
   let resolve_offset ~(base : codepos1) ~(offset : codeoffset1) : codepos1 =
     match offset with
     | `ByPosition pos -> pos
diff --git a/src/ecMatching.mli b/src/ecMatching.mli
index 7c7db1734c..651fb934e4 100644
--- a/src/ecMatching.mli
+++ b/src/ecMatching.mli
@@ -30,7 +30,9 @@ module Position : sig
   type codepos     = (codepos1 * int) list * codepos1
   type codeoffset1 = [`ByOffset of int | `ByPosition of codepos1]
 
-  val shift : offset:int -> codepos1 -> codepos1
+  val shift1 : offset:int -> codepos1 -> codepos1
+  val shift  : offset:int -> codepos  -> codepos
+
   val resolve_offset : base:codepos1 -> offset:codeoffset1 -> codepos1
 end
 
diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml
index 34ddfa0ead..f617b172cd 100644
--- a/src/phl/ecPhlLoopTx.ml
+++ b/src/phl/ecPhlLoopTx.ml
@@ -317,7 +317,14 @@ let process_unroll_for side cpos tc =
         [t_apply_hd h'; t_conseq_nm] ] tc
   in
 
-  let tcenv = t_doit 0 pos zs tc in FApi.t_onalli doi tcenv
+  let tcenv = t_doit 0 pos zs tc in
+  let tcenv = FApi.t_onalli doi tcenv in
+
+  let cpos = EcMatching.Position.shift ~offset:(-1) cpos in
+  let clen = blen * (List.length zs - 1) in
+
+  Format.eprintf "[W]%d %d@." blen (List.length zs);
+  FApi.t_last (EcPhlCodeTx.t_cfold side cpos (Some clen)) tcenv
 
 (* -------------------------------------------------------------------- *)
 let process_unroll (side, cpos, for_) tc =
diff --git a/tests/cfold.ec b/tests/cfold.ec
index f89259b5c7..f0edc8a5a3 100644
--- a/tests/cfold.ec
+++ b/tests/cfold.ec
@@ -108,7 +108,6 @@ theory CfoldWhileUnroll.
   proc.
   cfold 1.
   unroll for 2.
-  cfold 1.
   by auto => />.
   qed.
 end CfoldWhileUnroll.