Commit 193241d0 authored by Ralf Jung's avatar Ralf Jung

remove SearchAbout

parent a58a15e2
Pipeline #18371 passed with stage
in 18 minutes and 48 seconds
...@@ -2700,7 +2700,6 @@ Proof. ...@@ -2700,7 +2700,6 @@ Proof.
- iDestruct (contra_agree with "Hinit_cont Hcont") as %[-> ->]. - iDestruct (contra_agree with "Hinit_cont Hcont") as %[-> ->].
iPureIntro. split; first done. destruct Hcont as (((H1 & H2) & H3) & _). done. iPureIntro. split; first done. destruct Hcont as (((H1 & H2) & H3) & _). done.
- by iDestruct (contra_not_no_contra with "Hcont Hinit_cont") as "False". } - by iDestruct (contra_not_no_contra with "Hcont Hinit_cont") as "False". }
SearchAbout "snap".
(* We resolve. *) (* We resolve. *)
iDestruct "Hproph" as (rs) "[Hp Hpvs]". iDestruct "Hpvs" as %Hpvs. iDestruct "Hproph" as (rs) "[Hp Hpvs]". iDestruct "Hpvs" as %Hpvs.
wp_apply (wp_resolve with "Hp"); first done. wp_apply (wp_resolve with "Hp"); first done.
......
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