diff --git a/barrier/client.v b/barrier/client.v
index 8ad1d8f26208f9dcf4dfa363dea863dae509028f..5e888030cf26009598b28cc906f00cfded651bca 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -33,13 +33,13 @@ Section ClosedProofs.
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
   Proof.
-    apply ht_alt. rewrite (heap_alloc ⊤ (ndot nroot "Barrier")); last first.
+    apply ht_alt. rewrite (heap_alloc ⊤ (nroot .: "Barrier")); last first.
     { (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
-      move=>? _. exact I. }
+      by move=>? _. }
     apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
     rewrite -(client_safe (nroot .: "Heap" ) (nroot .: "Barrier" )) //.
     (* This, too, should be automated. *)
-    apply ndot_ne_disjoint. discriminate.
+    by apply ndot_ne_disjoint.
   Qed.
 
   Print Assumptions client_safe_closed.
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 84ed58a5e6864b9361e1d95a6a693c8130e78c97..08a2c881dddd7f1edf224b81fbb588d2df998ed8 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -8,7 +8,7 @@ Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
 Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
 
 Infix ".:" := ndot (at level 19, left associativity) : C_scope.
-Notation "(.:)" := ndot : C_scope.
+Notation "(.:)" := ndot (only parsing) : C_scope.
 
 Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
 Proof. by intros N1 x1 N2 x2 ?; simplify_eq. Qed.