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

Get rid of a SearchAbout.

parent 53f6857f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/heap_lang/lib/barrier/proof.v
+ 0
− 2
View file @ a24b19a9
...@@ -198,6 +198,4 @@ Lemma recv_mono l P1 P2 : (P1 ⊢ P2) → recv l P1 ⊢ recv l P2. ...@@ -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. Proof. iIntros (HP) "H". iApply (recv_weaken with "[] H"). iApply HP. Qed.
End proof. End proof.
SearchAbout _.
Typeclasses Opaque barrier_ctx send recv. Typeclasses Opaque barrier_ctx send recv.
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