diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml index ff8982df5f1d6e85b9819334ad52ea744a68fbd3..7026d2402035f301bee12cf740d9b92663f712f0 100644 --- a/src/plugins/wp/wpStrategy.ml +++ b/src/plugins/wp/wpStrategy.ml @@ -342,8 +342,8 @@ let add_assigns acc kind id a_desc = if goal && assigns_has_deps a_desc.a_assigns then Wp_parameters.warning ~once: true ~current:false ~wkey:AssignsCompleteness.wkey_pedantic - "WP uses \\from to compute precise hypotheses but their proof is not yet \ - supported" ; + "WP uses \\from to generate precise hypotheses, however their proof is \ + not supported yet" ; if goal then { acc with has_asgn_goal = true} else acc let add_assigns_any acc kind asgn =