Skip to content
Snippets Groups Projects
Commit afa8efc2 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use ewp tactic in heap_lang/tests.

parent df418290
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
heap_lang/tests.v
+ 2
− 2
View file @ afa8efc2
...@@ -65,9 +65,9 @@ Section LiftingTests. ...@@ -65,9 +65,9 @@ Section LiftingTests.
- wp_op. wp_op. - wp_op. wp_op.
(* TODO: Can we use the wp tactic again here? It seems that the tactic fails if there (* 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. *) are goals being generated. That should not be the case. *)
wp_focus (FindPred _ _). rewrite -FindPred_spec; last by omega. ewp apply FindPred_spec; last omega.
wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega. wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
- rewrite -FindPred_spec; eauto with omega. - by ewp apply FindPred_spec; eauto with omega.
Qed. Qed.
Lemma Pred_user E : Lemma Pred_user E :
......
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