Skip to content
Snippets Groups Projects
Commit 274fce90 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Rephrase a from warning

parent 289f6d07
No related branches found
No related tags found
No related merge requests found
...@@ -342,8 +342,8 @@ let add_assigns acc kind id a_desc = ...@@ -342,8 +342,8 @@ let add_assigns acc kind id a_desc =
if goal && assigns_has_deps a_desc.a_assigns then if goal && assigns_has_deps a_desc.a_assigns then
Wp_parameters.warning Wp_parameters.warning
~once: true ~current:false ~wkey:AssignsCompleteness.wkey_pedantic ~once: true ~current:false ~wkey:AssignsCompleteness.wkey_pedantic
"WP uses \\from to compute precise hypotheses but their proof is not yet \ "WP uses \\from to generate precise hypotheses, however their proof is \
supported" ; not supported yet" ;
if goal then { acc with has_asgn_goal = true} else acc if goal then { acc with has_asgn_goal = true} else acc
let add_assigns_any acc kind asgn = let add_assigns_any acc kind asgn =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment