From 391e52d7684d49096f7b81e8594c592daea5e8cd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 17 Sep 2017 14:45:35 +0200
Subject: [PATCH] Fix previous commit.

---
 theories/base_logic/lib/namespaces.v      | 2 +-
 theories/heap_lang/lib/barrier/protocol.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index c55135e46..c3d38e7aa 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -35,7 +35,7 @@ Section namespace.
   Global Instance ndot_inj : Inj2 (=) (=) (=) (@ndot A _ _).
   Proof. intros N1 x1 N2 x2; rewrite !ndot_eq=> ?; by simplify_eq. Qed.
 
-  Lemma nclose_nroot : ↑nroot = ⊤.
+  Lemma nclose_nroot : ↑nroot = (⊤:coPset).
   Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
   Lemma encode_nclose N : encode N ∈ (↑N:coPset).
   Proof.
diff --git a/theories/heap_lang/lib/barrier/protocol.v b/theories/heap_lang/lib/barrier/protocol.v
index 1992abed4..8ed9bbf50 100644
--- a/theories/heap_lang/lib/barrier/protocol.v
+++ b/theories/heap_lang/lib/barrier/protocol.v
@@ -77,7 +77,7 @@ Proof.
   - destruct p; set_solver.
   - apply elem_of_equiv=> /= -[j|]; last set_solver.
     set_unfold; rewrite !(inj_iff Change).
-    assert (Change j ∈ match p with Low => ∅ | High => {[Send]} end ↔ False)
+    assert (Change j ∈ match p with Low => ∅ : set token | High => {[Send]} end ↔ False)
       as -> by (destruct p; set_solver).
     destruct (decide (i1 = j)) as [->|]; first naive_solver.
     destruct (decide (i2 = j)) as [->|]; first naive_solver.
-- 
GitLab