diff --git a/src/plugins/wp/TacClear.ml b/src/plugins/wp/TacClear.ml
index b804eb95c975712f0c83243af82180988485f436..bf1f7aeaeee5ee9305a2d56a58abcb875acb0ebf 100644
--- a/src/plugins/wp/TacClear.ml
+++ b/src/plugins/wp/TacClear.ml
@@ -82,8 +82,9 @@ let tactical_inside step remove =
         List.fold_left add Filteredset.empty remove
       in
       let feedback =
+        let pp fmt f = Format.fprintf fmt "'%a'" Filtered.pretty f in
         Format.asprintf "Filtered: %a"
-          (Pretty_utils.pp_list ~sep:", " Filtered.pretty) removed
+          (Pretty_utils.pp_list ~sep:", " pp) removed
       in
       let cond = condition step @@ Lang.F.p_bool @@ Lang.F.e_and kept in
       removed, Tactical.replace_single ~at:step.id (feedback, cond)
@@ -114,8 +115,9 @@ let fold_selection s seq =
   in
   let removed, seq = Smap.fold tactical m ([], seq) in
   let feedback =
+    let pp fmt f = Format.fprintf fmt "'%a'" Filtered.pretty f in
     Format.asprintf "Filtered: %a"
-      (Pretty_utils.pp_list ~sep:", " Filtered.pretty) removed
+      (Pretty_utils.pp_list ~sep:", " pp) removed
   in
   feedback, seq
 
diff --git a/src/plugins/wp/TacUnfold.ml b/src/plugins/wp/TacUnfold.ml
index af0f08d7ecda26723a1420383748a8f023011306..a30d3798e06589c1e4ed673a63cda1e608de72bf 100644
--- a/src/plugins/wp/TacUnfold.ml
+++ b/src/plugins/wp/TacUnfold.ml
@@ -131,8 +131,9 @@ let tactical_inside step unfolds sequent =
       in
       let p = condition step @@ Lang.p_subst subst p in
       let feedback =
-        Format.asprintf "Unfold '%a'"
-          (Pretty_utils.pp_list ~sep:", " Lang.Fun.pretty) !unfolded
+        let pp fmt f = Format.fprintf fmt "'%a'" Lang.Fun.pretty f in
+        Format.asprintf "Unfold %a"
+          (Pretty_utils.pp_list ~sep:", " pp) !unfolded
       in
       !unfolded, snd @@ Tactical.replace_single ~at:step.id (feedback, p) sequent
     | _ -> raise Not_found
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 7af1209d3c472e1e717ba1dcdf4090b5f4b641ba..9c2a626fc58df6e504db7003ad19ac459f55babc 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: P_P(...) *) 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: P_Q(...) *) Have: P_R. }
+  Assume { (* Filtered: 'P_Q(...)' *) Have: P_R. }
   Prove: P_S(42).
   
   ------------------------------------------------------------