From 193241d0614dfed9c7ab62408b45d3d7fe2601be Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 11 Jul 2019 09:07:14 +0200 Subject: [PATCH] remove SearchAbout --- theories/logatom/herlihy_wing_queue/hwq.v | 1 - 1 file changed, 1 deletion(-) diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v index 428c7b4..91f122b 100644 --- a/theories/logatom/herlihy_wing_queue/hwq.v +++ b/theories/logatom/herlihy_wing_queue/hwq.v @@ -2700,7 +2700,6 @@ Proof. - iDestruct (contra_agree with "Hinit_cont Hcont") as %[-> ->]. iPureIntro. split; first done. destruct Hcont as (((H1 & H2) & H3) & _). done. - by iDestruct (contra_not_no_contra with "Hcont Hinit_cont") as "False". } - SearchAbout "snap". (* We resolve. *) iDestruct "Hproph" as (rs) "[Hp Hpvs]". iDestruct "Hpvs" as %Hpvs. wp_apply (wp_resolve with "Hp"); first done. -- GitLab