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

[wp] Fix sequence insertion order

parent e805dea0
No related branches found
No related tags found
No related merge requests found
...@@ -1740,7 +1740,7 @@ let step_at seq k = ...@@ -1740,7 +1740,7 @@ let step_at seq k =
let in_sequence_add_list ~replace = let in_sequence_add_list ~replace =
let rec in_list k h w = let rec in_list k h w =
if k = 0 then if k = 0 then
List.rev_append h List.rev_append (List.rev h)
(if replace (if replace
then match w with then match w with
| [] -> assert false | [] -> assert false
......
...@@ -247,11 +247,11 @@ ...@@ -247,11 +247,11 @@
Goal Wp.Tactical.typed_test_step_and_ensures-0 (generated): Goal Wp.Tactical.typed_test_step_and_ensures-0 (generated):
Assume { Assume {
(* Pre-condition *) (* Pre-condition *)
Have: P_R. Have: P_P.
(* Pre-condition *) (* Pre-condition *)
Have: P_Q. Have: P_Q.
(* Pre-condition *) (* Pre-condition *)
Have: P_P. Have: P_R.
} }
Prove: P_S. Prove: P_S.
......
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