Commit 82ac261b authored by Andrei Paskevich's avatar Andrei Paskevich

tentatively fix #13081

- keep existing positions in wp_label
- do not add the "WP" label, seems to be never used
parent 42a1adb2
......@@ -407,9 +407,11 @@ let well_founded_rel = function
(* Recursive computation of the weakest precondition *)
let wp_label ?loc ?(lab=[]) f =
let loc = option_apply f.t_loc (fun x -> Some x) loc in
let loc = option_apply loc (fun x -> Some x) f.t_loc in
let lab = lab @ f.t_label in
let lab = if List.mem "WP" lab then lab else "WP" :: lab in
t_label ?loc lab f
let t_True env =
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment