aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc/cctac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc/cctac.ml')
-rw-r--r--plugins/cc/cctac.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index c8924073c..bd788a425 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -424,10 +424,10 @@ let cc_tactic depth additionnal_terms =
List.map
(build_term_to_complete uf newmeta)
(epsilons uf) in
- Pp.msg_info
+ Feedback.msg_info
(Pp.str "Goal is solvable by congruence but \
some arguments are missing.");
- Pp.msg_info
+ Feedback.msg_info
(Pp.str " Try " ++
hov 8
begin