[wp] Coherence between messages in Clear and Unfold

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
 

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

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).
   
   ------------------------------------------------------------