From 274fce90c6c1df23f64c67e69ee28beeb015c1db Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 12 Nov 2020 09:17:09 +0100
Subject: [PATCH] [wp] Rephrase a from warning
---
src/plugins/wp/wpStrategy.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index ff8982df5f1..7026d240203 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 =
--
GitLab