diff --git a/prelude/base.v b/prelude/base.v
index 86b1036fb2c416eb10b7c9f30377b42f52db988c..f354f0e0b635da187966d0fd8320d8e178d9a2e9 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -590,7 +590,7 @@ Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : C_scope.
 
 Class Difference A := difference: A → A → A.
 Instance: Params (@difference) 2.
-Infix "∖" := difference (at level 40) : C_scope.
+Infix "∖" := difference (at level 40, left associativity) : C_scope.
 Notation "(∖)" := difference (only parsing) : C_scope.
 Notation "( x ∖)" := (difference x) (only parsing) : C_scope.
 Notation "(∖ x )" := (λ y, difference y x) (only parsing) : C_scope.
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 9950d42d348fca40966192e47bb7e541040920d4..ee59788b16cd3cbfff5a1fd16605e836d93c46c2 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -77,7 +77,7 @@ Section ndisjoint.
 End ndisjoint.
 
 (* The hope is that registering these will suffice to solve most goals
-of the form [N1 ⊥ N2] and those of the form [((N1 ⊆ E ∖ N2) ∖ ..) ∖ Nn]. *)
+of the form [N1 ⊥ N2] and those of the form [N1 ⊆ E ∖ N2 ∖ .. ∖ Nn]. *)
 Hint Resolve ndisj_subseteq_difference : ndisj.
 Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj.
 Hint Resolve ndot_preserve_disjoint_l : ndisj.