diff --git a/src/plugins/wp/TacClear.ml b/src/plugins/wp/TacClear.ml
index 48a835f007144110b92cd7dcb35dfd919b4b2f42..3808c2909095b05c7af9415ce7f47e2085947f0c 100644
--- a/src/plugins/wp/TacClear.ml
+++ b/src/plugins/wp/TacClear.ml
@@ -33,10 +33,18 @@ let condition original p = (* keep original kind of simple condition *)
   | _ -> assert false
 
 let tactical_step step =
-  Tactical.replace_single ~at:step.id ("Removed", Conditions.Have Lang.F.p_true)
+  Tactical.replace_single ~at:step.id
+    (* Note: the provided name is used in the GUi for the subgoal title *)
+    ("Removed Step", Conditions.Have Lang.F.p_true)
 
 module TermLset = Qed.Listset.Make(Lang.F.QED.Term)
 
+let pp_filtered fmt t =
+  match Lang.F.repr t with
+  | Qed.Logic.Fun(f,_) -> Format.fprintf fmt "%a(...)" Lang.Fun.pretty f
+  | _ -> Lang.F.pp_term fmt t
+
+
 let tactical_inside step remove =
   let remove = List.sort_uniq Lang.F.compare remove in
   let collect p =
@@ -47,9 +55,13 @@ let tactical_inside step remove =
   begin match step.condition with
     | Type p | Have p | When p | Core p | Init p ->
       let ps = Lang.F.e_props @@ collect p in
-      let ps = TermLset.diff ps remove in
-      let cond = condition step @@ Lang.F.p_bool @@ Lang.F.e_and ps in
-      Tactical.replace_single ~at:step.id ("Filtered", cond)
+      let kept = TermLset.diff ps remove in
+      let feedback =
+        Format.asprintf "Filtered: %a"
+          (Pretty_utils.pp_list ~sep:", " pp_filtered) remove
+      in
+      let cond = condition step @@ Lang.F.p_bool @@ Lang.F.e_and kept in
+      Tactical.replace_single ~at:step.id (feedback, cond)
 
     | _ -> raise Not_found
   end
@@ -71,7 +83,8 @@ let collect_remove m = function
 
 let fold_selection s seq =
   let m = List.fold_left collect_remove Smap.empty s in
-  "Filtered", Smap.fold (fun s l seq -> snd @@ tactical_inside s l seq) m seq
+  "Filtered mutiple selection",
+  Smap.fold (fun s l seq -> snd @@ tactical_inside s l seq) m seq
 
 let process (f: sequent -> string * sequent) s = [ f s ]
 
diff --git a/src/plugins/wp/TacUnfold.ml b/src/plugins/wp/TacUnfold.ml
index cb40a59232593e3ae3e3430e070e3b3adb3a764f..f72efde27b4351668c9ad6f5d474747613b8ed08 100644
--- a/src/plugins/wp/TacUnfold.ml
+++ b/src/plugins/wp/TacUnfold.ml
@@ -118,9 +118,22 @@ let tactical_inside step unfolds sequent =
   then raise Not_found
   else match step.condition with
     | Type p | Have p | When p | Core p | Init p ->
-      let subst t = Lang.F.Tmap.find t unfolds in
+      let unfolded = ref [] in
+      let subst t =
+        let result = Lang.F.Tmap.find t unfolds in
+        begin match F.repr t with
+          | Qed.Logic.Fun(f,_) -> unfolded := f :: !unfolded
+          | _ -> ()
+        end ;
+        result
+      in
       let p = condition step @@ Lang.p_subst subst p in
-      snd @@ Tactical.replace_single ~at:step.id ("Unfolded", p) sequent
+      let unfolded = List.sort_uniq Lang.Fun.compare !unfolded in
+      let feedback =
+        Format.asprintf "Unfolded: %a"
+          (Pretty_utils.pp_list ~sep:", " Lang.Fun.pretty) unfolded
+      in
+      snd @@ Tactical.replace_single ~at:step.id (feedback, p) sequent
     | _ -> raise Not_found
 
 let tactical_goal unfolds (seq, g) =
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
index ebcdcd1cd229d0de017357404831a238328bd6d8..7af1209d3c472e1e717ba1dcdf4090b5f4b641ba 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
@@ -51,7 +51,7 @@
   typed_clear_in_step_check subgoal:
   
   Goal Wp.Tactical.typed_clear_in_step_check-0 (generated):
-  Assume { (* Filtered *) Have: P_Q /\ P_R. }
+  Assume { (* Filtered: P_P(...) *) Have: P_Q /\ P_R. }
   Prove: P_S(42).
   
   ------------------------------------------------------------
@@ -77,7 +77,7 @@
   typed_clear_in_step_check subgoal:
   
   Goal Wp.Tactical.typed_clear_in_step_check-1 (generated):
-  Assume { (* Filtered *) Have: P_R. }
+  Assume { (* Filtered: P_Q(...) *) Have: P_R. }
   Prove: P_S(42).
   
   ------------------------------------------------------------