From 335c29dd717d6ec2bdee84a46306283ff0b68804 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Jan 2021 22:54:11 +0100
Subject: [PATCH] `Free` is atomic.

---
 iris_heap_lang/primitive_laws.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 0f168abe0..194bca70d 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -123,6 +123,8 @@ Proof. solve_atomic. Qed.
 
 Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
 Proof. solve_atomic. Qed.
+Instance free_atomic s v : Atomic s (Free (Val v)).
+Proof. solve_atomic. Qed.
 Instance load_atomic s v : Atomic s (Load (Val v)).
 Proof. solve_atomic. Qed.
 Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
-- 
GitLab