Commit 37713a6a authored by Ralf Jung's avatar Ralf Jung

move a TODO around

parent d26dfb1c
......@@ -63,8 +63,6 @@ Section LiftingTests.
Proof.
wp_lam. wp_op=> ?; wp_if.
- wp_op. wp_op.
(* TODO: Can we use the wp tactic again here? It seems that the tactic fails if there
are goals being generated. That should not be the case. *)
ewp apply FindPred_spec; last omega.
wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
- by ewp apply FindPred_spec; eauto with omega.
......
......@@ -190,6 +190,7 @@ Tactic Notation "wp" ">" tactic(tac) :=
end.
Tactic Notation "wp" tactic(tac) := (wp> tac); [wp_strip_later|..].
(* In case the precondition does not match *)
(* In case the precondition does not match.
TODO: Have one tactic unifying wp and ewp. *)
Tactic Notation "ewp" tactic(tac) := wp (etrans; [|tac]).
Tactic Notation "ewp" ">" tactic(tac) := wp> (etrans; [|tac]).
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