Skip to content
Snippets Groups Projects
Commit abd17210 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Fix "not yet" message for decreases clauses

parent 015036a0
No related branches found
No related tags found
No related merge requests found
......@@ -57,7 +57,7 @@ let pre_funspec kf kinstr env funspec =
unsupported
(fun spec ->
let ppt = Property.ip_decreases_of_spec kf kinstr spec in
if must_translate_opt ppt then Env.not_yet env "variant clause")
if must_translate_opt ppt then Env.not_yet env "decreases clause")
funspec;
(* TODO: spec.spec_terminates is not part of the E-ACSL subset *)
unsupported
......
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