diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index c55135e4629b5e0214dcd81c22b07009b329bca9..c3d38e7aa47799adfa5cae062309d1db18232098 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 1992abed4a66434436ca727d4a859107282d7df9..8ed9bbf50454e456be7b19dc39923bf6047a93df 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.