diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml
index 45af10852..88ce90195 100644
--- a/src/ecHiTacticals.ml
+++ b/src/ecHiTacticals.ml
@@ -173,7 +173,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pfun (`Upto info)         -> EcPhlFun.process_fun_upto info
     | Pfun `Code                -> EcPhlFun.process_fun_to_code
     | Pskip                     -> EcPhlSkip.t_skip
-    | Papp info                 -> EcPhlApp.process_app info
+    | Pseq info                 -> EcPhlSeq.process_seq info
     | Pwp wp                    -> EcPhlWp.process_wp wp
     | Psp sp                    -> EcPhlSp.process_sp sp
     | Prcond (side, b, i)       -> EcPhlRCond.process_rcond side b i
diff --git a/src/ecLexer.mll b/src/ecLexer.mll
index e5a5ced94..b05cfe095 100644
--- a/src/ecLexer.mll
+++ b/src/ecLexer.mll
@@ -261,8 +261,6 @@
     ("+"   , (PLUS             , false));
     ("-"   , (MINUS            , false));
     ("*"   , (STAR             , false));
-    ("<<"  , (BACKS            , false));
-    (">>"  , (FWDS             , false));
     ("<:"  , (LTCOLON          , false));
     ("==>" , (LONGARROW        , false));
     ("="   , (EQ               , false));
diff --git a/src/ecParser.mly b/src/ecParser.mly
index b1146388e..06f464f93 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -391,7 +391,6 @@
 %token AUTO
 %token AXIOM
 %token AXIOMATIZED
-%token BACKS
 %token BACKSLASH
 %token BETA
 %token BY
@@ -457,7 +456,6 @@
 %token FROM
 %token FUN
 %token FUSION
-%token FWDS
 %token GEN
 %token GLOB
 %token GLOBAL
@@ -2497,11 +2495,6 @@ call_info:
 | bad=form COMMA p=form              { CI_upto (bad,p,None) }
 | bad=form COMMA p=form COMMA q=form { CI_upto (bad,p,Some q) }
 
-tac_dir:
-| BACKS { Backs }
-| FWDS  { Fwds }
-| empty { Backs }
-
 icodepos_r:
 | IF       { (`If     :> pcp_match) }
 | WHILE    { (`While  :> pcp_match) }
@@ -2672,13 +2665,13 @@ dbhint:
 
 app_bd_info:
 | empty
-    { PAppNone }
+    { PSeqNone }
 
 | f=sform
-    { PAppSingle f }
+    { PSeqSingle f }
 
 | f=prod_form g=prod_form s=sform?
-    { PAppMult (s, fst f, snd f, fst g, snd g) }
+    { PSeqMult (s, fst f, snd f, fst g, snd g) }
 
 revert:
 | cl=ioption(brace(loc(ipcore_name)+)) gp=genpattern*
@@ -2915,8 +2908,8 @@ interleave_info:
 | PROC STAR
    { Pfun `Code }
 
-| SEQ s=side? d=tac_dir pos=s_codepos1 COLON p=form_or_double_form f=app_bd_info
-   { Papp (s, d, pos, p, f) }
+| SEQ s=side? pos=s_codepos1 COLON p=form_or_double_form f=app_bd_info
+   { Pseq (s, pos, p, f) }
 
 | WP n=s_codepos1?
    { Pwp n }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 169e22ba8..6b4f1e2b9 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -543,10 +543,10 @@ type call_info =
   | CI_inv of pformula
   | CI_upto of (pformula * pformula * pformula option)
 
-type p_app_xt_info =
-  | PAppNone
-  | PAppSingle of pformula
-  | PAppMult   of (pformula option) tuple5
+type p_seq_xt_info =
+  | PSeqNone
+  | PSeqSingle of pformula
+  | PSeqMult   of (pformula option) tuple5
 
 type ('a, 'b, 'c) rnd_tac_info =
   | PNoRndParams
@@ -559,8 +559,6 @@ type rnd_tac_info_f =
 
 type psemrndpos = (bool * pcodepos1) doption
 
-type tac_dir = Backs | Fwds
-
 type pfel_spec_preds = (pgamepath * pformula) list
 
 (* -------------------------------------------------------------------- *)
@@ -618,8 +616,8 @@ type fun_info = [
 ]
 
 (* -------------------------------------------------------------------- *)
-type app_info =
-  oside * tac_dir * pcodepos1 doption * pformula doption * p_app_xt_info
+type seq_info =
+  oside * pcodepos1 doption * pformula doption * p_seq_xt_info
 
 (* -------------------------------------------------------------------- *)
 type pcond_info = [
@@ -726,7 +724,7 @@ type phltactic =
   | Pskip
   | Prepl_stmt     of trans_info
   | Pfun           of fun_info
-  | Papp           of app_info
+  | Pseq           of seq_info
   | Pwp            of pdocodepos1
   | Psp            of pdocodepos1
   | Pwhile         of (oside * while_info)
diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml
index 8231b9f27..294512570 100644
--- a/src/phl/ecPhlCall.ml
+++ b/src/phl/ecPhlCall.ml
@@ -145,14 +145,14 @@ let t_ehoare_call_core fpre fpost tc =
 let t_ehoare_call fpre fpost tc =
   let _, _, _, s, _, wppre, _ = ehoare_call_pre_post fpre fpost tc in
   let tcenv =
-    EcPhlApp.t_ehoare_app (EcMatching.Zipper.cpos (List.length s.s_node)) wppre tc in
+    EcPhlSeq.t_ehoare_seq (EcMatching.Zipper.cpos (List.length s.s_node)) wppre tc in
   let tcenv = FApi.t_swap_goals 0 1 tcenv in
   FApi.t_sub [t_ehoare_call_core fpre fpost; t_id] tcenv
 
 let t_ehoare_call_concave f fpre fpost tc =
   let _, _, _, s, _, wppre, wppost = ehoare_call_pre_post fpre fpost tc in
   let tcenv =
-    EcPhlApp.t_ehoare_app (EcMatching.Zipper.cpos (List.length s.s_node))
+    EcPhlSeq.t_ehoare_seq (EcMatching.Zipper.cpos (List.length s.s_node))
      (map_ss_inv2 (fun wppre f -> f_app_simpl f [wppre] txreal) wppre f) tc in
   let tcenv = FApi.t_swap_goals 0 1 tcenv in
   let t_call =
diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml
index 8466ac935..461f570e2 100644
--- a/src/phl/ecPhlEqobs.ml
+++ b/src/phl/ecPhlEqobs.ml
@@ -476,7 +476,7 @@ let process_eqobs_inS info tc =
       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
-      (EcPhlApp.t_equiv_app (p1, p2) (Mpv2.to_form_ts_inv eqi inv) @+ [
+      (EcPhlSeq.t_equiv_seq (p1, p2) (Mpv2.to_form_ts_inv eqi inv) @+ [
         t_id;
         fun tc ->
           FApi.t_last
diff --git a/src/phl/ecPhlExists.ml b/src/phl/ecPhlExists.ml
index 70776aceb..dcc36981d 100644
--- a/src/phl/ecPhlExists.ml
+++ b/src/phl/ecPhlExists.ml
@@ -153,16 +153,16 @@ let process_ecall oside (l, tvi, fs) tc =
   let t_local_seq p1 tc =
     match kind, oside, p1 with
     | `Hoare n, _, Inv_ss p1 ->
-        EcPhlApp.t_hoare_app
+        EcPhlSeq.t_hoare_seq
           (Zpr.cpos (n-1)) p1 tc
     | `Equiv (n1, n2), None, Inv_ts p1 ->
-        EcPhlApp.t_equiv_app
+        EcPhlSeq.t_equiv_seq
           (Zpr.cpos (n1-1), Zpr.cpos (n2-1)) p1 tc
     | `Equiv (n1, n2), Some `Left, Inv_ts p1 ->
-        EcPhlApp.t_equiv_app
+        EcPhlSeq.t_equiv_seq
           (Zpr.cpos (n1-1), Zpr.cpos n2) p1 tc
     | `Equiv(n1, n2), Some `Right, Inv_ts p1 ->
-        EcPhlApp.t_equiv_app
+        EcPhlSeq.t_equiv_seq
           (Zpr.cpos n1, Zpr.cpos (n2-1)) p1 tc
     | _ -> tc_error !!tc "mismatched sidedness or kind of conclusion"
   in
diff --git a/src/phl/ecPhlHiAuto.ml b/src/phl/ecPhlHiAuto.ml
index c74f27ce3..c5c23d645 100644
--- a/src/phl/ecPhlHiAuto.ml
+++ b/src/phl/ecPhlHiAuto.ml
@@ -68,7 +68,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc =
 
   | LL_JUMP ->
       let m = EcIdent.create "&hr" in
-        ( EcPhlApp.t_bdhoare_app
+        ( EcPhlSeq.t_bdhoare_seq
            (Zpr.cpos (-1)) ({m;inv=f_true}, {m;inv=f_true}, 
             {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1})
 
@@ -86,7 +86,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc =
         @+ [apply_ll_strategy lls1; apply_ll_strategy lls2]
       in
 
-        ( EcPhlApp.t_bdhoare_app
+        ( EcPhlSeq.t_bdhoare_seq
            (Zpr.cpos (-1)) ({m;inv=f_true}, {m;inv=f_true}, {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1})
 
         @~ FApi.t_onalli (function
@@ -142,8 +142,8 @@ let t_lossless tc =
 
   | FequivS hs ->
     let ml, mr = fst hs.es_ml, fst hs.es_mr in
-      ((EcPhlApp.t_equiv_app_onesided `Left (EcMatching.Zipper.cpos 0) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+
-         [ (EcPhlApp.t_equiv_app_onesided `Right (EcMatching.Zipper.cpos 0) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+
+      ((EcPhlSeq.t_equiv_seq_onesided `Left (EcMatching.Zipper.cpos 0) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+
+         [ (EcPhlSeq.t_equiv_seq_onesided `Right (EcMatching.Zipper.cpos 0) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+
              [ EcPhlSkip.t_skip @! t_trivial ;
                t_single
              ];
diff --git a/src/phl/ecPhlHiCond.ml b/src/phl/ecPhlHiCond.ml
index 89225fb4d..5c0e6921d 100644
--- a/src/phl/ecPhlHiCond.ml
+++ b/src/phl/ecPhlHiCond.ml
@@ -26,7 +26,7 @@ let process_cond (info : EcParsetree.pcond_info) tc =
     let i2 = Option.map (fun i2 -> EcLowPhlGoal.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)
+    FApi.t_seqsub (EcPhlSeq.t_equiv_seq (n1, n2) f)
       [ t_id; t_equiv_cond side ] tc
 
   | `SeqOne (s, i, f1, f2) ->
@@ -36,7 +36,7 @@ let process_cond (info : EcParsetree.pcond_info) tc =
     let _, f1 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f1 in
     let _, f2 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f2 in
     FApi.t_seqsub
-      (EcPhlApp.t_equiv_app_onesided s n f1 f2)
+      (EcPhlSeq.t_equiv_seq_onesided s n f1 f2)
       [ t_id; t_bdhoare_cond] tc
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml
index 434dece2c..0844ab2f2 100644
--- a/src/phl/ecPhlLoopTx.ml
+++ b/src/phl/ecPhlLoopTx.ml
@@ -320,7 +320,7 @@ let process_unroll_for side cpos tc =
       let (h', pos', z') = oget hds.(i-1) in
       FApi.t_seqs [
         EcPhlWp.t_wp (Some (Single (Zpr.cpos (pos-2))));
-        EcPhlApp.t_hoare_app (Zpr.cpos (pos' - 1)) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+
+        EcPhlSeq.t_hoare_seq (Zpr.cpos (pos' - 1)) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+
         [t_apply_hd h'; t_conseq_nm] ] tc
   in
 
diff --git a/src/phl/ecPhlApp.ml b/src/phl/ecPhlSeq.ml
similarity index 85%
rename from src/phl/ecPhlApp.ml
rename to src/phl/ecPhlSeq.ml
index 2d2ea618b..e829480d0 100644
--- a/src/phl/ecPhlApp.ml
+++ b/src/phl/ecPhlSeq.ml
@@ -14,7 +14,7 @@ open EcLowPhlGoal
 module TTC = EcProofTyping
 
 (* -------------------------------------------------------------------- *)
-let t_hoare_app_r i phi tc =
+let t_hoare_seq_r i phi tc =
   let env = FApi.tc1_env tc in
   let hs = tc1_as_hoareS tc in
   let phi = ss_inv_rebind phi (fst hs.hs_m) in
@@ -23,10 +23,10 @@ let t_hoare_app_r i phi tc =
   let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs) in
   FApi.xmutate1 tc `HlApp [a; b]
 
-let t_hoare_app = FApi.t_low2 "hoare-app" t_hoare_app_r
+let t_hoare_seq = FApi.t_low2 "hoare-seq" t_hoare_seq_r
 
 (* -------------------------------------------------------------------- *)
-let t_ehoare_app_r i phi tc =
+let t_ehoare_seq_r i phi tc =
   let env = FApi.tc1_env tc in
   let hs = tc1_as_ehoareS tc in
   let s1, s2 = s_split env i hs.ehs_s in
@@ -35,10 +35,10 @@ let t_ehoare_app_r i phi tc =
   let b = f_eHoareS (snd hs.ehs_m) phi (stmt s2) (ehs_po hs) in
   FApi.xmutate1 tc `HlApp [a; b]
 
-let t_ehoare_app = FApi.t_low2 "hoare-app" t_ehoare_app_r
+let t_ehoare_seq = FApi.t_low2 "hoare-seq" t_ehoare_seq_r
 
 (* -------------------------------------------------------------------- *)
-let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc =
+let t_bdhoare_seq_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 m = fst bhs.bhs_m in
@@ -93,7 +93,7 @@ let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc =
   FApi.xmutate1 tc `HlApp conds
 
 (* -------------------------------------------------------------------- *)
-let t_bdhoare_app_r i info tc =
+let t_bdhoare_seq_r i info tc =
   let tactic tc =
     let hs  = tc1_as_hoareS tc in
     let tt1 = EcPhlConseq.t_hoareS_conseq_nm (hs_pr hs) {m=(fst hs.hs_m);inv=f_true} in
@@ -103,12 +103,12 @@ let t_bdhoare_app_r i info tc =
 
   FApi.t_last
     (FApi.t_try (t_intros_s_seq (`Symbol ["_"; "_"]) tactic))
-    (t_bdhoare_app_r_low i info tc)
+    (t_bdhoare_seq_r_low i info tc)
 
-let t_bdhoare_app = FApi.t_low2 "bdhoare-app" t_bdhoare_app_r
+let t_bdhoare_seq = FApi.t_low2 "bdhoare-seq" t_bdhoare_seq_r
 
 (* -------------------------------------------------------------------- *)
-let t_equiv_app (i, j) phi tc =
+let t_equiv_seq (i, j) phi tc =
   let env = FApi.tc1_env tc in
   let es = tc1_as_equivS tc in
   let sl1,sl2 = s_split env i es.es_sl in
@@ -119,7 +119,7 @@ let t_equiv_app (i, j) phi tc =
 
   FApi.xmutate1 tc `HlApp [a; b]
 
-let t_equiv_app_onesided side i pre post tc =
+let t_equiv_seq_onesided side i pre post tc =
   let env = FApi.tc1_env tc in
   let es = tc1_as_equivS tc in
   let (ml, mr) = fst es.es_ml, fst es.es_mr in
@@ -143,7 +143,7 @@ let t_equiv_app_onesided side i pre post tc =
 
   let modi = EcPV.s_write env (EcModules.stmt s2) in
   let r = map_ts_inv2 f_and p' (generalize_mod_side env modi (map_ts_inv2 f_imp q' (es_po es))) in
-  FApi.t_seqsub (t_equiv_app ij r)
+  FApi.t_seqsub (t_equiv_seq ij r)
     [t_id; (* s1 ~ s' : pr ==> r *)
      FApi.t_seqsub (EcPhlConseq.t_equivS_conseq_nm p' q')
        [(* r => forall mod, post => post' *) t_trivial;
@@ -153,31 +153,23 @@ let t_equiv_app_onesided side i pre post tc =
     ] tc
 
 (* -------------------------------------------------------------------- *)
-let process_phl_bd_info dir bd_info tc =
+let process_phl_bd_info bd_info tc =
   match bd_info with
-  | PAppNone ->
+  | PSeqNone ->
       let hs = tc1_as_bdhoareS tc in
       let m = fst hs.bhs_m in
-      let f1, f2 =
-         match dir with
-        | Backs -> bhs_bd hs, {m;inv=f_r1}
-        | Fwds  -> {m;inv=f_r1}, bhs_bd hs
-      in
+      let f1, f2 = bhs_bd hs, {m;inv=f_r1} in
         (* The last argument will not be used *)
         ({m;inv=f_true}, f1, f2, {m;inv=f_r0}, {m;inv=f_r1})
 
-  | PAppSingle f ->
+  | PSeqSingle f ->
       let hs = tc1_as_bdhoareS tc in
       let m = fst hs.bhs_m in
       let f  = snd (TTC.tc1_process_Xhl_form tc treal f) in
-      let f1, f2 =
-        match dir with
-        | Backs  -> (map_ss_inv2 f_real_div (bhs_bd hs) f, f)
-        | Fwds   -> (f, map_ss_inv2 f_real_div (bhs_bd hs) f)
-      in
+      let f1, f2 = (map_ss_inv2 f_real_div (bhs_bd hs) f, f) in
         ({m;inv=f_true}, f1, f2, {m;inv=f_r0}, {m;inv=f_r1})
 
-  | PAppMult (phi, f1, f2, g1, g2) ->
+  | PSeqMult (phi, f1, f2, g1, g2) ->
     let hs = tc1_as_bdhoareS tc in
     let m = fst hs.bhs_m in
       let phi =
@@ -212,7 +204,7 @@ let process_phl_bd_info dir bd_info tc =
       (phi, f1, f2, g1, g2)
 
 (* -------------------------------------------------------------------- *)
-let process_app (side, dir, k, phi, bd_info) tc =
+let process_seq ((side, k, phi, bd_info) : seq_info) (tc : tcenv1) =
   let concl = FApi.tc1_goal tc in
 
   let get_single phi =
@@ -225,19 +217,19 @@ let process_app (side, dir, k, phi, bd_info) tc =
       tc_error !!tc "seq: no side information expected" in
 
   match k, bd_info with
-  | Single i, PAppNone when is_hoareS concl ->
+  | Single i, PSeqNone when is_hoareS concl ->
     check_side side;
     let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in
     let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in
-    t_hoare_app i phi tc
+    t_hoare_seq i phi tc
 
-  | Single i, PAppNone when is_eHoareS concl ->
+  | Single i, PSeqNone when is_eHoareS concl ->
     check_side side;
     let _, phi = TTC.tc1_process_Xhl_formula_xreal tc (get_single phi) in
     let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in
-    t_ehoare_app i phi tc
+    t_ehoare_seq i phi tc
 
-  | Single i, PAppNone when is_equivS concl ->
+  | Single i, PSeqNone when is_equivS concl ->
     let pre, post =
       match phi with
       | Single _ -> tc_error !!tc "seq onsided: a pre and a post is expected"
@@ -250,24 +242,24 @@ let process_app (side, dir, k, phi, bd_info) tc =
       | None -> tc_error !!tc "seq onsided: side information expected"
       | Some side -> side in
     let i = EcLowPhlGoal.tc1_process_codepos1 tc (Some side, i) in
-    t_equiv_app_onesided side i pre post tc
+    t_equiv_seq_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 (ra, f1, f2, f3, f4) = process_phl_bd_info bd_info tc in
       let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in
-      t_bdhoare_app i (ra, pia, f1, f2, f3, f4) tc
+      t_bdhoare_seq i (ra, pia, f1, f2, f3, f4) tc
 
-  | Double (i, j), PAppNone when is_equivS concl ->
+  | Double (i, j), PSeqNone when is_equivS concl ->
       check_side side;
       let phi = TTC.tc1_process_prhl_formula tc (get_single phi) in
       let i = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left, i) in
       let j = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left, j) in
-      t_equiv_app (i, j) phi tc
+      t_equiv_seq (i, j) phi tc
 
-  | Single _, PAppNone
-  | Double _, PAppNone ->
+  | Single _, PSeqNone
+  | Double _, PSeqNone ->
       tc_error !!tc "invalid `position' parameter"
 
   | _, _ ->
diff --git a/src/phl/ecPhlApp.mli b/src/phl/ecPhlSeq.mli
similarity index 50%
rename from src/phl/ecPhlApp.mli
rename to src/phl/ecPhlSeq.mli
index 41d089476..b5b905ad5 100644
--- a/src/phl/ecPhlApp.mli
+++ b/src/phl/ecPhlSeq.mli
@@ -6,11 +6,11 @@ open EcMatching.Position
 open EcAst
 
 (* -------------------------------------------------------------------- *)
-val t_hoare_app   : codepos1 -> ss_inv -> backward
-val t_ehoare_app  : codepos1 -> ss_inv -> backward
-val t_bdhoare_app : codepos1 -> ss_inv tuple6 -> backward
-val t_equiv_app   : codepos1 pair -> ts_inv -> backward
-val t_equiv_app_onesided : side -> codepos1 -> ss_inv -> ss_inv -> backward
+val t_hoare_seq   : codepos1 -> ss_inv -> backward
+val t_ehoare_seq  : codepos1 -> ss_inv -> backward
+val t_bdhoare_seq : codepos1 -> ss_inv tuple6 -> backward
+val t_equiv_seq   : codepos1 pair -> ts_inv -> backward
+val t_equiv_seq_onesided : side -> codepos1 -> ss_inv -> ss_inv -> backward
 
 (* -------------------------------------------------------------------- *)
-val process_app : app_info -> backward
+val process_seq : seq_info -> backward
diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml
index c54b43ea4..1d1136c94 100644
--- a/src/phl/ecPhlWhile.ml
+++ b/src/phl/ecPhlWhile.ml
@@ -108,7 +108,7 @@ let t_ehoare_while inv tc =
   let m = EcMemory.memory hs.ehs_m in
   let e = ss_inv_of_expr m e in
   let tc =
-    FApi.t_rotate `Left 1 (EcPhlApp.t_ehoare_app (0, `ByPos (List.length hs.ehs_s.s_node - 1)) inv tc) in
+    FApi.t_rotate `Left 1 (EcPhlSeq.t_ehoare_seq (0, `ByPos (List.length hs.ehs_s.s_node - 1)) inv tc) in
   FApi.t_sub
     [(EcPhlConseq.t_ehoareS_conseq inv (map_ss_inv2 f_interp_ehoare_form (map_ss_inv1 f_not e) inv)) @+
        [t_trivial;