diff --git a/examples/tactics/inline.ec b/examples/tactics/inline.ec
new file mode 100644
index 0000000000..3f6c544a7a
--- /dev/null
+++ b/examples/tactics/inline.ec
@@ -0,0 +1,128 @@
+module F = {
+  proc f () = {
+    var r;
+
+    r <- 0;
+  }
+
+  proc g () = {
+    var s;
+
+    s <- 1;
+  }
+}.
+
+module G = {
+  proc f () = {
+    var t;
+
+    F.g();
+    t <- 2;
+  }
+
+  proc g () = {
+    var u;
+
+    F.f();
+    u <- 3;
+  }
+}.
+
+module Game = {
+  proc main () = {
+    F.f();
+    G.g();
+    F.g();
+    G.f();
+  }
+}.
+
+equiv inline_full_procedures : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline F.f G.g.
+admitted.
+
+equiv inline_star : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline *.
+admitted.
+
+equiv inline_blank : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline.
+admitted.
+
+equiv inline_module : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline F.
+admitted.
+
+equiv inline_procedure : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline f.
+admitted.
+
+equiv inline_minus_full_procedure : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline * - F.f.
+admitted.
+
+equiv inline_minus_procedure : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline * - f.
+admitted.
+
+equiv inline_minus_module : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline * - F.
+admitted.
+
+equiv inline_minuses : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline * - F - g.
+admitted.
+
+equiv inline_add_back : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline * - F F.
+admitted.
+
+equiv inline_remove_back : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline F - F.
+admitted.
+
+equiv inline_side : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline{1} *.
+admitted.
+
+equiv inline_occs : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline{1} (1 4).
+admitted.
+
+equiv inline_occs_pat : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline{1} (1 2) * - G.
+admitted.
+
+equiv inline_codepos : Game.main ~ Game.main : true ==> true.
+proof.
+proc.
+inline {1} 3.
+admitted.
diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml
index 5ef64cb1a5..47197a2a92 100644
--- a/src/ecHiGoal.ml
+++ b/src/ecHiGoal.ml
@@ -1034,7 +1034,7 @@ let process_rewrite1_r ttenv ?target ri tc =
       let tc =
         t_onselect
           p
-          (t_seq (EcPhlInline.process_inline (`All (None, None))) ((t_try (t_seq EcPhlAuto.t_auto process_done))))
+          (t_seq (EcPhlInline.process_inline (`ByName (None, None, ([], None)))) ((t_try (t_seq EcPhlAuto.t_auto process_done))))
           tc
       in
 
diff --git a/src/ecParser.mly b/src/ecParser.mly
index b241feef23..667ad47055 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -797,7 +797,7 @@ mod_ident1:
     { (mk_loc (EcLocation.make $startpos(_l) $endpos(_l))
          EcCoreLib.i_self, None) :: x }
 
-fident:
+%inline fident:
 | nm=mod_qident DOT x=lident { (nm, x) }
 | x=lident { ([], x) }
 
@@ -810,6 +810,26 @@ f_or_mod_ident:
       FM_FunOrVar fv}
 | m=loc(mod_qident) { FM_Mod m }
 
+
+inlinesubpat:
+| m=rlist1(uident, DOT) { m, None }
+| m=rlist1(uident, DOT) DOT f=lident { m, Some f}
+| f=lident { [], Some f}
+
+inlinepat1:
+| nm=loc(mod_qident)  {  `InlinePat(nm, ([], None)) }
+| f=loc(fident) {
+   let f0 = unloc f in
+   if fst f0 = [] then `InlinePat(mk_loc (loc f) [], ([], Some (snd f0)))
+   else `InlineXpath f
+}
+| nm=loc(mod_qident) SLASH sub=inlinesubpat { `InlinePat(nm, sub) }
+| u=loc(UNDERSCORE) SLASH sub=inlinesubpat { `InlinePat(mk_loc (loc u) [], sub) }
+| STAR { `InlineAll }
+
+inlinepat:
+| sign=iboption(MINUS) p=inlinepat1 { (if sign then `DIFF else `UNION), p }
+
 (* -------------------------------------------------------------------- *)
 %inline ordering_op:
 | GT { ">"  }
@@ -3168,15 +3188,15 @@ phltactic:
 | RNDSEM s=side? c=codepos1
     { Prndsem (s, c) }
 
-| INLINE s=side? u=inlineopt? o=occurences? f=plist1(loc(fident), empty)
-    { Pinline (`ByName (s, u, (f, o))) }
+| INLINE s=side? u=inlineopt? o=occurences?
+  { Pinline (`ByName(s, u, ([], o))) }
+
+| INLINE s=side? u=inlineopt? o=occurences? f1=inlinepat1 f=plist0(inlinepat, empty)
+  { Pinline (`ByName(s, u, ((`UNION, f1)::f, o))) }
 
 | INLINE s=side? u=inlineopt? p=codepos
     { Pinline (`CodePos (s, u, p)) }
 
-| INLINE s=side? u=inlineopt? STAR
-    { Pinline (`All (s, u)) }
-
 | KILL s=side? o=codepos
     { Pkill (s, o, Some 1) }
 
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 9bf58b3ef1..60d3bbbe4c 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -659,10 +659,19 @@ type async_while_info = {
 (* -------------------------------------------------------------------- *)
 type inlineopt = [`UseTuple of bool] option
 
+type inline_pat1 = [
+  | `InlineXpath of pgamepath
+  | `InlinePat of pmsymbol located * (psymbol list * psymbol option)
+  | `InlineAll
+]
+
+
+type inline_pat = ([ `DIFF | `UNION] * inline_pat1) list
+
 type inline_info = [
-  | `ByName    of oside * inlineopt * (pgamepath list * int list option)
+  | `ByName    of oside * inlineopt * (inline_pat * int list option)
   | `CodePos   of (oside * inlineopt * codepos)
-  | `All       of oside * inlineopt
+ (* | `All       of oside * inlineopt *)
 ]
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/phl/ecPhlInline.ml b/src/phl/ecPhlInline.ml
index e16f57296c..6806474a8f 100644
--- a/src/phl/ecPhlInline.ml
+++ b/src/phl/ecPhlInline.ml
@@ -2,6 +2,8 @@
 open EcParsetree
 open EcUtils
 open EcMaps
+open EcLocation
+open EcPath
 open EcTypes
 open EcModules
 open EcFol
@@ -216,19 +218,9 @@ let t_inline_equiv ~use_tuple =
 (* -------------------------------------------------------------------- *)
 module HiInternal = struct
   (* ------------------------------------------------------------------ *)
-  let pat_all env fs s =
-    let test f =
-      let is_defined = function FBdef _ -> true | _ -> false in
-
-      match fs with
-      | Some fs -> EcPath.Sx.mem (EcEnv.NormMp.norm_xfun env f) fs
-      | None    ->
-          let f = EcEnv.NormMp.norm_xfun env f in
-          let f = EcEnv.Fun.by_xpath f env in
-          is_defined f.f_def
-    in
+  let pat_all cond s =
 
-    let test = EcPath.Hx.memo 0 test in
+    let test = EcPath.Hx.memo 0 cond in
 
     let rec aux_i i =
       match i.i_node with
@@ -334,62 +326,57 @@ module HiInternal = struct
 end
 
 (* -------------------------------------------------------------------- *)
-let rec process_inline_all ~use_tuple side fs tc =
-  let env, _, concl = FApi.tc1_eflat tc in
+let rec process_inline_all ~use_tuple side cond tc =
+  let concl = FApi.tc1_goal tc in
 
   match concl.f_node, side with
   | FequivS _, None ->
       FApi.t_seq
-        (process_inline_all ~use_tuple (Some `Left ) fs)
-        (process_inline_all ~use_tuple (Some `Right) fs)
+        (process_inline_all ~use_tuple (Some `Left ) cond)
+        (process_inline_all ~use_tuple (Some `Right) cond)
         tc
 
   | FequivS es, Some b -> begin
       let st = sideif b es.es_sl es.es_sr in
-      match HiInternal.pat_all env fs st with
+      match HiInternal.pat_all cond st with
       | [] -> t_id tc
       | sp -> FApi.t_seq
                 (t_inline_equiv ~use_tuple b sp)
-                (process_inline_all ~use_tuple  side fs)
+                (process_inline_all ~use_tuple  side cond)
                 tc
   end
 
   | FhoareS hs, None -> begin
-      match HiInternal.pat_all env fs hs.hs_s with
+      match HiInternal.pat_all cond hs.hs_s with
       | [] -> t_id tc
       | sp -> FApi.t_seq
                 (t_inline_hoare ~use_tuple sp)
-                (process_inline_all ~use_tuple side fs)
+                (process_inline_all ~use_tuple side cond)
                 tc
   end
 
   | FcHoareS chs, None -> begin
-    match HiInternal.pat_all env fs chs.chs_s with
+    match HiInternal.pat_all cond chs.chs_s with
       | [] -> t_id tc
       | sp -> FApi.t_seq
                 (t_inline_choare ~use_tuple sp)
-                (process_inline_all ~use_tuple side fs)
+                (process_inline_all ~use_tuple side cond)
                 tc
    end
 
   | FbdHoareS bhs, None -> begin
-      match HiInternal.pat_all env fs bhs.bhs_s with
+      match HiInternal.pat_all cond bhs.bhs_s with
       | [] -> t_id tc
       | sp -> FApi.t_seq
                 (t_inline_bdhoare ~use_tuple sp)
-                (process_inline_all ~use_tuple side fs)
+                (process_inline_all ~use_tuple side cond)
                 tc
   end
 
   | _, _ -> tc_error !!tc "invalid arguments"
 
 (* -------------------------------------------------------------------- *)
-let process_inline_occs ~use_tuple side fs occs tc =
-  let env = FApi.tc1_env tc in
-  let cond =
-    if   EcPath.Sx.is_empty fs
-    then fun _ -> true
-    else fun f -> EcPath.Sx.mem (EcEnv.NormMp.norm_xfun env f) fs in
+let process_inline_occs ~use_tuple side cond occs tc =
   let occs  = Sint.of_list occs in
   let concl = FApi.tc1_goal tc in
 
@@ -441,27 +428,86 @@ let process_inline_codepos ~use_tuple side pos tc =
   with EcMatching.Zipper.InvalidCPos ->
     tc_error !!tc "invalid position"
 
+(* -------------------------------------------------------------------- *)
+let process_info tc infos =
+  let env = FApi.tc1_env tc in
+  let doit (dir, pat) =
+    let pat =
+      match pat with
+      | `InlineXpath f ->
+        let f = EcTyping.trans_gamepath env f in
+        `InlineXpath (EcEnv.NormMp.norm_xfun env f)
+      | `InlinePat (pm, (sub, f)) ->
+        let pm =
+          List.rev_map (fun (p, o) ->
+            if o <> None then tc_error !!tc ~loc:(loc p) "can not provide functor arguments";
+            unloc p) (unloc pm) in
+        let sub = List.rev_map unloc sub in
+        let f = omap unloc f in
+        `InlinePat(pm, sub, f)
+      | `InlineAll -> `InlineAll in
+     (dir, pat) in
+  List.map doit infos
+
+
+(* -------------------------------------------------------------------- *)
+let test_match pm sub fx f =
+
+  let rec test_path ids p =
+    match ids, p.p_node with
+    | [], _ -> true
+    | [id], EcPath.Psymbol id' -> EcSymbols.sym_equal id id'
+    | id::ids, EcPath.Pqname(p, id') -> EcSymbols.sym_equal id id' && test_path ids p
+    | _, _ -> false
+    in
+
+  begin match fx with None -> true | Some sym -> EcSymbols.sym_equal sym f.x_sub end
+  && match f.x_top.m_top with
+  | `Local a ->
+    sub = [] &&
+    begin match pm with
+    | [] -> true
+    | [id] -> EcSymbols.sym_equal id (EcIdent.name a)
+    | _ -> false
+    end
+
+  | `Concrete (p, sp) -> ofold (fun sp b -> b && test_path sub sp) (test_path pm p) sp
+
+
+let test_pat for_occ env infos f =
+  let fn = EcEnv.NormMp.norm_xfun env f in
+
+  let test_pat1 all pat =
+    match pat with
+    | `InlineXpath fn' -> EcPath.x_equal fn fn'
+    | `InlinePat (pm, sub, fx) -> test_match pm sub fx f
+    | `InlineAll ->
+      all ||
+      match (EcEnv.Fun.by_xpath fn env).f_def with
+      | FBdef _ -> true | _ -> false in
+
+  let rec aux b infos =
+    match infos with
+    | [] -> b
+    | (`UNION, pat) :: infos -> aux (b || test_pat1 for_occ pat) infos
+    | (`DIFF, pat) :: infos -> aux (b && not(test_pat1 true pat)) infos in
+
+  aux false infos
+
 (* -------------------------------------------------------------------- *)
 let process_inline infos tc =
   let use_tuple use =
     odfl true (omap (function `UseTuple b -> b) use) in
-
   match infos with
-  | `ByName (side, use, (fs, occs)) -> begin
-      let env = FApi.tc1_env tc in
-      let use_tuple = use_tuple use in
-      let fs  =
-        List.fold_left (fun fs f ->
-          let f = EcTyping.trans_gamepath env f in
-            EcPath.Sx.add (EcEnv.NormMp.norm_xfun env f) fs)
-          EcPath.Sx.empty fs
-      in
-        match occs with
-        | None      -> process_inline_all ~use_tuple side (Some fs) tc
-        | Some occs -> process_inline_occs ~use_tuple side fs occs tc
+  | `ByName (side, use, (infos, occs)) ->
+    let infos = process_info tc infos in
+    let infos = if infos = [] then [`UNION, `InlineAll] else infos in
+    let env = FApi.tc1_env tc in
+    let use_tuple = use_tuple use in
+    begin match occs with
+    | None      -> process_inline_all ~use_tuple side (test_pat false env infos) tc
+    | Some occs -> process_inline_occs ~use_tuple side (test_pat true env infos) occs tc
     end
 
   | `CodePos (side, use, pos) ->
-       process_inline_codepos ~use_tuple:(use_tuple use) side pos tc
-
-  | `All (side, use) -> process_inline_all ~use_tuple:(use_tuple use) side None tc
+    process_inline_codepos ~use_tuple:(use_tuple use) side pos tc