diff --git a/src/ecCoreModules.ml b/src/ecCoreModules.ml
index 285569cdda..1ecb5ed356 100644
--- a/src/ecCoreModules.ml
+++ b/src/ecCoreModules.ml
@@ -43,6 +43,14 @@ let name_of_lv lv =
   | LvTuple pvs ->
      String.concat "_" (List.map (EcTypes.name_of_pvar |- fst) pvs)
 
+let lv_of_expr e =
+  match e.e_node with
+  | Evar pv ->
+     LvVar (pv, e_ty e)
+  | Etuple pvs ->
+     LvTuple (List.map (fun e -> EcTypes.destr_var e, e_ty e) pvs)
+  | _ -> failwith "failed to construct lv from expr"
+
 (* -------------------------------------------------------------------- *)
 type instr = EcAst.instr
 
diff --git a/src/ecCoreModules.mli b/src/ecCoreModules.mli
index 71a8eec3b7..961a482c16 100644
--- a/src/ecCoreModules.mli
+++ b/src/ecCoreModules.mli
@@ -12,6 +12,7 @@ val ty_of_lv     : lvalue -> EcTypes.ty
 val lv_of_list   : (prog_var * ty) list -> lvalue option
 val lv_to_list   : lvalue -> prog_var list
 val name_of_lv   : lvalue -> string
+val lv_of_expr   : expr -> lvalue
 
 (* --------------------------------------------------------------------- *)
 type instr = EcAst.instr
diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml
index 6272daaa2e..d50432deba 100644
--- a/src/ecHiTacticals.ml
+++ b/src/ecHiTacticals.ml
@@ -189,6 +189,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pcallconcave info         -> EcPhlCall.process_call_concave info
     | Pswap sw                  -> EcPhlSwap.process_swap sw
     | Pinline info              -> EcPhlInline.process_inline info
+    | Poutline info             -> EcPhlOutline.process_outline info
     | Pinterleave info          -> EcPhlSwap.process_interleave info
     | Pcfold info               -> EcPhlCodeTx.process_cfold info
     | Pkill info                -> EcPhlCodeTx.process_kill info
diff --git a/src/ecLexer.mll b/src/ecLexer.mll
index 82bb7ea451..e5917ee403 100644
--- a/src/ecLexer.mll
+++ b/src/ecLexer.mll
@@ -154,6 +154,7 @@
     "conseq"      , CONSEQ     ;        (* KW: tactic *)
     "exfalso"     , EXFALSO    ;        (* KW: tactic *)
     "inline"      , INLINE     ;        (* KW: tactic *)
+    "outline"     , OUTLINE    ;        (* KW: tactic *)
     "interleave"  , INTERLEAVE ;        (* KW: tactic *)
     "alias"       , ALIAS      ;        (* KW: tactic *)
     "weakmem"     , WEAKMEM    ;        (* KW: tactic *)
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 80893a255c..dfac80454d 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -512,6 +512,7 @@
 %token NOTATION
 %token OF
 %token OP
+%token OUTLINE
 %token PCENT
 %token PHOARE
 %token PIPE
@@ -3129,6 +3130,10 @@ interleave_info:
 | s=side? c1=interleavepos c2=interleavepos c3=interleavepos* k=word
    { (s, c1, c2 :: c3, k) }
 
+%inline outline_kind:
+| s=brace(stmt) { OKstmt(s) }
+| r=sexpr? LEAT f=loc(fident) { OKproc(f, r) }
+
 phltactic:
 | PROC
    { Pfun `Def }
@@ -3219,6 +3224,14 @@ phltactic:
 | INLINE s=side? u=inlineopt? p=codepos
     { Pinline (`CodePos (s, u, p)) }
 
+| OUTLINE s=side LBRACKET st=codepos1 e=option(MINUS e=codepos1 {e}) RBRACKET k=outline_kind
+    { Poutline {
+	  outline_side  = s; 
+	  outline_start = st; 
+	  outline_end   = odfl st e; 
+	  outline_kind  = k }
+    }
+
 | KILL s=side? o=codepos
     { Pkill (s, o, Some 1) }
 
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 5c754039c4..02e6bf7a3a 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -670,6 +670,18 @@ type inline_info = [
  (* | `All       of oside * inlineopt *)
 ]
 
+(* -------------------------------------------------------------------- *)
+type outline_kind =
+  | OKstmt of pstmt
+  | OKproc of pgamepath * pexpr option
+
+type outline_info = {
+    outline_side: side;
+    outline_start: codepos1;
+    outline_end: codepos1;
+    outline_kind: outline_kind;
+}
+
 (* -------------------------------------------------------------------- *)
 type fel_info = {
   pfel_cntr  : pformula;
@@ -731,6 +743,7 @@ type phltactic =
   | Pswap          of ((oside * swap_kind) located list)
   | Pcfold         of (oside * codepos * int option)
   | Pinline        of inline_info
+  | Poutline       of outline_info
   | Pinterleave    of interleave_info located
   | Pkill          of (oside * codepos * int option)
   | Prnd           of oside * semrndpos option * rnd_tac_info_f
diff --git a/src/ecUnifyProc.ml b/src/ecUnifyProc.ml
new file mode 100644
index 0000000000..836aabc656
--- /dev/null
+++ b/src/ecUnifyProc.ml
@@ -0,0 +1,115 @@
+open EcAst
+open EcTypes
+open EcModules
+open EcSymbols
+
+(*---------------------------------------------------------------------------------------*)
+type u_error =
+  | UE_InvalidRetInstr
+  | UE_UnexpectedReturn
+  | UE_ExprNotInLockstep of expr * expr
+  | UE_InstrNotInLockstep of instr * instr
+  | UE_DifferentProgramLengths of stmt * stmt
+
+exception UnificationError of u_error
+
+(*---------------------------------------------------------------------------------------*)
+type u_value =
+  | Empty
+  | Fixed of expr
+ 
+type umap = u_value Msym.t
+
+(*---------------------------------------------------------------------------------------*)
+let rec unify_exprs umap e1 e2 =
+  match e1.e_node, e2.e_node with
+  | Eint _, Eint _ -> umap
+  | Elocal _, Elocal _ -> umap
+  | Evar pv, e2n ->
+     let var = symbol_of_pv pv in
+
+     (* Only update a value if it hasn't been fixed previously *)
+     let update value =
+       match value with
+       | None ->
+          begin
+            match e2n with
+            | Evar _ -> None
+            | _ -> raise (UnificationError (UE_ExprNotInLockstep (e1, e2)))
+          end
+       | Some Empty -> Some (Fixed e2)
+       | _ -> value
+     in
+
+     Msym.change update var umap
+  | Eop _, Eop _ -> umap
+  | Eapp (f1, a1), Eapp (f2, a2) ->
+     let umap = unify_exprs umap f1 f2 in
+     List.fold_left (fun umap (e1, e2) -> unify_exprs umap e1 e2) umap (List.combine a1 a2)
+  | Equant (_, _, e1), Equant (_, _, e2) ->
+     unify_exprs umap e1 e2
+  | Elet (_, e1, u1), Elet (_, e2, u2) ->
+     let umap = unify_exprs umap e1 e2 in
+     unify_exprs umap u1 u2
+  | Etuple t1, Etuple t2 ->
+     List.fold_left (fun umap (e1, e2) -> unify_exprs umap e1 e2) umap (List.combine t1 t2)
+  | Eif (c1, t1, f1), Eif (c2, t2, f2) ->
+     let umap = unify_exprs umap c1 c2 in
+     let umap = unify_exprs umap t1 t2 in
+     unify_exprs umap f1 f2
+  | Ematch (c1, p1, _), Ematch (c2, p2, _) ->
+     let umap = unify_exprs umap c1 c2 in
+     List.fold_left (fun umap (e1, e2) -> unify_exprs umap e1 e2) umap (List.combine p1 p2)
+  | Eproj (e1, _), Eproj (e2, _) ->
+     unify_exprs umap e1 e2
+  | _ -> raise (UnificationError (UE_ExprNotInLockstep (e1, e2)))
+
+(*---------------------------------------------------------------------------------------*)
+let rec unify_instrs umap i1 i2 =
+ match i1.i_node, i2.i_node with
+  | Sasgn(_, e1), Sasgn(_, e2)
+  | Srnd(_, e1), Srnd(_, e2) ->
+     unify_exprs umap e1 e2
+  | Scall(_, _, args1), Scall(_, _, args2) ->
+     List.fold_left (fun umap (e1, e2) -> unify_exprs umap e1 e2) umap (List.combine args1 args2)
+  | Sif(e1, st1, sf1), Sif(e2, st2, sf2) ->
+     let umap = unify_exprs umap e1 e2 in
+     let umap = unify_stmts umap st1 st2 in
+     unify_stmts umap sf1 sf2
+  | Swhile(e1, s1), Swhile(e2, s2) ->
+     let umap = unify_exprs umap e1 e2 in
+     unify_stmts umap s1 s2
+  | Smatch(e1, bs1), Smatch(e2, bs2) ->
+     let umap = unify_exprs umap e1 e2 in
+     List.fold_left (fun umap (b1, b2) -> unify_stmts umap (snd b1) (snd b2)) umap (List.combine bs1 bs2)
+  | Sassert e1, Sassert e2 ->
+     unify_exprs umap e1 e2
+  | Sabstract _, Sabstract _ -> umap
+  | _ -> raise (UnificationError (UE_InstrNotInLockstep (i1, i2)));
+
+and unify_stmts umap s1 s2 =
+  let s1n, s2n = s1.s_node, s2.s_node in
+  if List.length s1n <> List.length s2n then
+    raise (UnificationError (UE_DifferentProgramLengths (s1, s2)));
+  List.fold_left (fun umap (i1, i2) -> unify_instrs umap i1 i2) umap (List.combine s1n s2n)
+
+(*---------------------------------------------------------------------------------------*)
+(* Given a function definition attempt to unify its body with the statements `sb` 
+   and if a return statement is given, also unify it's expression. *)
+let unify_func umap fdef sb sr =
+  (* Unify the body *)
+  let umap = unify_stmts umap fdef.f_body sb in
+
+  (* Unify the return stmt (if it exists) and retrieve its lv *)
+  match sr with
+  | Some i -> begin
+      (* Check that there is a return expression to unify with *)
+      if fdef.f_ret = None then
+        raise (UnificationError UE_UnexpectedReturn);
+
+      (* Only unify with assignment instructions *)
+      match i.i_node with
+      | Sasgn (lv, e) -> Some lv, unify_exprs umap (Option.get fdef.f_ret) e
+      | _ -> raise (UnificationError UE_InvalidRetInstr)
+  end
+  | _ -> None, umap
diff --git a/src/ecUnifyProc.mli b/src/ecUnifyProc.mli
new file mode 100644
index 0000000000..38b60a2754
--- /dev/null
+++ b/src/ecUnifyProc.mli
@@ -0,0 +1,43 @@
+open EcTypes
+open EcModules
+open EcSymbols
+
+(*---------------------------------------------------------------------------------------*)
+(* `Unification` of procedures *)
+(*
+  Given: r <@ foo(a1: t1, a2: t2, ...); and s1; s2; ...; sr.
+  Attempt to find values for a1, a2, ... such that, the body of `foo` with a1, a2, ...
+  replaced will exactly match s1; s2; ..., and that `r <- res` match sr.
+  Where `res` is the return expression of `foo`.
+
+  Currently, this is done by traversing the respective ASTs and when a relevant
+  program variable is encountered on the lhs, use the rhs expression.
+
+  FIXME: This is incredibly basic and should be iterated on with a more advanced
+  procedure unification algorithm.
+ *)
+
+(*---------------------------------------------------------------------------------------*)
+type u_error =
+  | UE_InvalidRetInstr
+  | UE_UnexpectedReturn
+  | UE_ExprNotInLockstep of expr * expr
+  | UE_InstrNotInLockstep of instr * instr
+  | UE_DifferentProgramLengths of stmt * stmt
+
+exception UnificationError of u_error
+
+(*---------------------------------------------------------------------------------------*)
+type u_value =
+  | Empty
+  | Fixed of expr
+
+type umap = u_value Msym.t
+
+(*---------------------------------------------------------------------------------------*)
+(* The following functions attempt to unify unknown program variables
+   in the lhs with expressions from the rhs *)
+val unify_exprs : umap -> expr -> expr -> umap
+val unify_instrs : umap -> instr -> instr -> umap
+val unify_stmts : umap -> stmt -> stmt -> umap
+val unify_func : umap -> function_def -> stmt -> instr option -> lvalue option * umap
diff --git a/src/phl/ecPhlOutline.ml b/src/phl/ecPhlOutline.ml
new file mode 100644
index 0000000000..3f9f6388ef
--- /dev/null
+++ b/src/phl/ecPhlOutline.ml
@@ -0,0 +1,298 @@
+open EcParsetree
+open EcFol
+open EcUtils
+open EcModules
+open EcTypes
+open EcSymbols
+open EcUnifyProc
+
+open EcCoreGoal
+open EcCoreGoal.FApi
+open EcLowGoal
+open EcLowPhlGoal
+
+(*---------------------------------------------------------------------------------------*)
+(*
+   Transitivity star with (ideally) lossless pre-conditions over the intermediate
+   programs, and automatic discharging of the first two goals.
+*)
+(* FIXME: Move to ecPhlTrans *)
+
+let t_equivS_trans_eq side s tc =
+  let env = tc1_env tc in
+  let es = tc1_as_equivS tc in
+  let c,m = match side with `Left -> es.es_sl, es.es_ml | `Right -> es.es_sr, es.es_mr in
+
+  let mem_pre = split_sided (EcMemory.memory m) es.es_pr in
+  let fv_pr  = EcPV.PV.fv env (EcMemory.memory m) es.es_pr in
+  let fv_po  = EcPV.PV.fv env (fst m) es.es_po in
+  let fv_r = EcPV.s_read env c in
+  let mk_eqs fv =
+    let vfv, gfv = EcPV.PV.elements fv in
+    let veq = List.map (fun (x,ty) -> f_eq (f_pvar x ty mleft) (f_pvar x ty mright)) vfv in
+    let geq = List.map (fun mp -> f_eqglob mp mleft mp mright) gfv in
+    f_ands (veq @ geq) in
+  let pre = mk_eqs (EcPV.PV.union (EcPV.PV.union fv_pr fv_po) fv_r) in
+  let pre = f_and pre (odfl f_true mem_pre) in
+  let post = mk_eqs fv_po in
+  let c1, c2 =
+    if side = `Left then (pre, post), (es.es_pr, es.es_po)
+    else (es.es_pr, es.es_po), (pre, post)
+  in
+
+  let exists_subtac (tc : tcenv1) =
+    (* Ideally these are guaranteed fresh *)
+    let pl = EcIdent.create "&p__1" in
+    let pr = EcIdent.create "&p__2" in
+    let h  = EcIdent.create "__" in
+    let tc = t_intros_i_1 [pl; pr; h] tc in
+    let goal = tc1_goal tc in
+
+    let p = match side with | `Left -> pl | `Right -> pr in
+    let b = match side with | `Left -> true | `Right -> false in
+
+    let handle_exists () =
+      (* Pairing up the correct variables for the exists intro *)
+      let vs, fm = EcFol.destr_exists goal in
+      let eqs_pre, _ =
+        let l, r = EcFol.destr_and fm in
+        if b then l, r else r, l
+      in
+      let eqs, _ = destr_and eqs_pre in
+      let eqs = destr_ands ~deep:false eqs in
+      let doit eq =
+        let l, r = destr_eq eq in
+        let l, r = if b then r, l else l, r in
+        let v = EcFol.destr_local l in
+        v, r
+      in
+      let eqs = List.map doit eqs in
+      let exvs =
+        List.map
+          (fun (id, _) ->
+            let v = List.assoc id eqs in
+            Fsubst.f_subst_mem (EcMemory.memory m) p v)
+          vs
+      in
+
+      as_tcenv1 (t_exists_intro_s (List.map paformula exvs) tc)
+    in
+
+    let tc =
+      if EcFol.is_exists goal then
+        handle_exists ()
+      else
+        tc
+    in
+
+    t_seq
+      (t_generalize_hyp ?clear:(Some `Yes) h)
+      EcHiGoal.process_done
+      tc
+  in
+
+  let tc = t_seqsub
+             (EcPhlTrans.t_equivS_trans (EcMemory.memtype m, s) c1 c2)
+             [exists_subtac; EcHiGoal.process_done; t_id; t_id]
+             tc
+  in
+  tc
+
+(*---------------------------------------------------------------------------------------*)
+(*
+   This is the improved transitivity star from above but allows for a range of code
+   positions to select the program slice that is changing. The prefix and suffix are
+   extracted and copied across to build the new program.
+*)
+(* FIXME: Maybe move to ecPhlTrans as well *)
+
+let t_outline_stmt side start_pos end_pos s tc =
+  let goal = tc1_as_equivS tc in
+
+  (* Check which memory/program we are outlining *)
+  let code = match side with
+    | `Left  -> goal.es_sl
+    | `Right -> goal.es_sr
+  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 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
+
+  (* The middle goal, showing equivalence with the replaced code, ideally solves. *)
+  let tp = match side with | `Left -> 1 | `Right -> 2 in
+  let p = EcHiGoal.process_tfocus tc (Some [Some tp, Some tp], None) in
+  let tc =
+    t_onselect
+      p
+      (t_try (
+           t_seqs [
+               EcPhlInline.process_inline (`ByName (None, None, ([], None)));
+               EcPhlEqobs.process_eqobs_in none {sim_pos = none; sim_hint = ([], none); sim_eqs = none};
+               EcPhlAuto.t_auto;
+               EcHiGoal.process_done;
+         ]))
+      tc
+  in
+  tc
+
+(*---------------------------------------------------------------------------------------*)
+(* The main tactic *)
+
+type out_error =
+  | OE_InvalidFunc
+  | OE_UnnecessaryReturn
+  | OE_UnificationFailure of EcSymbols.symbol
+
+exception OutlineError of out_error
+
+(*
+  `outline` - replace a program slice with a procedure call.
+
+  Arguments,
+    side: selects the program (left or right) that will outlined.
+    start_pos, end_pos: selects the particular slice of the program to outline.
+    fname: path of the function that we are using to outline.
+    res_lv: optional left-value for the result.
+      when None, assume the entire slice contains the body and return.
+      otherwise, assume entire slice contains just the body.
+*)
+let t_outline_proc side start_pos end_pos fname res_lv tc =
+  let env = tc1_env tc in
+  let goal = tc1_as_equivS tc in
+
+  (* Extract the function args, body, and return expression *)
+  let func = EcEnv.Fun.by_xpath fname env in
+  let f_def =
+    match func.f_def with
+    | FBdef d -> d
+    | _ -> raise (OutlineError OE_InvalidFunc)
+  in
+
+  (* Get the code from the side we are outlining *)
+  let code = match side with
+    | `Left  -> goal.es_sl
+    | `Right -> goal.es_sr
+  in
+
+  (* 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 body =
+       if start_pos = end_pos then
+         s_empty
+       else
+         let _, hd, tl  = s_split_i start_pos (stmt rest) in
+         stmt (hd :: tl)
+    in
+
+    match f_def.f_ret, res_lv with
+    | None, None ->
+       s_seq body (stmt [ret_instr]), None
+    | Some _, Some _ ->
+       s_seq body (stmt [ret_instr]), None
+    | Some _, None ->
+       body, Some ret_instr
+    | _, _ -> raise (OutlineError OE_UnnecessaryReturn)
+  in
+
+  (* Get the symbol for each function argument used *)
+  let arg_names = func.f_sig.fs_anames in
+  let args = List.filter_map ov_name arg_names in
+
+  (* Insert all the argument symbols we are attempting to unify *)
+  let umap = List.fold_left (fun umap a -> Msym.add a Empty umap) Msym.empty args in
+
+  (* Unify the function *)
+  let lv, args_map = unify_func umap f_def old_code_body old_code_ret in
+  (* Use the correct lv *)
+  let lv = match lv with | None -> res_lv | _ -> lv in
+
+  (* Check that we were able to unify all arguments *)
+  let args =
+    List.map
+      (fun a ->
+        match Msym.find a args_map with
+        | Empty -> raise (OutlineError (OE_UnificationFailure a))
+        | Fixed e -> e
+      )
+      args
+  in
+
+  (* Buid the call statement *)
+  let proc_call = s_call (lv, fname, args) in
+
+  (* Offload to transitivity *)
+  t_outline_stmt side start_pos end_pos proc_call 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 goal = tc1_as_equivS tc in
+  let ppe = EcPrinting.PPEnv.ofenv env in
+
+  (* Check which memory we are outlining *)
+  let mem = match side with
+    | `Left  -> goal.es_ml
+    | `Right -> goal.es_mr
+  in
+
+  try
+    match info.outline_kind with
+    | OKstmt s ->
+       let s = EcProofTyping.tc1_process_stmt tc (EcMemory.memtype mem) s in
+       t_outline_stmt side start_pos end_pos s tc
+    | OKproc (f, pres_lv) ->
+       let loc = EcLocation.loc f in
+       (* Get the function *)
+       let f = EcTyping.trans_gamepath env f in
+       let func = EcEnv.Fun.by_xpath f env in
+       let f_def =
+         match func.f_def with
+         | FBdef d -> d
+         | _ -> raise (OutlineError OE_InvalidFunc)
+       in
+
+       (* Translate the res_lv if given *)
+       let res_lv =
+         match pres_lv, f_def.f_ret with
+         | Some r, Some e -> begin
+             try
+               let subenv = EcEnv.Memory.push_active mem env in
+               let ue = EcUnify.UniEnv.create (Some []) in
+               let res = EcTyping.transexpcast subenv `InProc ue e.e_ty r in
+               let ts = Tuni.subst (EcUnify.UniEnv.close ue) in
+               let es = e_subst { e_subst_id with es_ty = ts } in
+               Some (lv_of_expr (es res))
+             with EcUnify.UninstanciateUni ->
+               EcTyping.tyerror loc env EcTyping.FreeTypeVariables
+           end
+         | None, _ -> None
+         | _, _ -> raise (OutlineError OE_UnnecessaryReturn)
+       in
+
+       t_outline_proc side start_pos end_pos f res_lv tc
+  with
+  | OutlineError OE_UnnecessaryReturn ->
+     tc_error !!tc "outline: left-value given when function does not return"
+  | OutlineError OE_InvalidFunc ->
+     tc_error !!tc "outline: cannot outline an abstract function"
+  | OutlineError (OE_UnificationFailure x) ->
+     tc_error !!tc "outline: unable to unify `%s`" x
+  | UnificationError UE_InvalidRetInstr ->
+     tc_error !!tc ("outline: return instruction kind not supported")
+  | UnificationError (UE_DifferentProgramLengths (s1, s2)) ->
+     tc_error !!tc "outline: body's are different lengths\n%a ~ %a" (EcPrinting.pp_stmt ppe) s1 (EcPrinting.pp_stmt ppe) s2
+  | UnificationError (UE_InstrNotInLockstep (i1, i2))->
+     tc_error !!tc "outline: instructions not in sync\n%a ~ %a" (EcPrinting.pp_instr ppe) i1 (EcPrinting.pp_instr ppe) i2
+  | UnificationError (UE_ExprNotInLockstep (e1, e2))->
+     tc_error !!tc "outline: expressions not in sync\n%a ~ %a" (EcPrinting.pp_expr ppe) e1 (EcPrinting.pp_expr ppe) e2
diff --git a/src/phl/ecPhlOutline.mli b/src/phl/ecPhlOutline.mli
new file mode 100644
index 0000000000..9994ddac32
--- /dev/null
+++ b/src/phl/ecPhlOutline.mli
@@ -0,0 +1,9 @@
+open EcCoreGoal.FApi
+open EcParsetree
+open EcModules
+open EcPath
+
+val t_outline_stmt : side -> codepos1 -> codepos1 -> stmt -> backward
+val t_outline_proc : side -> codepos1 -> codepos1 -> xpath -> lvalue option -> backward
+
+val process_outline : outline_info -> backward
diff --git a/tests/outline.ec b/tests/outline.ec
new file mode 100644
index 0000000000..0781a49a33
--- /dev/null
+++ b/tests/outline.ec
@@ -0,0 +1,130 @@
+require import AllCore.
+
+op dint : int distr.
+
+module M = {
+  var x : int
+
+  proc f1() : unit = {
+    M.x <- 0;
+  }
+
+  proc f2(a: int) : unit = {
+    M.x <- a;
+  }
+
+  proc f3(a: int, b: int) : int = {
+    return a + b;
+  }
+
+  proc f4(a: int, b: int) : int = {
+    var t;
+    if (a <= b) {
+      t <- b;
+    } else {
+      t <- a;
+    }
+    return t;
+  }
+
+  proc f5(d: int distr) : int = {
+    var v;
+    v <$ d;
+    return v;
+  }
+}.
+
+module N = {
+  proc g1() : unit = {
+    M.f1();
+  }
+
+  proc g2(a) : unit = {
+    M.f2(a);
+  }
+
+  proc g3(a, b) : unit = {
+    var r;
+    r <@ M.f3(a, b);
+  }
+
+  proc g4(a: int, b: int) : unit = {
+    var m;
+    if (a <= b) {
+      m <- b;
+    } else {
+      m <- a;
+    }
+    M.x <- m;
+  }
+
+  proc g5() : unit = {
+    var x;
+    x <$ dint;
+  }
+
+  proc g6() : unit = {
+    var a, b, m;
+    a <$ dint;
+    b <$ dint;
+    if (a <= b) {
+      m <- b;
+    } else {
+      m <- a;
+    }
+    M.x <- m;
+  }
+}.
+
+equiv outline_no_args_no_ret: N.g1 ~ N.g1: true ==> true.
+proc.
+inline {1} 1.
+outline {1} [1] <@ M.f1.
+by sim.
+qed.
+
+equiv outline_no_ret: N.g2 ~ N.g2: true ==> true.
+proc.
+inline {1} 1.
+outline {1} [2] <@ M.f2.
+by inline*; auto.
+qed.
+
+equiv outline_no_body: N.g3 ~ N.g3: true ==> true.
+proc.
+inline {1} 1.
+outline {1} [3] <@ M.f3.
+by inline*; auto.
+qed.
+
+equiv outline_slice: N.g4 ~ N.g4: true ==> true.
+proc.
+outline {1} [1-2] <@ M.f4.
+by inline*; auto.
+qed.
+
+equiv outline_explicit_ret: N.g5 ~ N.g5: true ==> true.
+proc.
+outline {1} [1] x <@ M.f5.
+by inline*; auto.
+qed.
+
+equiv outline_multi: N.g6 ~ N.g6: true ==> true.
+proof.
+proc.
+outline {1} [3-4] <@ N.g4.
+outline {1} [2] b <@ M.f5.
+outline {1} [1] a <@ M.f5.
+by inline*; auto.
+qed.
+
+equiv outline_stmt: N.g6 ~ N.g6: true ==> true.
+proof.
+proc.
+outline {1} [1-4] {
+  a <@ M.f5(dint);
+  b <@ M.f5(dint);
+  N.g4(a,b);
+}.
+by inline*; auto.
+qed.