Commit 4c27fb0a authored by Robbert Krebbers's avatar Robbert Krebbers

Generalize 7c4416b6 to remove head "value ;;" expressions after any wp_ tactic.

parent 1aba9415
Pipeline #1595 passed with stage
......@@ -148,7 +148,7 @@ Tactic Notation "wp_store" :=
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
|env_cbv; reflexivity
|wp_finish; try wp_seq]
|wp_finish]
| _ => fail "wp_store: not a 'wp'"
end.
......
......@@ -22,8 +22,14 @@ Ltac wp_value_head :=
match goal with |- _ wp _ _ _ => simpl | _ => fail end)
end.
Ltac wp_seq_head :=
lazymatch goal with
| |- _ wp ?E (Seq _ _) ?Q => etrans; [|eapply wp_seq; wp_done]; strip_later
end.
Ltac wp_finish := intros_revert ltac:(
rewrite /= ?to_of_val; try strip_later; try wp_value_head).
rewrite /= ?to_of_val; try strip_later; try wp_value_head);
repeat wp_seq_head.
Tactic Notation "wp_value" :=
lazymatch goal with
......
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