diff --git a/src/ecCorePrinting.ml b/src/ecCorePrinting.ml
index 0ac541b84..8d9a2aa07 100644
--- a/src/ecCorePrinting.ml
+++ b/src/ecCorePrinting.ml
@@ -24,7 +24,7 @@ module type PrinterAPI = sig
 
   (* ------------------------------------------------------------------ *)
   val string_of_hcmp : EcFol.hoarecmp -> string
-  val string_of_cpos1 : EcParsetree.codepos1 -> string
+  val string_of_cpos1 : EcMatching.Position.codepos1 -> string
 
   (* ------------------------------------------------------------------ *)
   type 'a pp = Format.formatter -> 'a -> unit
diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml
index 32f6ea2ed..2b9d8ec4a 100644
--- a/src/ecHiTacticals.ml
+++ b/src/ecHiTacticals.ml
@@ -174,9 +174,9 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pskip                     -> EcPhlSkip.t_skip
     | Papp info                 -> EcPhlApp.process_app info
     | Pwp wp                    -> EcPhlWp.process_wp wp
-    | Psp sp                    -> EcPhlSp.t_sp sp
+    | Psp sp                    -> EcPhlSp.process_sp sp
     | Prcond (side, b, i)       -> EcPhlRCond.process_rcond side b i
-    | Prmatch (side, c, i)      -> EcPhlRCond.t_rcond_match side c i
+    | Prmatch (side, c, i)      -> EcPhlRCond.process_rcond_match side c i
     | Pcond info                -> EcPhlHiCond.process_cond info
     | Pmatch infos              -> EcPhlHiCond.process_match infos
     | Pwhile (side, info)       -> EcPhlWhile.process_while side info
diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml
index 4164530fe..683dd5e18 100644
--- a/src/ecLowPhlGoal.ml
+++ b/src/ecLowPhlGoal.ml
@@ -9,6 +9,7 @@ open EcFol
 open EcEnv
 open EcPV
 open EcCoreGoal
+open EcMatching.Position
 
 module Zpr = EcMatching.Zipper
 
@@ -266,19 +267,19 @@ let set_pre ~pre f =
 (* -------------------------------------------------------------------- *)
 exception InvalidSplit of codepos1
 
-let s_split i s =
+let s_split env i s =
   let module Zpr = EcMatching.Zipper in
-  try  Zpr.split_at_cpos1 i s
+  try  Zpr.split_at_cpos1 env i s
   with Zpr.InvalidCPos -> raise (InvalidSplit i)
 
-let s_split_i i s =
+let s_split_i env i s =
   let module Zpr = EcMatching.Zipper in
-  try  Zpr.find_by_cpos1 ~rev:false i s
+  try  Zpr.find_by_cpos1 ~rev:false env i s
   with Zpr.InvalidCPos -> raise (InvalidSplit i)
 
-let o_split ?rev i s =
+let o_split ?rev env i s =
   let module Zpr = EcMatching.Zipper in
-  try  Zpr.may_split_at_cpos1 ?rev i s
+  try  Zpr.may_split_at_cpos1 ?rev env i s
   with Zpr.InvalidCPos -> raise (InvalidSplit (oget i))
 
 (* -------------------------------------------------------------------- *)
@@ -576,13 +577,15 @@ type 'a zip_t =
 
 let t_fold f (cenv : code_txenv) (cpos : codepos) (_ : form * form) (state, s) =
   try
-    let (me, f) = Zpr.fold cenv cpos f state s in
+    let env = EcEnv.LDecl.toenv (snd cenv) in
+    let (me, f) = Zpr.fold env cenv cpos f state s in
       ((me, f, []) : memenv * _ * form list)
   with Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"
 
 let t_zip f (cenv : code_txenv) (cpos : codepos) (prpo : form * form) (state, s) =
   try
-    let (me, zpr, gs) = f cenv prpo state (Zpr.zipper_of_cpos cpos s) in
+    let env = EcEnv.LDecl.toenv (snd cenv) in
+    let (me, zpr, gs) = f cenv prpo state (Zpr.zipper_of_cpos env cpos s) in
       ((me, Zpr.zip zpr, gs) : memenv * _ * form list)
   with Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"
 
diff --git a/src/ecMatching.ml b/src/ecMatching.ml
index a2c288115..d471259f7 100644
--- a/src/ecMatching.ml
+++ b/src/ecMatching.ml
@@ -6,7 +6,6 @@
 open EcUtils
 open EcMaps
 open EcIdent
-open EcParsetree
 open EcEnv
 open EcAst
 open EcTypes
@@ -14,8 +13,31 @@ open EcModules
 open EcFol
 open EcGenRegexp
 
+(* -------------------------------------------------------------------- *)
+module Position = struct
+  type cp_match = [
+    | `If
+    | `While
+    | `Assign of lvmatch
+    | `Sample
+    | `Call
+  ]
+
+  and lvmatch = [ `LvmNone | `LvmVar of EcTypes.prog_var ]
+
+  type cp_base = [
+    | `ByPos of int
+    | `ByMatch of int option * cp_match
+  ]
+
+  type codepos1   = int * cp_base
+  type codepos    = (codepos1 * int) list * codepos1
+end
+
 (* -------------------------------------------------------------------- *)
 module Zipper = struct
+  open Position
+
   exception InvalidCPos
 
   module P = EcPath
@@ -41,7 +63,11 @@ module Zipper = struct
 
   let zipper hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; }
 
-  let find_by_cp_match ((i, cm) : int option * cp_match) (s : stmt) =
+  let find_by_cp_match
+    (env     : EcEnv.env)
+    ((i, cm) : int option * cp_match)
+    (s       : stmt)
+  =
     let rec progress (acc : instr list) (s : instr list) (i : int) =
       if i <= 0 then
         let shd = oget (List.Exceptionless.hd acc) in
@@ -57,10 +83,19 @@ module Zipper = struct
         match ir.i_node, cm with
         | Swhile _, `While  -> i-1
         | Sif    _, `If     -> i-1
-        | Sasgn  _, `Assign -> i-1
         | Srnd   _, `Sample -> i-1
         | Scall  _, `Call   -> i-1
-        | _       , _       -> i
+
+        | Sasgn  (lv, _), `Assign lvm -> begin
+            match lv, lvm with
+            | _, `LvmNone -> i-1
+            | LvVar (pv, _), `LvmVar pvm
+                 when EcReduction.EqTest.for_pv env pv pvm
+              -> i-1
+            | _ -> i
+          end
+
+        | _ -> i
 
       in progress (ir :: acc) s i
 
@@ -76,7 +111,7 @@ module Zipper = struct
     | false -> (s1, ir, s2)
     | true  -> (s2, ir, s1)
 
-  let split_at_cp_base ~after (cb : cp_base) (s : stmt) =
+  let split_at_cp_base ~after (env : EcEnv.env) (cb : cp_base) (s : stmt) =
     match cb with
     | `ByPos i -> begin
         let i = if i < 0 then List.length s.s_node + i else i in
@@ -85,14 +120,14 @@ module Zipper = struct
       end
 
     | `ByMatch (i, cm) ->
-        let (s1, i, s2) = find_by_cp_match (i, cm) s in
+        let (s1, i, s2) = find_by_cp_match env (i, cm) s in
 
         match after with
         | false -> (List.rev s1, i :: s2)
         | true  -> (List.rev_append s1 [i], s2)
 
-  let split_at_cpos1 ~after ((ipos, cb) : codepos1) s =
-    let (s1, s2) = split_at_cp_base ~after cb s in
+  let split_at_cpos1 ~after (env : EcEnv.env) ((ipos, cb) : codepos1) s =
+    let (s1, s2) = split_at_cp_base ~after env cb s in
 
     let (s1, s2) =
       match ipos with
@@ -112,13 +147,13 @@ module Zipper = struct
 
     in (s1, s2)
 
-  let find_by_cpos1 ?(rev = true) (cpos1 : codepos1) s =
-    match split_at_cpos1 ~after:false cpos1 s with
+  let find_by_cpos1 ?(rev = true) (env : EcEnv.env) (cpos1 : codepos1) s =
+    match split_at_cpos1 ~after:false env cpos1 s with
     | (s1, i :: s2) -> ((if rev then List.rev s1 else s1), i, s2)
     | _ -> raise InvalidCPos
 
-  let zipper_at_nm_cpos1 ((cp1, sub) : codepos1 * int) s zpr =
-    let (s1, i, s2) = find_by_cpos1 cp1 s in
+  let zipper_at_nm_cpos1 (env : EcEnv.env) ((cp1, sub) : codepos1 * int) s zpr =
+    let (s1, i, s2) = find_by_cpos1 env cp1 s in
 
     match i.i_node, sub with
     | Swhile (e, sw), 0 ->
@@ -132,23 +167,23 @@ module Zipper = struct
 
     | _ -> raise InvalidCPos
 
-  let zipper_of_cpos ((nm, cp1) : codepos) s =
+  let zipper_of_cpos (env : EcEnv.env) ((nm, cp1) : codepos) s =
     let zpr, s =
       List.fold_left
-        (fun (zpr, s) nm1 -> zipper_at_nm_cpos1 nm1 s zpr)
+        (fun (zpr, s) nm1 -> zipper_at_nm_cpos1 env nm1 s zpr)
         (ZTop, s) nm in
 
-    let s1, i, s2 = find_by_cpos1 cp1 s in
+    let s1, i, s2 = find_by_cpos1 env cp1 s in
 
     zipper s1 (i :: s2) zpr
 
-  let split_at_cpos1 cpos1 s =
-    split_at_cpos1 ~after:true cpos1 s
+  let split_at_cpos1 env cpos1 s =
+    split_at_cpos1 ~after:true env cpos1 s
 
-  let may_split_at_cpos1 ?(rev = false) cpos1 s =
+  let may_split_at_cpos1 ?(rev = false) env cpos1 s =
     ofdfl
       (fun () -> if rev then (s.s_node, []) else ([], s.s_node))
-      (omap (split_at_cpos1^~ s) cpos1)
+      (omap ((split_at_cpos1 env)^~ s) cpos1)
 
   let rec zip i ((hd, tl), ip) =
     let s = stmt (List.rev_append hd (List.ocons i tl)) in
@@ -178,21 +213,21 @@ module Zipper = struct
     in
       List.rev after
 
-  let fold env cpos f state s =
-    let zpr = zipper_of_cpos cpos s in
+  let fold env cenv cpos f state s =
+    let zpr = zipper_of_cpos env cpos s in
 
       match zpr.z_tail with
       | []      -> raise InvalidCPos
       | i :: tl -> begin
-          match f env state i with
+          match f cenv state i with
           | (state', [i']) when i == i' && state == state' -> (state, s)
           | (state', si  ) -> (state', zip { zpr with z_tail = si @ tl })
       end
 
-  let map cpos f s =
+  let map env cpos f s =
     fst_map
       Option.get
-      (fold () cpos (fun () _ i -> fst_map some (f i)) None s)
+      (fold env () cpos (fun () _ i -> fst_map some (f i)) None s)
 end
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/ecMatching.mli b/src/ecMatching.mli
index 40a4213f8..3ad222073 100644
--- a/src/ecMatching.mli
+++ b/src/ecMatching.mli
@@ -1,7 +1,6 @@
 (* -------------------------------------------------------------------- *)
 open EcMaps
 open EcUid
-open EcParsetree
 open EcIdent
 open EcTypes
 open EcModules
@@ -10,8 +9,31 @@ open EcUnify
 open EcEnv
 open EcGenRegexp
 
+(* -------------------------------------------------------------------- *)
+module Position : sig
+  type cp_match = [
+    | `If
+    | `While
+    | `Assign of lvmatch
+    | `Sample
+    | `Call
+  ]
+
+  and lvmatch = [ `LvmNone | `LvmVar of EcTypes.prog_var ]
+
+  type cp_base = [
+    | `ByPos of int
+    | `ByMatch of int option * cp_match
+  ]
+
+  type codepos1   = int * cp_base
+  type codepos    = (codepos1 * int) list * codepos1
+end
+
 (* -------------------------------------------------------------------- *)
 module Zipper : sig
+  open Position
+
   type ipath =
   | ZTop
   | ZWhile  of expr * spath
@@ -32,18 +54,18 @@ module Zipper : sig
   val cpos : int -> codepos1
 
   (* Split a statement from a top-level position (codepos1) *)
-  val find_by_cpos1  : ?rev:bool -> codepos1 -> stmt -> instr list * instr * instr list
-  val split_at_cpos1 : codepos1 -> stmt -> instr list * instr list
+  val find_by_cpos1  : ?rev:bool -> env -> codepos1 -> stmt -> instr list * instr * instr list
+  val split_at_cpos1 : env -> codepos1 -> stmt -> instr list * instr list
 
   (* Split a statement from an optional top-level position (codepos1) *)
-  val may_split_at_cpos1 : ?rev:bool -> codepos1 option -> stmt -> instr list * instr list
+  val may_split_at_cpos1 : ?rev:bool -> env -> codepos1 option -> stmt -> instr list * instr list
 
   (* [zipper] soft constructor *)
   val zipper : instr list -> instr list -> ipath -> zipper
 
   (* Return the zipper for the stmt [stmt] at code position [codepos].
    * Raise [InvalidCPos] if [codepos] is not valid for [stmt]. *)
-  val zipper_of_cpos : codepos -> stmt -> zipper
+  val zipper_of_cpos : env -> codepos -> stmt -> zipper
 
   (* Zip the zipper, returning the corresponding statement *)
   val zip : zipper -> stmt
@@ -58,19 +80,19 @@ module Zipper : sig
 
   type ('a, 'state) folder = 'a -> 'state -> instr -> 'state * instr list
 
-  (* [fold v cpos f state s] create the zipper for [s] at [cpos], and apply
+  (* [fold env v cpos f state s] create the zipper for [s] at [cpos], and apply
    * [f] to it, along with [v] and the state [state]. [f] must return the
    * new [state] and a new [zipper]. These last are directly returned.
    *
    * Raise [InvalidCPos] if [cpos] is not valid for [s], or any exception
    * raised by [f].
    *)
-  val fold : 'a -> codepos -> ('a, 'state) folder -> 'state -> stmt -> 'state * stmt
+  val fold : env -> 'a -> codepos -> ('a, 'state) folder -> 'state -> stmt -> 'state * stmt
 
-  (* [map cpos f s] is a special case of [fold] where the state and the
+  (* [map cpos env f s] is a special case of [fold] where the state and the
    * out-of-band data are absent
    *)
-  val map : codepos -> (instr -> 'a * instr list) -> stmt -> 'a * stmt
+  val map : env -> codepos -> (instr -> 'a * instr list) -> stmt -> 'a * stmt
 
 end
 
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 4908cd313..ed3eb5f7d 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -1434,19 +1434,21 @@ param_decl:
 (* -------------------------------------------------------------------- *)
 (* Statements                                                           *)
 
-lvalue_u:
+lvalue_var:
 | x=loc(fident)
    { match lqident_of_fident x.pl_desc with
      | None   -> parse_error x.pl_loc None
-     | Some v -> PLvSymbol (mk_loc x.pl_loc v) }
+     | Some v -> mk_loc x.pl_loc v }
+
+lvalue_u:
+| x=lvalue_var
+   { PLvSymbol x }
 
 | LPAREN p=plist2(qident, COMMA) RPAREN
    { PLvTuple p }
 
-| x=loc(fident) DLBRACKET ti=tvars_app? es=plist1(expr, COMMA) RBRACKET
-   { match lqident_of_fident x.pl_desc with
-     | None   -> parse_error x.pl_loc None
-     | Some v -> PLvMap (mk_loc x.pl_loc v, ti, es) }
+| x=lvalue_var DLBRACKET ti=tvars_app? e=plist1(expr, COMMA) RBRACKET
+   { PLvMap (x, ti, e) }
 
 %inline lvalue:
 | x=loc(lvalue_u) { x }
@@ -2602,21 +2604,26 @@ tac_dir:
 | empty { Backs }
 
 icodepos_r:
-| IF       { (`If     :> cp_match) }
-| WHILE    { (`While  :> cp_match) }
-| LARROW   { (`Assign :> cp_match) }
-| LESAMPLE { (`Sample :> cp_match) }
-| LEAT     { (`Call   :> cp_match) }
+| IF       { (`If     :> pcp_match) }
+| WHILE    { (`While  :> pcp_match) }
+| LESAMPLE { (`Sample :> pcp_match) }
+| LEAT     { (`Call   :> pcp_match) }
+
+| lvm=lvmatch LARROW { (`Assign lvm :> pcp_match) }
+
+lvmatch:
+| empty        { (`LvmNone  :> plvmatch) }
+| x=lvalue_var { (`LvmVar x :> plvmatch) }
 
 %inline icodepos:
  | HAT x=icodepos_r { x }
 
 codepos1_wo_off:
 | i=sword
-    { (`ByPos i :> cp_base) }
+    { (`ByPos i :> pcp_base) }
 
 | k=icodepos i=option(brace(sword))
-    { (`ByMatch (i, k) :> cp_base) }
+    { (`ByMatch (i, k) :> pcp_base) }
 
 codepos1:
 | cp=codepos1_wo_off { (0, cp) }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 7f2fb45ac..2bf321008 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -487,12 +487,21 @@ type preduction = {
 }
 
 (* -------------------------------------------------------------------- *)
-type cp_match = [ `If | `While | `Assign | `Sample | `Call ]
-type cp_base  = [ `ByPos of int | `ByMatch of int option * cp_match ]
+type pcp_match = [
+  | `If
+  | `While
+  | `Assign of plvmatch
+  | `Sample
+  | `Call
+]
+
+and plvmatch = [ `LvmNone | `LvmVar of pqsymbol ]
+
+type pcp_base  = [ `ByPos of int | `ByMatch of int option * pcp_match ]
 
-type codepos1 = int * cp_base
-type codepos  = (codepos1 * int) list * codepos1
-type docodepos1 = codepos1 doption option
+type pcodepos1 = int * pcp_base
+type pcodepos  = (pcodepos1 * int) list * pcodepos1
+type pdocodepos1 = pcodepos1 doption option
 
 (* -------------------------------------------------------------------- *)
 type swap_kind =
@@ -530,7 +539,7 @@ type ('a, 'b, 'c) rnd_tac_info =
 type rnd_tac_info_f =
   (pformula, pformula option, pformula) rnd_tac_info
 
-type semrndpos = (bool * codepos1) doption
+type psemrndpos = (bool * pcodepos1) doption
 
 type tac_dir = Backs | Fwds
 
@@ -597,13 +606,13 @@ type fun_info = [
 
 (* -------------------------------------------------------------------- *)
 type app_info =
-  oside * tac_dir * codepos1 doption * pformula doption * p_app_xt_info
+  oside * tac_dir * pcodepos1 doption * pformula doption * p_app_xt_info
 
 (* -------------------------------------------------------------------- *)
 type pcond_info = [
   | `Head   of oside
-  | `Seq    of oside * codepos1 option pair * pformula
-  | `SeqOne of  side * codepos1 option * pformula * pformula
+  | `Seq    of oside * pcodepos1 option pair * pformula
+  | `SeqOne of  side * pcodepos1 option * pformula * pformula
 ]
 
 (* -------------------------------------------------------------------- *)
@@ -634,7 +643,7 @@ type inline_pat = ([ `DIFF | `UNION] * inline_pat1) list
 
 type inline_info = [
   | `ByName    of oside * inlineopt * (inline_pat * int list option)
-  | `CodePos   of (oside * inlineopt * codepos)
+  | `CodePos   of (oside * inlineopt * pcodepos)
  (* | `All       of oside * inlineopt *)
 ]
 
@@ -645,8 +654,8 @@ type outline_kind =
 
 type outline_info = {
     outline_side: side;
-    outline_start: codepos1;
-    outline_end: codepos1;
+    outline_start: pcodepos1;
+    outline_end: pcodepos1;
     outline_kind: outline_kind;
 }
 
@@ -670,7 +679,7 @@ type conseq_ppterm = ((pformula option pair) * (conseq_info) option) gppterm
 
 (* -------------------------------------------------------------------- *)
 type sim_info = {
-  sim_pos  : codepos1 pair option;
+  sim_pos  : pcodepos1 pair option;
   sim_hint : (pgamepath option pair * pformula) list * pformula option;
   sim_eqs  : pformula option
 }
@@ -679,7 +688,7 @@ type sim_info = {
 type rw_eqv_info = {
   rw_eqv_side  : side;
   rw_eqv_dir   : [`LtoR | `RtoL];
-  rw_eqv_pos   : codepos1;
+  rw_eqv_pos   : pcodepos1;
   rw_eqv_lemma : ppterm;
   rw_eqv_proc  : (pexpr list located * pexpr option) option;
 }
@@ -706,32 +715,32 @@ type phltactic =
   | Prepl_stmt     of trans_info
   | Pfun           of fun_info
   | Papp           of app_info
-  | Pwp            of docodepos1
-  | Psp            of docodepos1
+  | Pwp            of pdocodepos1
+  | Psp            of pdocodepos1
   | Pwhile         of (oside * while_info)
   | Pasyncwhile    of async_while_info
-  | Pfission       of (oside * codepos * (int * (int * int)))
-  | Pfusion        of (oside * codepos * (int * (int * int)))
-  | Punroll        of (oside * codepos * bool)
-  | Psplitwhile    of (pexpr * oside * codepos)
+  | Pfission       of (oside * pcodepos * (int * (int * int)))
+  | Pfusion        of (oside * pcodepos * (int * (int * int)))
+  | Punroll        of (oside * pcodepos * bool)
+  | Psplitwhile    of (pexpr * oside * pcodepos)
   | Pcall          of oside * call_info gppterm
   | Pcallconcave   of (pformula * call_info gppterm)
-  | Prcond         of (oside * bool * codepos1)
-  | Prmatch        of (oside * symbol * codepos1)
+  | Prcond         of (oside * bool * pcodepos1)
+  | Prmatch        of (oside * symbol * pcodepos1)
   | Pcond          of pcond_info
   | Pmatch         of matchmode
   | Pswap          of ((oside * swap_kind) located list)
-  | Pcfold         of (oside * codepos * int option)
+  | Pcfold         of (oside * pcodepos * int option)
   | Pinline        of inline_info
   | Poutline       of outline_info
   | Pinterleave    of interleave_info located
-  | Pkill          of (oside * codepos * int option)
-  | Pasgncase      of (oside * codepos)
-  | Prnd           of oside * semrndpos option * rnd_tac_info_f
-  | Prndsem        of bool * oside * codepos1
-  | Palias         of (oside * codepos * osymbol_r)
+  | Pkill          of (oside * pcodepos * int option)
+  | Pasgncase      of (oside * pcodepos)
+  | Prnd           of oside * psemrndpos option * rnd_tac_info_f
+  | Prndsem        of bool * oside * pcodepos1
+  | Palias         of (oside * pcodepos * osymbol_r)
   | Pweakmem       of (oside * psymbol * fun_params)
-  | Pset           of (oside * codepos * bool * psymbol * pexpr)
+  | Pset           of (oside * pcodepos * bool * psymbol * pexpr)
   | Pconseq        of (pcqoptions * (conseq_ppterm option tuple3))
   | Pconseqauto    of crushmode
   | Pconcave       of (pformula option tuple2 gppterm * pformula)
@@ -742,7 +751,7 @@ type phltactic =
   | Pbydeno        of ([`PHoare | `Equiv | `EHoare ] * (deno_ppterm * bool * pformula option))
   | PPr            of (pformula * pformula) option
   | Pbyupto
-  | Pfel           of (codepos1 * fel_info)
+  | Pfel           of (pcodepos1 * fel_info)
   | Phoare
   | Pprbounded
   | Psim           of crushmode option* sim_info
@@ -750,11 +759,11 @@ type phltactic =
   | Prw_equiv      of rw_eqv_info
   | Psymmetry
   | Pbdhoare_split of bdh_split
-  | Pprocchange    of side option * codepos * pexpr
-  | Pprocrewrite   of side option * codepos * prrewrite
+  | Pprocchange    of side option * pcodepos * pexpr
+  | Pprocrewrite   of side option * pcodepos * prrewrite
 
     (* Eager *)
-  | Peager_seq       of (eager_info * codepos1 pair * pformula)
+  | Peager_seq       of (eager_info * pcodepos1 pair * pformula)
   | Peager_if
   | Peager_while     of (eager_info)
   | Peager_fun_def
diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml
index 7275e6610..160ee1f61 100644
--- a/src/ecPrinting.ml
+++ b/src/ecPrinting.ml
@@ -1316,7 +1316,7 @@ let pp_locality fmt lc =
   Format.fprintf fmt "%s" (odfl "" (string_of_locality lc))
 
 (* -------------------------------------------------------------------- *)
-let string_of_cpos1 ((off, cp) : EcParsetree.codepos1) =
+let string_of_cpos1 ((off, cp) : EcMatching.Position.codepos1) =
   let s =
     match cp with
     | `ByPos i ->
@@ -1326,11 +1326,11 @@ let string_of_cpos1 ((off, cp) : EcParsetree.codepos1) =
         let s =
           let k =
             match k with
-            | `If     -> "if"
-            | `While  -> "while"
-            | `Assign -> "<-"
-            | `Sample -> "<$"
-            | `Call   -> "<@"
+            | `If       -> "if"
+            | `While    -> "while"
+            | `Assign _ -> "<-"
+            | `Sample   -> "<$"
+            | `Call     -> "<@"
           in Printf.sprintf "^%s" k in
 
         match i with
diff --git a/src/ecProofTyping.ml b/src/ecProofTyping.ml
index 2fe5cf066..eb1cc232a 100644
--- a/src/ecProofTyping.ml
+++ b/src/ecProofTyping.ml
@@ -173,6 +173,19 @@ let tc1_process_Xhl_formula ?side tc pf =
 let tc1_process_Xhl_formula_xreal tc pf =
   tc1_process_Xhl_form tc txreal pf
 
+(* ------------------------------------------------------------------ *)
+let tc1_process_codepos tc (side, cpos) =
+  let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
+  let env = FApi.tc1_env tc in
+  let env = EcEnv.Memory.push_active me env in
+  EcTyping.trans_codepos env cpos
+(* ------------------------------------------------------------------ *)
+let tc1_process_codepos1 tc (side, cpos) =
+  let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
+  let env = FApi.tc1_env tc in
+  let env = EcEnv.Memory.push_active me env in
+  EcTyping.trans_codepos1 env cpos
+  
 (* ------------------------------------------------------------------ *)
 (* FIXME: factor out to typing module                                 *)
 (* FIXME: TC HOOK - check parameter constraints                       *)
diff --git a/src/ecProofTyping.mli b/src/ecProofTyping.mli
index bb9ebc96d..7169f3c8d 100644
--- a/src/ecProofTyping.mli
+++ b/src/ecProofTyping.mli
@@ -8,6 +8,7 @@ open EcModules
 open EcEnv
 open EcCoreGoal
 open EcMemory
+open EcMatching.Position
 
 (* -------------------------------------------------------------------- *)
 type ptnenv = ty Mid.t * EcUnify.unienv
@@ -62,6 +63,9 @@ val tc1_process_stmt :
 val tc1_process_prhl_stmt :
      ?map:EcTyping.ismap -> tcenv1 -> side -> pstmt -> stmt
 
+val tc1_process_codepos : tcenv1 -> oside * pcodepos -> codepos
+val tc1_process_codepos1 : tcenv1 -> oside * pcodepos1 -> codepos1
+
 (* -------------------------------------------------------------------- *)
 exception NoMatch
 
diff --git a/src/ecTyping.ml b/src/ecTyping.ml
index 6493450c3..8c8d0fc09 100644
--- a/src/ecTyping.ml
+++ b/src/ecTyping.ml
@@ -11,6 +11,7 @@ open EcDecl
 open EcMemory
 open EcModules
 open EcFol
+open EcMatching.Position
 
 module MMsym = EcSymbols.MMsym
 module Sid   = EcIdent.Sid
@@ -3440,6 +3441,43 @@ and trans_prop env ?mv ue pf =
 and trans_pattern env ps ue pf =
   trans_form_or_pattern env ~ps ue pf None
 
+(* -------------------------------------------------------------------- *)
+let trans_lv_match ?(memory : memory option) (env : EcEnv.env) (p : plvmatch) : lvmatch =
+  match p with
+  | `LvmNone as p -> (p :> lvmatch)
+  | `LvmVar pv -> begin
+    match memory with
+    | None ->
+      `LvmVar (fst (trans_pv env pv))
+    | Some m ->
+      `LvmVar (transpvar env m pv)
+    end
+(* -------------------------------------------------------------------- *)
+let trans_cp_match ?(memory : memory option) (env : EcEnv.env) (p : pcp_match) : cp_match =
+  match p with
+  | (`Sample | `While | `Call | `If) as p ->
+    (p :> cp_match)
+  | `Assign lv ->
+    `Assign (trans_lv_match ?memory env lv)
+(* -------------------------------------------------------------------- *)
+let trans_cp_base ?(memory : memory option) (env : EcEnv.env) (p : pcp_base) : cp_base =
+  match p with
+  | `ByPos _ as p -> (p :> cp_base)
+  | `ByMatch (i, p) -> `ByMatch (i, trans_cp_match ?memory env p)
+(* -------------------------------------------------------------------- *)
+let trans_codepos1 ?(memory : memory option) (env : EcEnv.env) (p : pcodepos1) : codepos1 =
+  snd_map (trans_cp_base ?memory env) p
+
+(* -------------------------------------------------------------------- *)
+let trans_codepos ?(memory : memory option) (env : EcEnv.env) ((nm, p) : pcodepos) : codepos =
+  let nm = List.map (fst_map (trans_codepos1 ?memory env)) nm in
+  let p = trans_codepos1 ?memory env p in
+  (nm, p)
+
+(* -------------------------------------------------------------------- *)
+let trans_dcodepos1 ?(memory : memory option) (env : EcEnv.env) (p : pcodepos1 doption) : codepos1 doption =
+  DOption.map (trans_codepos1 ?memory env) p
+
 (* -------------------------------------------------------------------- *)
 let get_instances (tvi, bty) env =
   let inst = List.pmap
diff --git a/src/ecTyping.mli b/src/ecTyping.mli
index 116355bae..522269a01 100644
--- a/src/ecTyping.mli
+++ b/src/ecTyping.mli
@@ -10,6 +10,7 @@ open EcParsetree
 open EcTypes
 open EcModules
 open EcFol
+open EcMatching.Position
 
 (* -------------------------------------------------------------------- *)
 type wp = EcEnv.env -> EcMemory.memenv -> stmt -> EcFol.form -> EcFol.form option
@@ -209,16 +210,24 @@ val transexpcast :
 val transexpcast_opt :
   env -> [`InProc|`InOp] -> EcUnify.unienv -> ty option -> pexpr -> expr
 
+(* -------------------------------------------------------------------- *)
+val trans_pv : EcEnv.env -> pqsymbol -> prog_var * ty
+
 (* -------------------------------------------------------------------- *)
 type ismap = (instr list) EcMaps.Mstr.t
 
 val transstmt : ?map:ismap -> env -> EcUnify.unienv -> pstmt -> stmt
 
+(* -------------------------------------------------------------------- *)
+val trans_codepos1 : ?memory:EcMemory.memory -> env -> pcodepos1 -> codepos1
+val trans_codepos : ?memory:EcMemory.memory -> env -> pcodepos -> codepos
+val trans_dcodepos1 : ?memory:EcMemory.memory -> env -> pcodepos1 doption -> codepos1 doption
+
 (* -------------------------------------------------------------------- *)
 type ptnmap = ty EcIdent.Mid.t ref
 type metavs = EcFol.form Msym.t
 
-val transmem       : env -> EcSymbols.symbol located -> EcIdent.t
+val transmem : env -> EcSymbols.symbol located -> EcIdent.t
 
 val trans_form_opt :
   env -> ?mv:metavs -> EcUnify.unienv -> pformula -> ty option -> EcFol.form
@@ -258,7 +267,6 @@ val trans_args :
   -> expr list * EcTypes.ty
 
 (* -------------------------------------------------------------------- *)
-
 (* This only checks the memory restrictions. *)
 val check_mem_restr_fun :
   env -> xpath -> mod_restr -> unit
diff --git a/src/ecUtils.ml b/src/ecUtils.ml
index 2aa8183d5..a5a463c0f 100644
--- a/src/ecUtils.ml
+++ b/src/ecUtils.ml
@@ -278,6 +278,13 @@ type 'a doption =
   | Single of 'a
   | Double of ('a * 'a)
 
+module DOption = struct
+  let map (type a b) (f : a -> b) (x : a doption) : b doption =
+    match x with
+    | Single v -> Single (f v)
+    | Double (v1, v2) -> Double (f v1, f v2)
+end
+
 (* -------------------------------------------------------------------- *)
 type ('a, 'b) tagged = Tagged of ('a * 'b option)
 
diff --git a/src/ecUtils.mli b/src/ecUtils.mli
index acece0189..f2f876e15 100644
--- a/src/ecUtils.mli
+++ b/src/ecUtils.mli
@@ -147,6 +147,10 @@ type 'a doption =
   | Single of 'a
   | Double of ('a * 'a)
 
+module DOption : sig
+  val map : ('a -> 'b) -> 'a doption -> 'b doption
+end
+
 (* -------------------------------------------------------------------- *)
 type ('a, 'b) tagged = Tagged of ('a * 'b option)
 
diff --git a/src/phl/ecPhlApp.ml b/src/phl/ecPhlApp.ml
index 2389db17e..554aa2402 100644
--- a/src/phl/ecPhlApp.ml
+++ b/src/phl/ecPhlApp.ml
@@ -14,8 +14,9 @@ module TTC = EcProofTyping
 
 (* -------------------------------------------------------------------- *)
 let t_hoare_app_r i phi tc =
+  let env = FApi.tc1_env tc in
   let hs = tc1_as_hoareS tc in
-  let s1, s2 = s_split i hs.hs_s in
+  let s1, s2 = s_split env i hs.hs_s in
   let a = f_hoareS_r { hs with hs_s = stmt s1; hs_po = phi }  in
   let b = f_hoareS_r { hs with hs_pr = phi; hs_s = stmt s2 } in
   FApi.xmutate1 tc `HlApp [a; b]
@@ -24,8 +25,9 @@ let t_hoare_app = FApi.t_low2 "hoare-app" t_hoare_app_r
 
 (* -------------------------------------------------------------------- *)
 let t_ehoare_app_r i f tc =
+  let env = FApi.tc1_env tc in
   let hs = tc1_as_ehoareS tc in
-  let s1, s2 = s_split i hs.ehs_s in
+  let s1, s2 = s_split env i hs.ehs_s in
   let a = f_eHoareS_r { hs with ehs_s = stmt s1; ehs_po = f }  in
   let b = f_eHoareS_r { hs with ehs_pr = f; ehs_s = stmt s2 } in
   FApi.xmutate1 tc `HlApp [a; b]
@@ -34,8 +36,9 @@ let t_ehoare_app = FApi.t_low2 "hoare-app" t_ehoare_app_r
 
 (* -------------------------------------------------------------------- *)
 let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc =
+  let env = FApi.tc1_env tc in
   let bhs = tc1_as_bdhoareS tc in
-  let s1, s2 = s_split i bhs.bhs_s in
+  let s1, s2 = s_split env i bhs.bhs_s in
   let s1, s2 = stmt s1, stmt s2 in
   let nR = f_not pR in
   let cond_phi = f_hoareS bhs.bhs_m bhs.bhs_pr s1 phi in
@@ -96,9 +99,10 @@ let t_bdhoare_app = FApi.t_low2 "bdhoare-app" t_bdhoare_app_r
 
 (* -------------------------------------------------------------------- *)
 let t_equiv_app (i, j) phi tc =
+  let env = FApi.tc1_env tc in
   let es = tc1_as_equivS tc in
-  let sl1,sl2 = s_split i es.es_sl in
-  let sr1,sr2 = s_split j es.es_sr in
+  let sl1,sl2 = s_split env i es.es_sl in
+  let sr1,sr2 = s_split env j es.es_sr in
   let a = f_equivS_r {es with es_sl=stmt sl1; es_sr=stmt sr1; es_po=phi} in
   let b = f_equivS_r {es with es_pr=phi; es_sl=stmt sl2; es_sr=stmt sr2} in
 
@@ -116,7 +120,7 @@ let t_equiv_app_onesided side i pre post tc =
     match side with
     | `Left  -> (i, Zpr.cpos (List.length s'. s_node))
     | `Right -> (Zpr.cpos (List.length s'. s_node), i) in
-  let _s1, s2 = s_split i s in
+  let _s1, s2 = s_split env i s in
 
   let modi = EcPV.s_write env (EcModules.stmt s2) in
   let subst = Fsubst.f_subst_mem mhr (fst m) in
@@ -203,11 +207,13 @@ let process_app (side, dir, k, phi, bd_info) tc =
   | Single i, PAppNone when is_hoareS concl ->
     check_side side;
     let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in
+    let i = EcProofTyping.tc1_process_codepos1 tc (side, i) in
     t_hoare_app i phi tc
 
   | Single i, PAppNone when is_eHoareS concl ->
     check_side side;
     let _, phi = TTC.tc1_process_Xhl_formula_xreal tc (get_single phi) in
+    let i = EcProofTyping.tc1_process_codepos1 tc (side, i) in
     t_ehoare_app i phi tc
 
   | Single i, PAppNone when is_equivS concl ->
@@ -222,15 +228,21 @@ let process_app (side, dir, k, phi, bd_info) tc =
       match side with
       | None -> tc_error !!tc "seq onsided: side information expected"
       | Some side -> side in
+    let i = EcProofTyping.tc1_process_codepos1 tc (Some side, i) in
     t_equiv_app_onesided side i pre post tc
 
   | Single i, _ when is_bdHoareS concl ->
+      check_side side;
       let _, pia = TTC.tc1_process_Xhl_formula tc (get_single phi) in
       let (ra, f1, f2, f3, f4) = process_phl_bd_info dir bd_info tc in
+      let i = EcProofTyping.tc1_process_codepos1 tc (side, i) in
       t_bdhoare_app i (ra, pia, f1, f2, f3, f4) tc
 
   | Double (i, j), PAppNone when is_equivS concl ->
+      check_side side;
       let phi = TTC.tc1_process_prhl_formula tc (get_single phi) in
+      let i = EcProofTyping.tc1_process_codepos1 tc (Some `Left, i) in
+      let j = EcProofTyping.tc1_process_codepos1 tc (Some `Left, j) in
       t_equiv_app (i, j) phi tc
 
   | Single _, PAppNone
diff --git a/src/phl/ecPhlApp.mli b/src/phl/ecPhlApp.mli
index 860062774..2036ee667 100644
--- a/src/phl/ecPhlApp.mli
+++ b/src/phl/ecPhlApp.mli
@@ -3,6 +3,7 @@ open EcUtils
 open EcParsetree
 open EcFol
 open EcCoreGoal.FApi
+open EcMatching.Position
 
 (* -------------------------------------------------------------------- *)
 val t_hoare_app   : codepos1 -> form -> backward
diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml
index 2efe48fb7..884749a7e 100644
--- a/src/phl/ecPhlCodeTx.ml
+++ b/src/phl/ecPhlCodeTx.ml
@@ -293,16 +293,20 @@ let t_cfold = FApi.t_low3 "code-tx-cfold" t_cfold_r
 
 (* -------------------------------------------------------------------- *)
 let process_cfold (side, cpos, olen) tc =
+  let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
   t_cfold side cpos olen tc
 
 let process_kill (side, cpos, len) tc =
+  let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
   t_kill side cpos len tc
 
 let process_alias (side, cpos, id) tc =
+  let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
   t_alias side cpos id tc
 
 let process_set (side, cpos, fresh, id, e) tc =
   let e = TTC.tc1_process_Xhl_exp tc side None e in
+  let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
   t_set side cpos (fresh, id) e tc
 
 (* -------------------------------------------------------------------- *)
@@ -363,7 +367,7 @@ let process_weakmem (side, id, params) tc =
   FApi.xmutate1 tc `WeakenMem [concl]
 
 (* -------------------------------------------------------------------- *)
-let process_case ((side, pos) : side option * codepos) (tc : tcenv1) =
+let process_case ((side, pos) : side option * pcodepos) (tc : tcenv1) =
   let (env, _, concl) = FApi.tc1_eflat tc in
 
   let change (i : instr) =
@@ -396,8 +400,8 @@ let process_case ((side, pos) : side option * codepos) (tc : tcenv1) =
     assert false;
 
   let _, s = EcLowPhlGoal.tc1_get_stmt side tc in
-  let goals, s = EcMatching.Zipper.map pos change s in
+  let pos = EcProofTyping.tc1_process_codepos tc (side, pos) in
+  let goals, s = EcMatching.Zipper.map env pos change s in
   let concl = EcLowPhlGoal.hl_set_stmt side concl s in
 
   FApi.xmutate1 tc `ProcCase (goals @ [concl])
-
diff --git a/src/phl/ecPhlCodeTx.mli b/src/phl/ecPhlCodeTx.mli
index fa6ff09e0..e6c24752b 100644
--- a/src/phl/ecPhlCodeTx.mli
+++ b/src/phl/ecPhlCodeTx.mli
@@ -2,6 +2,7 @@
 open EcParsetree
 open EcTypes
 open EcCoreGoal.FApi
+open EcMatching.Position
 
 (* -------------------------------------------------------------------- *)
 val t_kill  : oside -> codepos -> int option -> backward
@@ -10,11 +11,11 @@ val t_set   : oside -> codepos -> bool * psymbol -> expr -> backward
 val t_cfold : oside -> codepos -> int option -> backward
 
 (* -------------------------------------------------------------------- *)
-val process_kill  : oside * codepos * int option -> backward
-val process_alias : oside * codepos * psymbol option -> backward
-val process_set   : oside * codepos * bool * psymbol * pexpr -> backward
-val process_cfold : oside * codepos * int option -> backward
-val process_case  : oside * codepos -> backward
+val process_kill  : oside * pcodepos * int option -> backward
+val process_alias : oside * pcodepos * psymbol option -> backward
+val process_set   : oside * pcodepos * bool * psymbol * pexpr -> backward
+val process_cfold : oside * pcodepos * int option -> backward
+val process_case  : oside * pcodepos -> backward
 
 (* -------------------------------------------------------------------- *)
 val process_weakmem : (oside * psymbol * fun_params) -> backward
diff --git a/src/phl/ecPhlEager.ml b/src/phl/ecPhlEager.ml
index be52acd59..65d1541a6 100644
--- a/src/phl/ecPhlEager.ml
+++ b/src/phl/ecPhlEager.ml
@@ -32,10 +32,11 @@ let pf_hSS pf hyps h =
 
 (* -------------------------------------------------------------------- *)
 let tc1_destr_eagerS tc s s' =
+  let env = FApi.tc1_env tc in
   let es = tc1_as_equivS tc in
   let c , c' = es.es_sl, es.es_sr in
-  let s1, c  = s_split (Zpr.cpos (List.length s.s_node)) c in
-  let c',s1' = s_split (Zpr.cpos (List.length c'.s_node - List.length s'.s_node)) c' in
+  let s1, c  = s_split env (Zpr.cpos (List.length s.s_node)) c in
+  let c',s1' = s_split env (Zpr.cpos (List.length c'.s_node - List.length s'.s_node)) c' in
 
   if not (List.all2 i_equal s1 s.s_node) then begin
     let ppe  = EcPrinting.PPEnv.ofenv (FApi.tc1_env tc) in
@@ -103,8 +104,8 @@ let t_eager_seq_r i j eqR h tc =
   pf_compat !!tc env (s_write env s) (s_write env s') seqR eqIs eqXs;
 
   let eqO2 = Mpv2.eq_refl (PV.fv env (fst eC.es_mr) eC.es_po) in
-  let c1 ,c2  = s_split i c in
-  let c1',c2' = s_split j c' in
+  let c1 ,c2  = s_split env i c in
+  let c1',c2' = s_split env j c' in
 
   let to_form eq =  Mpv2.to_form (fst eC.es_ml) (fst eC.es_mr) eq f_true in
 
@@ -613,6 +614,8 @@ let process_info info tc =
 let process_seq info (i, j) eqR tc =
   let eqR   = TTC.tc1_process_prhl_form tc tbool eqR in
   let gs, h = process_info info tc in
+  let i = EcProofTyping.tc1_process_codepos1 tc (Some `Left , i) in
+  let j = EcProofTyping.tc1_process_codepos1 tc (Some `Right, j) in
   FApi.t_last (t_eager_seq i j eqR h) gs
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/phl/ecPhlEager.mli b/src/phl/ecPhlEager.mli
index 0e8435233..b105deae2 100644
--- a/src/phl/ecPhlEager.mli
+++ b/src/phl/ecPhlEager.mli
@@ -3,6 +3,7 @@ open EcUtils
 open EcParsetree
 open EcFol
 open EcCoreGoal.FApi
+open EcMatching.Position
 
 (* -------------------------------------------------------------------- *)
 val t_eager_seq     : codepos1 -> codepos1 -> form -> EcIdent.t -> backward
@@ -13,7 +14,7 @@ val t_eager_fun_abs : EcFol.form -> EcIdent.t -> backward
 val t_eager_call    : form -> form -> backward
 
 (* -------------------------------------------------------------------- *)
-val process_seq     : eager_info -> codepos1 pair -> pformula -> backward
+val process_seq     : eager_info -> pcodepos1 pair -> pformula -> backward
 val process_if      : backward
 val process_while   : eager_info -> backward
 val process_fun_def : backward
diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml
index 6c7e1c72d..88dfad5b4 100644
--- a/src/phl/ecPhlEqobs.ml
+++ b/src/phl/ecPhlEqobs.ml
@@ -434,8 +434,10 @@ let process_eqobs_inS info tc =
         (FApi.t_try (FApi.t_seq EcPhlSkip.t_skip t_trivial))
         (t_eqobs_inS sim eqo tc)
     | Some(p1,p2) ->
-      let _,sl2 = s_split p1 es.es_sl in
-      let _,sr2 = s_split p2 es.es_sr in
+      let p1 = EcProofTyping.tc1_process_codepos1 tc (Some `Left , p1) in
+      let p2 = EcProofTyping.tc1_process_codepos1 tc (Some `Right, p2) in
+      let _,sl2 = s_split env p1 es.es_sl in
+      let _,sr2 = s_split env p2 es.es_sr in
       let _, eqi =
         try s_eqobs_in_full (stmt sl2) (stmt sr2) sim Mpv2.empty_local eqo
         with EqObsInError -> tc_error !!tc "cannot apply sim" in
diff --git a/src/phl/ecPhlFel.ml b/src/phl/ecPhlFel.ml
index 1490db585..0bfdfbb7a 100644
--- a/src/phl/ecPhlFel.ml
+++ b/src/phl/ecPhlFel.ml
@@ -133,7 +133,7 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc =
     with _ -> tc_error !!tc "not applicable to abstract functions"
   in
 
-  let s_hd, s_tl = EcLowPhlGoal.s_split at_pos fdef.f_body in
+  let s_hd, s_tl = EcLowPhlGoal.s_split env at_pos fdef.f_body in
   let fve        = PV.fv env mhr f_event in
   let fvc        = PV.fv env mhr cntr in
   let fvi        = PV.fv env mhr inv in
@@ -256,6 +256,7 @@ let process_fel at_pos (infos : fel_info) tc =
       -> destr_pr pr
     | _ -> tc_error !!tc "a goal of the form Pr[ _ ] <= _ is required" in
 
+  let at_pos  = EcTyping.trans_codepos1 env at_pos in
   let hyps    = LDecl.inv_memenv1 hyps1 in
   let cntr    = TTC.pf_process_form !!tc hyps tint infos.pfel_cntr in
   let ash     = TTC.pf_process_form !!tc hyps (tfun tint treal) infos.pfel_asg in
diff --git a/src/phl/ecPhlFel.mli b/src/phl/ecPhlFel.mli
index 7335c48b1..283d4b2a7 100644
--- a/src/phl/ecPhlFel.mli
+++ b/src/phl/ecPhlFel.mli
@@ -3,6 +3,7 @@ open EcPath
 open EcParsetree
 open EcFol
 open EcCoreGoal.FApi
+open EcMatching.Position
 
 (* -------------------------------------------------------------------- *)
 val t_failure_event :
@@ -13,4 +14,4 @@ val t_failure_event :
   -> backward
 
 (* -------------------------------------------------------------------- *)
-val process_fel : codepos1 -> fel_info -> backward
+val process_fel : pcodepos1 -> fel_info -> backward
diff --git a/src/phl/ecPhlHiCond.ml b/src/phl/ecPhlHiCond.ml
index de25c70ff..77ffeb1b2 100644
--- a/src/phl/ecPhlHiCond.ml
+++ b/src/phl/ecPhlHiCond.ml
@@ -4,10 +4,11 @@ open EcCoreGoal
 open EcLowGoal
 open EcLowPhlGoal
 open EcPhlCond
+open EcMatching.Position
 
 (* -------------------------------------------------------------------- *)
-let process_cond info tc =
-  let default_if (i : EcParsetree.codepos1 option) s =
+let process_cond (info : EcParsetree.pcond_info) tc =
+  let default_if (i : codepos1 option) s =
     ofdfl (fun _ -> Zpr.cpos (tc1_pos_last_if tc s)) i in
 
   match info with
@@ -21,6 +22,8 @@ let process_cond info tc =
   | `Seq (side, (i1, i2), f) ->
     let es = tc1_as_equivS tc in
     let f  = EcProofTyping.tc1_process_prhl_formula tc f in
+    let i1 = Option.map (fun i1 -> EcProofTyping.tc1_process_codepos1 tc (side, i1)) i1 in
+    let i2 = Option.map (fun i2 -> EcProofTyping.tc1_process_codepos1 tc (side, i2)) i2 in
     let n1 = default_if i1 es.es_sl in
     let n2 = default_if i2 es.es_sr in
     FApi.t_seqsub (EcPhlApp.t_equiv_app (n1, n2) f)
@@ -28,6 +31,7 @@ let process_cond info tc =
 
   | `SeqOne (s, i, f1, f2) ->
     let es = tc1_as_equivS tc in
+    let i = Option.map (fun i1 -> EcProofTyping.tc1_process_codepos1 tc (Some s, i1)) i in
     let n = default_if i (match s with `Left -> es.es_sl | `Right -> es.es_sr) in
     let _, f1 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f1 in
     let _, f2 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f2 in
diff --git a/src/phl/ecPhlInline.ml b/src/phl/ecPhlInline.ml
index 0004785f2..25a74be2f 100644
--- a/src/phl/ecPhlInline.ml
+++ b/src/phl/ecPhlInline.ml
@@ -316,10 +316,10 @@ module HiInternal = struct
     in fun (p : Zp.spath) -> aux_s IPpat p
 
   (* ------------------------------------------------------------------ *)
-  let pat_of_codepos pos stmt =
+  let pat_of_codepos env pos stmt =
     let module Zp = EcMatching.Zipper in
 
-    let zip = Zp.zipper_of_cpos pos stmt in
+    let zip = Zp.zipper_of_cpos env pos stmt in
     match zip.Zp.z_tail with
     | { i_node = Scall _ } :: tl ->
          pat_of_spath ((zip.Zp.z_head, tl), zip.Zp.z_path)
@@ -400,21 +400,23 @@ let process_inline_occs ~use_tuple side cond occs tc =
 
 (* -------------------------------------------------------------------- *)
 let process_inline_codepos ~use_tuple side pos tc =
+  let env = FApi.tc1_env tc in
   let concl = FApi.tc1_goal tc in
+  let pos = EcProofTyping.tc1_process_codepos tc (side, pos) in
 
   try
     match concl.f_node, side with
     | FequivS es, Some b ->
         let st = sideif b es.es_sl es.es_sr in
-        let sp = HiInternal.pat_of_codepos pos st in
+        let sp = HiInternal.pat_of_codepos env pos st in
         t_inline_equiv ~use_tuple b sp tc
 
     | FhoareS hs, None ->
-        let sp = HiInternal.pat_of_codepos pos hs.hs_s in
+        let sp = HiInternal.pat_of_codepos env pos hs.hs_s in
         t_inline_hoare ~use_tuple sp tc
 
     | FbdHoareS bhs, None ->
-        let sp = HiInternal.pat_of_codepos pos bhs.bhs_s in
+        let sp = HiInternal.pat_of_codepos env pos bhs.bhs_s in
         t_inline_bdhoare ~use_tuple sp tc
 
     | _, _ -> tc_error !!tc "invalid arguments"
diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml
index 632acc571..34ddfa0ea 100644
--- a/src/phl/ecPhlLoopTx.ml
+++ b/src/phl/ecPhlLoopTx.ml
@@ -18,10 +18,10 @@ module Zpr = EcMatching.Zipper
 module TTC = EcProofTyping
 
 (* -------------------------------------------------------------------- *)
-type fission_t    = oside * codepos * (int * (int * int))
-type fusion_t     = oside * codepos * (int * (int * int))
-type unroll_t     = oside * codepos * bool
-type splitwhile_t = pexpr * oside * codepos
+type fission_t    = oside * pcodepos * (int * (int * int))
+type fusion_t     = oside * pcodepos * (int * (int * int))
+type unroll_t     = oside * pcodepos * bool
+type splitwhile_t = pexpr * oside * pcodepos
 
 (* -------------------------------------------------------------------- *)
 let check_independence (pf, hyps) b init c1 c2 c3 =
@@ -205,26 +205,27 @@ let t_splitwhile = FApi.t_low3 "split-while" t_splitwhile_r
 
 (* -------------------------------------------------------------------- *)
 let process_fission (side, cpos, infos) tc =
+  let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
   t_fission side cpos infos tc
 
 let process_fusion (side, cpos, infos) tc =
+  let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
   t_fusion side cpos infos tc
 
 let process_splitwhile (b, side, cpos) tc =
   let b =
     try  TTC.tc1_process_Xhl_exp tc side (Some tbool) b
-    with EcFol.DestrError _ -> tc_error !!tc "goal must be a *HL statement"
-  in t_splitwhile b side cpos tc
+    with EcFol.DestrError _ -> tc_error !!tc "goal must be a *HL statement" in
+  let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
+  t_splitwhile b side cpos tc
 
 (* -------------------------------------------------------------------- *)
 let process_unroll_for side cpos tc =
-  if not (List.is_empty (fst cpos)) then
-    tc_error !!tc "cannot use deep code position";
-
   let env  = FApi.tc1_env tc in
   let hyps = FApi.tc1_hyps tc in
   let _, c = EcLowPhlGoal.tc1_get_stmt side tc in
-  let z    = Zpr.zipper_of_cpos cpos c in
+  let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
+  let z    = Zpr.zipper_of_cpos env cpos c in
   let pos  = 1 + List.length z.Zpr.z_head in
 
   (* Extract loop condition / body *)
@@ -320,6 +321,9 @@ let process_unroll_for side cpos tc =
 
 (* -------------------------------------------------------------------- *)
 let process_unroll (side, cpos, for_) tc =
-  if   for_
-  then process_unroll_for side cpos tc
-  else t_unroll side cpos tc
+  if for_ then
+    process_unroll_for side cpos tc
+  else begin
+    let cpos = EcProofTyping.tc1_process_codepos tc (side, cpos) in
+    t_unroll side cpos tc
+  end
\ No newline at end of file
diff --git a/src/phl/ecPhlLoopTx.mli b/src/phl/ecPhlLoopTx.mli
index 85ca2053d..8d619f9af 100644
--- a/src/phl/ecPhlLoopTx.mli
+++ b/src/phl/ecPhlLoopTx.mli
@@ -2,21 +2,21 @@
 open EcParsetree
 open EcTypes
 open EcCoreGoal.FApi
+open EcMatching.Position
 
 (* -------------------------------------------------------------------- *)
-type fission_t    = oside * codepos * (int * (int * int))
-type fusion_t     = oside * codepos * (int * (int * int))
-type unroll_t     = oside * codepos * bool
-type splitwhile_t = pexpr * oside * codepos
-
 val t_fission    : oside -> codepos -> int * (int * int) -> backward
 val t_fusion     : oside -> codepos -> int * (int * int) -> backward
 val t_unroll     : oside -> codepos -> backward
 val t_splitwhile : expr -> oside -> codepos -> backward
 
-
 (* -------------------------------------------------------------------- *)
-val process_unroll_for : oside -> codepos -> backward
+type fission_t    = oside * pcodepos * (int * (int * int))
+type fusion_t     = oside * pcodepos * (int * (int * int))
+type unroll_t     = oside * pcodepos * bool
+type splitwhile_t = pexpr * oside * pcodepos
+
+val process_unroll_for : oside -> pcodepos -> backward
 val process_fission    : fission_t -> backward
 val process_fusion     : fusion_t -> backward
 val process_unroll     : unroll_t -> backward
diff --git a/src/phl/ecPhlOutline.ml b/src/phl/ecPhlOutline.ml
index a727e25dc..6774ad118 100644
--- a/src/phl/ecPhlOutline.ml
+++ b/src/phl/ecPhlOutline.ml
@@ -107,6 +107,7 @@ let t_equivS_trans_eq side s tc =
 (* FIXME: Maybe move to ecPhlTrans as well *)
 
 let t_outline_stmt side start_pos end_pos s tc =
+  let env = FApi.tc1_env tc in
   let goal = tc1_as_equivS tc in
 
   (* Check which memory/program we are outlining *)
@@ -116,8 +117,8 @@ let t_outline_stmt side start_pos end_pos s tc =
   in
 
   (* Extract the program prefix and suffix *)
-  let rest, code_suff  = s_split end_pos code in
-  let code_pref, _, _ = s_split_i start_pos (stmt rest) in
+  let rest, code_suff  = s_split env end_pos code in
+  let code_pref, _, _ = s_split_i env start_pos (stmt rest) in
 
   let new_prog = s_seq (s_seq (stmt code_pref) s) (stmt code_suff) in
   let tc = t_equivS_trans_eq side new_prog tc in
@@ -180,12 +181,12 @@ let t_outline_proc side start_pos end_pos fname res_lv tc =
 
   (* Get the return statement and body we will attempt to unify *)
   let old_code_body, old_code_ret =
-    let rest, ret_instr, _ = s_split_i end_pos code in
+    let rest, ret_instr, _ = s_split_i env end_pos code in
     let body =
        if start_pos = end_pos then
          s_empty
        else
-         let _, hd, tl  = s_split_i start_pos (stmt rest) in
+         let _, hd, tl  = s_split_i env start_pos (stmt rest) in
          stmt (hd :: tl)
     in
 
@@ -232,14 +233,18 @@ let t_outline_proc side start_pos end_pos fname res_lv tc =
 (* Process a user call to outline *)
 
 let process_outline info tc =
-  let side = info.outline_side in
-  let start_pos = info.outline_start in
-  let end_pos = info.outline_end in
-
   let env = tc1_env tc in
+  let side = info.outline_side in
   let goal = tc1_as_equivS tc in
   let ppe = EcPrinting.PPEnv.ofenv env in
 
+  let start_pos =
+    EcProofTyping.tc1_process_codepos1 tc
+      (Some side, info.outline_start) in
+  let end_pos =
+    EcProofTyping.tc1_process_codepos1 tc
+      (Some side, info.outline_end) in
+
   (* Check which memory we are outlining *)
   let mem = match side with
     | `Left  -> goal.es_ml
diff --git a/src/phl/ecPhlOutline.mli b/src/phl/ecPhlOutline.mli
index 5477994f4..ceb411636 100644
--- a/src/phl/ecPhlOutline.mli
+++ b/src/phl/ecPhlOutline.mli
@@ -1,4 +1,5 @@
 open EcCoreGoal.FApi
+open EcMatching.Position
 open EcParsetree
 open EcModules
 open EcPath
diff --git a/src/phl/ecPhlRCond.ml b/src/phl/ecPhlRCond.ml
index 4a328ee18..e28a07939 100644
--- a/src/phl/ecPhlRCond.ml
+++ b/src/phl/ecPhlRCond.ml
@@ -13,8 +13,8 @@ open EcLowPhlGoal
 (* -------------------------------------------------------------------- *)
 module Low = struct
   (* ------------------------------------------------------------------ *)
-  let gen_rcond pf b m at_pos s =
-    let head, i, tail = s_split_i at_pos s in
+  let gen_rcond (pf, env) b m at_pos s =
+    let head, i, tail = s_split_i env at_pos s in
     let e, s =
       match i.i_node with
       | Sif(e,s1,s2) -> e, if b then s1.s_node else s2.s_node
@@ -31,18 +31,20 @@ module Low = struct
 
   (* ------------------------------------------------------------------ *)
   let t_hoare_rcond_r b at_pos tc =
+    let env = FApi.tc1_env tc in
     let hs = tc1_as_hoareS tc in
     let m  = EcMemory.memory hs.hs_m in
-    let hd,_,e,s = gen_rcond !!tc b m at_pos hs.hs_s in
+    let hd,_,e,s = gen_rcond (!!tc, env) b m at_pos hs.hs_s in
     let concl1  = f_hoareS_r { hs with hs_s = hd; hs_po = e } in
     let concl2  = f_hoareS_r { hs with hs_s = s } in
     FApi.xmutate1 tc `RCond [concl1; concl2]
 
   (* ------------------------------------------------------------------ *)
   let t_ehoare_rcond_r b at_pos tc =
+    let env = FApi.tc1_env tc in
     let hs = tc1_as_ehoareS tc in
     let m  = EcMemory.memory hs.ehs_m in
-    let hd,_,e,s = gen_rcond !!tc b m at_pos hs.ehs_s in
+    let hd,_,e,s = gen_rcond (!!tc, env) b m at_pos hs.ehs_s in
     let pre =
       match destr_app hs.ehs_pr with
       | o, pre :: _ when f_equal o fop_interp_ehoare_form -> pre
@@ -54,21 +56,23 @@ module Low = struct
 
   (* ------------------------------------------------------------------ *)
   let t_bdhoare_rcond_r b at_pos tc =
+    let env = FApi.tc1_env tc in
     let bhs = tc1_as_bdhoareS tc in
     let m  = EcMemory.memory bhs.bhs_m in
-    let hd,_,e,s = gen_rcond !!tc b m at_pos bhs.bhs_s in
+    let hd,_,e,s = gen_rcond (!!tc, env) b m at_pos bhs.bhs_s in
     let concl1  = f_hoareS bhs.bhs_m bhs.bhs_pr hd e in
     let concl2  = f_bdHoareS_r { bhs with bhs_s = s } in
     FApi.xmutate1 tc `RCond [concl1; concl2]
 
   (* ------------------------------------------------------------------ *)
   let t_equiv_rcond_r side b at_pos tc =
+    let env = FApi.tc1_env tc in
     let es = tc1_as_equivS tc in
     let m,mo,s =
       match side with
       | `Left  -> es.es_ml,es.es_mr, es.es_sl
       | `Right -> es.es_mr,es.es_ml, es.es_sr in
-    let hd,_,e,s = gen_rcond !!tc b EcFol.mhr at_pos s in
+    let hd,_,e,s = gen_rcond (!!tc, env) b EcFol.mhr at_pos s in
     let mo' = EcIdent.create "&m" in
     let s1 = Fsubst.f_subst_id in
     let s1 = Fsubst.f_bind_mem s1 (EcMemory.memory m) EcFol.mhr in
@@ -103,13 +107,14 @@ let t_rcond side b at_pos tc =
     Low.t_equiv_rcond side b at_pos tc
 
 let process_rcond side b at_pos tc =
+  let at_pos = EcProofTyping.tc1_process_codepos1 tc (side, at_pos) in
   t_rcond side b at_pos tc
 
 (* -------------------------------------------------------------------- *)
 module LowMatch = struct
   (* ------------------------------------------------------------------ *)
   let gen_rcond (pf, env) c m at_pos s =
-    let head, i, tail = s_split_i at_pos s in
+    let head, i, tail = s_split_i env at_pos s in
     let e, infos, (cvars, subs) =
       match i.i_node with
       | Smatch (e, bs) -> begin
@@ -309,3 +314,8 @@ let t_rcond_match side c at_pos tc =
   | None when is_eHoareS concl -> LowMatch.t_ehoare_rcond_match c at_pos tc
   | None -> LowMatch.t_hoare_rcond_match c at_pos tc
   | Some side -> LowMatch.t_equiv_rcond_match side c at_pos tc
+
+(* -------------------------------------------------------------------- *)
+let process_rcond_match side c at_pos tc =
+  let at_pos = EcProofTyping.tc1_process_codepos1 tc (side, at_pos) in
+  t_rcond_match side c at_pos tc
diff --git a/src/phl/ecPhlRCond.mli b/src/phl/ecPhlRCond.mli
index ef7c378e8..87306ed99 100644
--- a/src/phl/ecPhlRCond.mli
+++ b/src/phl/ecPhlRCond.mli
@@ -2,6 +2,7 @@
 open EcSymbols
 open EcParsetree
 open EcCoreGoal.FApi
+open EcMatching.Position
 
 (* -------------------------------------------------------------------- *)
 module Low : sig
@@ -20,5 +21,8 @@ end
 
 (* -------------------------------------------------------------------- *)
 val t_rcond       : oside -> bool -> codepos1 -> backward
-val process_rcond : oside -> bool -> codepos1 -> backward
-val t_rcond_match : oside -> symbol -> codepos1 -> backward
+val process_rcond : oside -> bool -> pcodepos1 -> backward
+
+(* -------------------------------------------------------------------- *)
+val process_rcond_match : oside -> symbol -> pcodepos1 -> backward
+val t_rcond_match       : oside -> symbol -> codepos1 -> backward
diff --git a/src/phl/ecPhlRewrite.ml b/src/phl/ecPhlRewrite.ml
index 796f05e36..81fec34a3 100644
--- a/src/phl/ecPhlRewrite.ml
+++ b/src/phl/ecPhlRewrite.ml
@@ -19,7 +19,7 @@ let get_expression_of_instruction (i : instr) =
 (* -------------------------------------------------------------------- *)
 let t_change
     (side : side option)
-    (pos  : codepos)
+    (pos  : EcMatching.Position.codepos)
     (expr : expr -> LDecl.hyps * memenv -> 'a * expr)
     (tc   : tcenv1)
 =
@@ -52,7 +52,8 @@ let t_change
       (hoare | ehoare | phoare | equiv)";
 
   let m, s = EcLowPhlGoal.tc1_get_stmt side tc in
-  let (data, goals), s = EcMatching.Zipper.map pos (change m) s in
+  let (data, goals), s =
+    EcMatching.Zipper.map (FApi.tc1_env tc) pos (change m) s in
   let concl = EcLowPhlGoal.hl_set_stmt side concl s in
 
   data, FApi.xmutate1 tc `ProcChange (goals @ [concl])
@@ -60,10 +61,12 @@ let t_change
 (* -------------------------------------------------------------------- *)
 let process_change
     (side : side option)
-    (pos  : codepos)
+    (pos  : pcodepos)
     (form : pexpr)
     (tc   : tcenv1)
 =
+  let pos = EcProofTyping.tc1_process_codepos tc (side, pos) in
+
   let expr (e : expr) ((hyps, m) : LDecl.hyps * memenv) =
     let hyps = LDecl.push_active m hyps in
     let e =
@@ -77,7 +80,7 @@ let process_change
 (* -------------------------------------------------------------------- *)
 let process_rewrite_rw
     (side : side option)
-    (pos  : codepos)
+    (pos  : pcodepos)
     (pt   : ppterm)
     (tc   : tcenv1)
 =
@@ -124,8 +127,8 @@ let process_rewrite_rw
     (m, data), expr_of_form (fst m) e
   in
 
+  let pos = EcProofTyping.tc1_process_codepos tc (side, pos) in
   let (m, (pt, mode, cpos)), tc = t_change side pos change tc in
-
   let cpos = EcMatching.FPosition.reroot [1] cpos in
 
   let discharge (tc : tcenv1) =
@@ -141,7 +144,7 @@ let process_rewrite_rw
 (* -------------------------------------------------------------------- *)
 let process_rewrite_simpl
   (side : side option)
-  (pos  : codepos)
+  (pos  : pcodepos)
   (tc   : tcenv1)
 =
 let ri = EcReduction.nodelta in
@@ -153,6 +156,7 @@ let change (e : expr) ((hyps, me) : LDecl.hyps * memenv) =
     (fst me, f), e
   in
 
+  let pos = EcProofTyping.tc1_process_codepos tc (side, pos) in
   let (m, f), tc = t_change side pos change tc in
 
   FApi.t_first (
@@ -166,7 +170,7 @@ let change (e : expr) ((hyps, me) : LDecl.hyps * memenv) =
 (* -------------------------------------------------------------------- *)
 let process_rewrite
   (side : side option)
-  (pos  : codepos)
+  (pos  : pcodepos)
   (rw   : prrewrite)
   (tc   : tcenv1)
 =
diff --git a/src/phl/ecPhlRewrite.mli b/src/phl/ecPhlRewrite.mli
index 8b7c76c0d..f3b1c3523 100644
--- a/src/phl/ecPhlRewrite.mli
+++ b/src/phl/ecPhlRewrite.mli
@@ -3,8 +3,8 @@ open EcParsetree
 open EcCoreGoal.FApi
 
 (* -------------------------------------------------------------------- *)
-val process_change : side option -> codepos -> pexpr -> backward
+val process_change : side option -> pcodepos -> pexpr -> backward
 
-val process_rewrite_rw    : side option -> codepos -> ppterm -> backward
-val process_rewrite_simpl : side option -> codepos -> backward
-val process_rewrite       : side option -> codepos -> prrewrite -> backward
+val process_rewrite_rw    : side option -> pcodepos -> ppterm -> backward
+val process_rewrite_simpl : side option -> pcodepos -> backward
+val process_rewrite       : side option -> pcodepos -> prrewrite -> backward
diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml
index 12ebf095c..780bf5708 100644
--- a/src/phl/ecPhlRnd.ml
+++ b/src/phl/ecPhlRnd.ml
@@ -7,6 +7,7 @@ open EcModules
 open EcFol
 open EcPV
 
+open EcMatching.Position
 open EcCoreGoal
 open EcLowGoal
 open EcLowPhlGoal
@@ -18,6 +19,7 @@ type chl_infos_t = (form, form option, form) rnd_tac_info
 type bhl_infos_t = (form, ty -> form option, ty -> form) rnd_tac_info
 type rnd_infos_t = (pformula, pformula option, pformula) rnd_tac_info
 type mkbij_t     = EcTypes.ty -> EcTypes.ty -> EcFol.form
+type semrndpos   = (bool * codepos1) doption
 
 (* -------------------------------------------------------------------- *)
 module Core = struct
@@ -375,8 +377,9 @@ module Core = struct
 
   (* -------------------------------------------------------------------- *)
   let t_hoare_rndsem_r reduce pos tc =
+    let env = FApi.tc1_env tc in
     let hs = tc1_as_hoareS tc in
-    let s1, s2 = o_split (Some pos) hs.hs_s in
+    let s1, s2 = o_split env (Some pos) hs.hs_s in
     let fv =
       if reduce then
         Some (PV.fv (FApi.tc1_env tc) (fst hs.hs_m) hs.hs_po)
@@ -387,8 +390,9 @@ module Core = struct
 
  (* -------------------------------------------------------------------- *)
   let t_bdhoare_rndsem_r reduce pos tc =
+    let env = FApi.tc1_env tc in
     let bhs = tc1_as_bdhoareS tc in
-    let s1, s2 = o_split (Some pos) bhs.bhs_s in
+    let s1, s2 = o_split env (Some pos) bhs.bhs_s in
     let fv =
       if reduce then
         Some (PV.fv (FApi.tc1_env tc) (fst bhs.bhs_m) bhs.bhs_po)
@@ -399,12 +403,13 @@ module Core = struct
 
  (* -------------------------------------------------------------------- *)
   let t_equiv_rndsem_r reduce side pos tc =
+    let env = FApi.tc1_env tc in
     let es = tc1_as_equivS tc in
     let s, m =
       match side with
       | `Left  -> es.es_sl, es.es_ml
       | `Right -> es.es_sr, es.es_mr in
-    let s1, s2 = o_split (Some pos) s in
+    let s1, s2 = o_split env (Some pos) s in
     let fv =
       if reduce then
         Some (PV.fv (FApi.tc1_env tc) (fst m) es.es_po)
@@ -645,9 +650,23 @@ let process_rnd side pos tac_info tc =
       | PSingleRndParam f -> Some (process_form f), None
       | PTwoRndParams (f, finv) -> Some (process_form f), Some (process_form finv)
       | _ -> tc_error !!tc "invalid arguments"
+    in
 
+    let pos = pos |> Option.map (function
+      | Single (b, p) ->
+          let p =
+            if Option.is_some side then
+              EcProofTyping.tc1_process_codepos1 tc (side, p)
+            else EcTyping.trans_codepos1 (FApi.tc1_env tc) p
+          in Single (b, p)
+      | Double ((b1, p1), (b2, p2)) ->
+          let p1 = EcProofTyping.tc1_process_codepos1 tc (Some `Left , p1) in
+          let p2 = EcProofTyping.tc1_process_codepos1 tc (Some `Right, p2) in
+          Double ((b1, p1), (b2, p2))
+    )
     in
-      t_equiv_rnd side ?pos bij_info tc
+    
+    t_equiv_rnd side ?pos bij_info tc
 
   | _ -> tc_error !!tc "invalid arguments"
 
@@ -659,6 +678,7 @@ let t_equiv_rndsem   = FApi.t_low3 "equiv-rndsem"   Core.t_equiv_rndsem_r
 (* -------------------------------------------------------------------- *)
 let process_rndsem ~reduce side pos tc =
   let concl = FApi.tc1_goal tc in
+  let pos = EcProofTyping.tc1_process_codepos1 tc (side, pos) in
 
   match side with
   | None when is_hoareS concl ->
diff --git a/src/phl/ecPhlRnd.mli b/src/phl/ecPhlRnd.mli
index 6d74486aa..29d6865e2 100644
--- a/src/phl/ecPhlRnd.mli
+++ b/src/phl/ecPhlRnd.mli
@@ -4,6 +4,7 @@ open EcParsetree
 open EcTypes
 open EcFol
 open EcCoreGoal.FApi
+open EcMatching.Position
 
 (* -------------------------------------------------------------------- *)
 type chl_infos_t = (form, form option, form) rnd_tac_info
@@ -16,12 +17,14 @@ val wp_equiv_disj_rnd : side -> backward
 val wp_equiv_rnd      : (mkbij_t pair) option -> backward
 
 (* -------------------------------------------------------------------- *)
+type semrndpos = (bool * codepos1) doption
+
 val t_hoare_rnd   : backward
 val t_bdhoare_rnd : bhl_infos_t -> backward
 val t_equiv_rnd   : ?pos:semrndpos -> oside -> (mkbij_t option) pair -> backward
 
 (* -------------------------------------------------------------------- *)
-val process_rnd : oside -> semrndpos option -> rnd_infos_t -> backward
+val process_rnd : oside -> psemrndpos option -> rnd_infos_t -> backward
 
 (* -------------------------------------------------------------------- *)
-val process_rndsem : reduce:bool -> oside -> codepos1 -> backward
+val process_rndsem : reduce:bool -> oside -> pcodepos1 -> backward
diff --git a/src/phl/ecPhlRwEquiv.ml b/src/phl/ecPhlRwEquiv.ml
index 23e99bf13..3e3806437 100644
--- a/src/phl/ecPhlRwEquiv.ml
+++ b/src/phl/ecPhlRwEquiv.ml
@@ -55,7 +55,8 @@ let t_rewrite_equiv side dir cp (equiv : equivF) equiv_pt rargslv tc =
 
   (* Extract the call statement and surrounding code *)
   let prefix, (llv, func, largs), suffix =
-    let p, i, s = s_split_i cp code in
+    let cp = EcProofTyping.tc1_process_codepos1 tc (Some side, cp) in
+    let p, i, s = s_split_i env cp code in
     if not (is_call i) then
       rwe_error RWE_InvalidPosition;
     stmt p, destr_call i, stmt s
diff --git a/src/phl/ecPhlRwEquiv.mli b/src/phl/ecPhlRwEquiv.mli
index e1186c654..eee53c609 100644
--- a/src/phl/ecPhlRwEquiv.mli
+++ b/src/phl/ecPhlRwEquiv.mli
@@ -6,7 +6,7 @@ open EcAst
 val t_rewrite_equiv :
   side ->
   [`LtoR | `RtoL ] ->
-  codepos1 ->
+  pcodepos1 ->
   equivF ->
   proofterm ->
   (expr list * lvalue option) option ->
diff --git a/src/phl/ecPhlSp.ml b/src/phl/ecPhlSp.ml
index 82359ac71..91f9167d2 100644
--- a/src/phl/ecPhlSp.ml
+++ b/src/phl/ecPhlSp.ml
@@ -1,5 +1,6 @@
 (* -------------------------------------------------------------------- *)
 open EcUtils
+open EcParsetree
 open EcAst
 open EcTypes
 open EcModules
@@ -240,15 +241,16 @@ let t_sp_side pos tc =
   match concl.f_node, pos with
   | FhoareS hs, (None | Some (Single _)) ->
       let pos = pos |> omap as_single in
-      let stmt1, stmt2 = o_split ~rev:true pos hs.hs_s in
+      let stmt1, stmt2 = o_split ~rev:true env pos hs.hs_s in
       let stmt1, hs_pr = LI.sp_stmt hs.hs_m env stmt1 hs.hs_pr in
       check_sp_progress pos stmt1;
       let subgoal = f_hoareS_r { hs with hs_s = stmt (stmt1@stmt2); hs_pr } in
       FApi.xmutate1 tc `Sp [subgoal]
 
-  | FbdHoareS bhs, (None | Some (Single _)) ->
+
+    | FbdHoareS bhs, (None | Some (Single _)) ->
       let pos = pos |> omap as_single in
-      let stmt1, stmt2 = o_split ~rev:true pos bhs.bhs_s in
+      let stmt1, stmt2 = o_split ~rev:true env pos bhs.bhs_s in
       check_form_indep stmt1 bhs.bhs_m bhs.bhs_bd;
       let stmt1, bhs_pr = LI.sp_stmt bhs.bhs_m env stmt1 bhs.bhs_pr in
       check_sp_progress pos stmt1;
@@ -260,8 +262,8 @@ let t_sp_side pos tc =
       let posL = pos |> omap fst in
       let posR = pos |> omap snd in
 
-      let stmtL1, stmtL2 = o_split ~rev:true posL es.es_sl in
-      let stmtR1, stmtR2 = o_split ~rev:true posR es.es_sr in
+      let stmtL1, stmtL2 = o_split ~rev:true env posL es.es_sl in
+      let stmtR1, stmtR2 = o_split ~rev:true env posR es.es_sr in
 
       let         es_pr = es.es_pr in
       let stmtL1, es_pr = LI.sp_stmt es.es_ml env stmtL1 es_pr in
@@ -289,3 +291,9 @@ let t_sp_side pos tc =
 
 (* -------------------------------------------------------------------- *)
 let t_sp = FApi.t_low1 "sp" t_sp_side
+
+(* -------------------------------------------------------------------- *)
+let process_sp (cpos : pcodepos1 doption option) (tc : tcenv1) =
+  let env = FApi.tc1_env tc in
+  let cpos = Option.map (EcTyping.trans_dcodepos1 env) cpos in
+  t_sp cpos tc
diff --git a/src/phl/ecPhlSp.mli b/src/phl/ecPhlSp.mli
index 8142b5eb4..2625f4030 100644
--- a/src/phl/ecPhlSp.mli
+++ b/src/phl/ecPhlSp.mli
@@ -1,7 +1,11 @@
 (* -------------------------------------------------------------------- *)
 open EcParsetree
+open EcMatching.Position
 open EcCoreGoal.FApi
 open EcUtils
 
 (* -------------------------------------------------------------------- *)
 val t_sp : (codepos1 doption) option -> backward
+
+(* -------------------------------------------------------------------- *)
+val process_sp : (pcodepos1 doption) option -> backward
diff --git a/src/phl/ecPhlWp.ml b/src/phl/ecPhlWp.ml
index 761d5c83a..9c7553f56 100644
--- a/src/phl/ecPhlWp.ml
+++ b/src/phl/ecPhlWp.ml
@@ -142,7 +142,7 @@ module TacInternal = struct
   let t_hoare_wp ?(uselet=true) i tc =
     let env = FApi.tc1_env tc in
     let hs = tc1_as_hoareS tc in
-    let (s_hd, s_wp) = o_split i hs.hs_s in
+    let (s_hd, s_wp) = o_split env i hs.hs_s in
     let s_wp = EcModules.stmt s_wp in
     let s_wp, post =
       wp ~uselet ~onesided:true env hs.hs_m s_wp hs.hs_po in
@@ -154,7 +154,7 @@ module TacInternal = struct
   let t_ehoare_wp ?(uselet=true) i tc =
     let env = FApi.tc1_env tc in
     let hs = tc1_as_ehoareS tc in
-    let (s_hd, s_wp) = o_split i hs.ehs_s in
+    let (s_hd, s_wp) = o_split env i hs.ehs_s in
     let s_wp = EcModules.stmt s_wp in
     let (s_wp, post) = ewp ~uselet env hs.ehs_m s_wp hs.ehs_po in
     check_wp_progress tc i hs.ehs_s s_wp;
@@ -165,7 +165,7 @@ module TacInternal = struct
   let t_bdhoare_wp ?(uselet=true) i tc =
     let env = FApi.tc1_env tc in
     let bhs = tc1_as_bdhoareS tc in
-    let (s_hd, s_wp) = o_split i bhs.bhs_s in
+    let (s_hd, s_wp) = o_split env i bhs.bhs_s in
     let s_wp = EcModules.stmt s_wp in
     let s_wp,post = wp ~uselet env bhs.bhs_m s_wp bhs.bhs_po in
     check_wp_progress tc i bhs.bhs_s s_wp;
@@ -177,8 +177,8 @@ module TacInternal = struct
     let env = FApi.tc1_env tc in
     let es = tc1_as_equivS tc in
     let i = omap fst ij and j = omap snd ij in
-    let s_hdl,s_wpl = o_split i es.es_sl in
-    let s_hdr,s_wpr = o_split j es.es_sr in
+    let s_hdl,s_wpl = o_split env i es.es_sl in
+    let s_hdr,s_wpr = o_split env j es.es_sr in
     let meml, s_wpl = es.es_ml, EcModules.stmt s_wpl in
     let memr, s_wpr = es.es_mr, EcModules.stmt s_wpr in
     let post = es.es_po in
@@ -223,5 +223,7 @@ let typing_wp env m s f =
 let () = EcTyping.wp := Some typing_wp
 
 (* -------------------------------------------------------------------- *)
-let process_wp k tc =
-  t_wp k tc
+let process_wp pos tc =
+  let pos =
+    Option.map (EcTyping.trans_dcodepos1 (FApi.tc1_env tc)) pos
+  in t_wp pos tc
diff --git a/src/phl/ecPhlWp.mli b/src/phl/ecPhlWp.mli
index be82a0df0..fc8689f6d 100644
--- a/src/phl/ecPhlWp.mli
+++ b/src/phl/ecPhlWp.mli
@@ -1,6 +1,7 @@
 (* -------------------------------------------------------------------- *)
 open EcUtils
 open EcParsetree
+open EcMatching.Position
 
 open EcCoreGoal.FApi
 
@@ -13,4 +14,4 @@ open EcCoreGoal.FApi
 
 val t_wp : ?uselet:bool -> (codepos1 doption) option -> backward
 
-val process_wp : (codepos1 doption) option -> backward
+val process_wp : (pcodepos1 doption) option -> backward
diff --git a/tests/codepos-assign-with-name.ec b/tests/codepos-assign-with-name.ec
new file mode 100644
index 000000000..407f7745b
--- /dev/null
+++ b/tests/codepos-assign-with-name.ec
@@ -0,0 +1,23 @@
+(* -------------------------------------------------------------------- *)
+require import AllCore.
+
+module M = {
+  proc f() = {
+    var x : int;
+    var y : int;
+
+    y <- 1;
+    x <- 0;
+    return y;
+  }
+}.
+
+op p : int -> bool.
+
+lemma L : hoare[M.f : true ==> p res].
+proof.
+proc.
+fail kill ^y<-.
+kill ^x<-.
+abort.
+