From a24b19a9051e7fb1187b092e93e3bce2430387e5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 Jan 2017 18:04:59 +0100
Subject: [PATCH] Get rid of a SearchAbout.

---
 theories/heap_lang/lib/barrier/proof.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index 41e84948d..dd3928187 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -198,6 +198,4 @@ Lemma recv_mono l P1 P2 : (P1 ⊢ P2) → recv l P1 ⊢ recv l P2.
 Proof. iIntros (HP) "H". iApply (recv_weaken with "[] H"). iApply HP. Qed.
 End proof.
 
-SearchAbout _.
-
 Typeclasses Opaque barrier_ctx send recv.
-- 
GitLab