diff --git a/CHANGELOG.md b/CHANGELOG.md
index 210ae54badd1596da1f9ef7dbbc566f04e2adb76..16857f629431e444e1888bb44c8d5a5937fbebcd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,10 @@ API-breaking change is listed.
 - Rename `dom_map_filter` into `dom_map_filter_subseteq` and repurpose
   `dom_map_filter` for the version with the equality. This follows the naming
   convention for similar lemmas.
+- Disambiguate Haskell-style notations for partially applied operators. For
+  example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as a
+  prefix, as done in VST. A sed script to perform the renaming can be found at:
+  https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/93
 
 ## std++ 1.2.1 (released 2019-08-29)
 
diff --git a/theories/base.v b/theories/base.v
index 83847b691a6b9450b9022e0178be499aeba9b791..3900bc61734e1cf3c6cb20c5df4edf90e85f1a1d 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -167,11 +167,11 @@ Notation "'False'" := False (format "False") : type_scope.
 (** * Equality *)
 (** Introduce some Haskell style like notations. *)
 Notation "(=)" := eq (only parsing) : stdpp_scope.
-Notation "( x =)" := (eq x) (only parsing) : stdpp_scope.
-Notation "(= x )" := (λ y, eq y x) (only parsing) : stdpp_scope.
+Notation "( x =.)" := (eq x) (only parsing) : stdpp_scope.
+Notation "(.= x )" := (λ y, eq y x) (only parsing) : stdpp_scope.
 Notation "(≠)" := (λ x y, x ≠ y) (only parsing) : stdpp_scope.
-Notation "( x ≠)" := (λ y, x ≠ y) (only parsing) : stdpp_scope.
-Notation "(≠ x )" := (λ y, y ≠ x) (only parsing) : stdpp_scope.
+Notation "( x ≠.)" := (λ y, x ≠ y) (only parsing) : stdpp_scope.
+Notation "(.≠ x )" := (λ y, y ≠ x) (only parsing) : stdpp_scope.
 
 Infix "=@{ A }" := (@eq A)
   (at level 70, only parsing, no associativity) : stdpp_scope.
@@ -199,12 +199,12 @@ Infix "≡@{ A }" := (@equiv A _)
   (at level 70, only parsing, no associativity) : stdpp_scope.
 
 Notation "(≡)" := equiv (only parsing) : stdpp_scope.
-Notation "( X ≡)" := (equiv X) (only parsing) : stdpp_scope.
-Notation "(≡ X )" := (λ Y, Y ≡ X) (only parsing) : stdpp_scope.
+Notation "( X ≡.)" := (equiv X) (only parsing) : stdpp_scope.
+Notation "(.≡ X )" := (λ Y, Y ≡ X) (only parsing) : stdpp_scope.
 Notation "(≢)" := (λ X Y, ¬X ≡ Y) (only parsing) : stdpp_scope.
 Notation "X ≢ Y":= (¬X ≡ Y) (at level 70, no associativity) : stdpp_scope.
-Notation "( X ≢)" := (λ Y, X ≢ Y) (only parsing) : stdpp_scope.
-Notation "(≢ X )" := (λ Y, Y ≢ X) (only parsing) : stdpp_scope.
+Notation "( X ≢.)" := (λ Y, X ≢ Y) (only parsing) : stdpp_scope.
+Notation "(.≢ X )" := (λ Y, Y ≢ X) (only parsing) : stdpp_scope.
 
 Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope.
 Notation "(≢@{ A } )" := (λ X Y, ¬X ≡@{A} Y) (only parsing) : stdpp_scope.
@@ -295,8 +295,8 @@ Hint Mode ProofIrrel ! : typeclass_instances.
 
 (** ** Common properties *)
 (** These operational type classes allow us to refer to common mathematical
-properties in a generic way. For example, for injectivity of [(k ++)] it
-allows us to write [inj (k ++)] instead of [app_inv_head k]. *)
+properties in a generic way. For example, for injectivity of [(k ++.)] it
+allows us to write [inj (k ++.)] instead of [app_inv_head k]. *)
 Class Inj {A B} (R : relation A) (S : relation B) (f : A → B) : Prop :=
   inj x y : S (f x) (f y) → R x y.
 Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
@@ -414,16 +414,16 @@ Class TotalOrder {A} (R : relation A) : Prop := {
 
 (** * Logic *)
 Notation "(∧)" := and (only parsing) : stdpp_scope.
-Notation "( A ∧)" := (and A) (only parsing) : stdpp_scope.
-Notation "(∧ B )" := (λ A, A ∧ B) (only parsing) : stdpp_scope.
+Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope.
+Notation "(.∧ B )" := (λ A, A ∧ B) (only parsing) : stdpp_scope.
 
 Notation "(∨)" := or (only parsing) : stdpp_scope.
-Notation "( A ∨)" := (or A) (only parsing) : stdpp_scope.
-Notation "(∨ B )" := (λ A, A ∨ B) (only parsing) : stdpp_scope.
+Notation "( A ∨.)" := (or A) (only parsing) : stdpp_scope.
+Notation "(.∨ B )" := (λ A, A ∨ B) (only parsing) : stdpp_scope.
 
 Notation "(↔)" := iff (only parsing) : stdpp_scope.
-Notation "( A ↔)" := (iff A) (only parsing) : stdpp_scope.
-Notation "(↔ B )" := (λ A, A ↔ B) (only parsing) : stdpp_scope.
+Notation "( A ↔.)" := (iff A) (only parsing) : stdpp_scope.
+Notation "(.↔ B )" := (λ A, A ↔ B) (only parsing) : stdpp_scope.
 
 Hint Extern 0 (_ ↔ _) => reflexivity : core.
 Hint Extern 0 (_ ↔ _) => symmetry; assumption : core.
@@ -488,18 +488,18 @@ Proof. unfold impl. red; intuition. Qed.
 (** * Common data types *)
 (** ** Functions *)
 Notation "(→)" := (λ A B, A → B) (only parsing) : stdpp_scope.
-Notation "( A →)" := (λ B, A → B) (only parsing) : stdpp_scope.
-Notation "(→ B )" := (λ A, A → B) (only parsing) : stdpp_scope.
+Notation "( A →.)" := (λ B, A → B) (only parsing) : stdpp_scope.
+Notation "(.→ B )" := (λ A, A → B) (only parsing) : stdpp_scope.
 
 Notation "t $ r" := (t r)
   (at level 65, right associativity, only parsing) : stdpp_scope.
 Notation "($)" := (λ f x, f x) (only parsing) : stdpp_scope.
-Notation "($ x )" := (λ f, f x) (only parsing) : stdpp_scope.
+Notation "(.$ x )" := (λ f, f x) (only parsing) : stdpp_scope.
 
 Infix "∘" := compose : stdpp_scope.
 Notation "(∘)" := compose (only parsing) : stdpp_scope.
-Notation "( f ∘)" := (compose f) (only parsing) : stdpp_scope.
-Notation "(∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope.
+Notation "( f ∘.)" := (compose f) (only parsing) : stdpp_scope.
+Notation "(.∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope.
 
 Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A → B) :=
   populate (λ _, inhabitant).
@@ -599,8 +599,8 @@ Instance Empty_set_leibniz : LeibnizEquiv Empty_set.
 Proof. intros [] []; reflexivity. Qed.
 
 (** ** Products *)
-Notation "( x ,)" := (pair x) (only parsing) : stdpp_scope.
-Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
+Notation "( x ,.)" := (pair x) (only parsing) : stdpp_scope.
+Notation "(., y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
 
 Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1").
 Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2").
@@ -786,8 +786,8 @@ Hint Mode Union ! : typeclass_instances.
 Instance: Params (@union) 2 := {}.
 Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
 Notation "(∪)" := union (only parsing) : stdpp_scope.
-Notation "( x ∪)" := (union x) (only parsing) : stdpp_scope.
-Notation "(∪ x )" := (λ y, union y x) (only parsing) : stdpp_scope.
+Notation "( x ∪.)" := (union x) (only parsing) : stdpp_scope.
+Notation "(.∪ x )" := (λ y, union y x) (only parsing) : stdpp_scope.
 Infix "∪*" := (zip_with (∪)) (at level 50, left associativity) : stdpp_scope.
 Notation "(∪*)" := (zip_with (∪)) (only parsing) : stdpp_scope.
 Infix "∪**" := (zip_with (zip_with (∪)))
@@ -804,24 +804,24 @@ Hint Mode DisjUnion ! : typeclass_instances.
 Instance: Params (@disj_union) 2 := {}.
 Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
 Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
-Notation "( x ⊎)" := (disj_union x) (only parsing) : stdpp_scope.
-Notation "(⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
+Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
+Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
 
 Class Intersection A := intersection: A → A → A.
 Hint Mode Intersection ! : typeclass_instances.
 Instance: Params (@intersection) 2 := {}.
 Infix "∩" := intersection (at level 40) : stdpp_scope.
 Notation "(∩)" := intersection (only parsing) : stdpp_scope.
-Notation "( x ∩)" := (intersection x) (only parsing) : stdpp_scope.
-Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
+Notation "( x ∩.)" := (intersection x) (only parsing) : stdpp_scope.
+Notation "(.∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
 
 Class Difference A := difference: A → A → A.
 Hint Mode Difference ! : typeclass_instances.
 Instance: Params (@difference) 2 := {}.
 Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
 Notation "(∖)" := difference (only parsing) : stdpp_scope.
-Notation "( x ∖)" := (difference x) (only parsing) : stdpp_scope.
-Notation "(∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope.
+Notation "( x ∖.)" := (difference x) (only parsing) : stdpp_scope.
+Notation "(.∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope.
 Infix "∖*" := (zip_with (∖)) (at level 40, left associativity) : stdpp_scope.
 Notation "(∖*)" := (zip_with (∖)) (only parsing) : stdpp_scope.
 Infix "∖**" := (zip_with (zip_with (∖)))
@@ -846,12 +846,12 @@ Hint Mode SubsetEq ! : typeclass_instances.
 Instance: Params (@subseteq) 2 := {}.
 Infix "⊆" := subseteq (at level 70) : stdpp_scope.
 Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
-Notation "( X ⊆)" := (subseteq X) (only parsing) : stdpp_scope.
-Notation "(⊆ X )" := (λ Y, Y ⊆ X) (only parsing) : stdpp_scope.
+Notation "( X ⊆.)" := (subseteq X) (only parsing) : stdpp_scope.
+Notation "(.⊆ X )" := (λ Y, Y ⊆ X) (only parsing) : stdpp_scope.
 Notation "X ⊈ Y" := (¬X ⊆ Y) (at level 70) : stdpp_scope.
 Notation "(⊈)" := (λ X Y, X ⊈ Y) (only parsing) : stdpp_scope.
-Notation "( X ⊈)" := (λ Y, X ⊈ Y) (only parsing) : stdpp_scope.
-Notation "(⊈ X )" := (λ Y, Y ⊈ X) (only parsing) : stdpp_scope.
+Notation "( X ⊈.)" := (λ Y, X ⊈ Y) (only parsing) : stdpp_scope.
+Notation "(.⊈ X )" := (λ Y, Y ⊈ X) (only parsing) : stdpp_scope.
 
 Infix "⊆@{ A }" := (@subseteq A _) (at level 70, only parsing) : stdpp_scope.
 Notation "(⊆@{ A } )" := (@subseteq A _) (only parsing) : stdpp_scope.
@@ -870,12 +870,12 @@ Hint Extern 0 (_ ⊆** _) => reflexivity : core.
 
 Infix "⊂" := (strict (⊆)) (at level 70) : stdpp_scope.
 Notation "(⊂)" := (strict (⊆)) (only parsing) : stdpp_scope.
-Notation "( X ⊂)" := (strict (⊆) X) (only parsing) : stdpp_scope.
-Notation "(⊂ X )" := (λ Y, Y ⊂ X) (only parsing) : stdpp_scope.
+Notation "( X ⊂.)" := (strict (⊆) X) (only parsing) : stdpp_scope.
+Notation "(.⊂ X )" := (λ Y, Y ⊂ X) (only parsing) : stdpp_scope.
 Notation "X ⊄ Y" := (¬X ⊂ Y) (at level 70) : stdpp_scope.
 Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : stdpp_scope.
-Notation "( X ⊄)" := (λ Y, X ⊄ Y) (only parsing) : stdpp_scope.
-Notation "(⊄ X )" := (λ Y, Y ⊄ X) (only parsing) : stdpp_scope.
+Notation "( X ⊄.)" := (λ Y, X ⊄ Y) (only parsing) : stdpp_scope.
+Notation "(.⊄ X )" := (λ Y, Y ⊄ X) (only parsing) : stdpp_scope.
 
 Infix "⊂@{ A }" := (strict (⊆@{A})) (at level 70, only parsing) : stdpp_scope.
 Notation "(⊂@{ A } )" := (strict (⊆@{A})) (only parsing) : stdpp_scope.
@@ -903,12 +903,12 @@ Hint Mode ElemOf - ! : typeclass_instances.
 Instance: Params (@elem_of) 3 := {}.
 Infix "∈" := elem_of (at level 70) : stdpp_scope.
 Notation "(∈)" := elem_of (only parsing) : stdpp_scope.
-Notation "( x ∈)" := (elem_of x) (only parsing) : stdpp_scope.
-Notation "(∈ X )" := (λ x, elem_of x X) (only parsing) : stdpp_scope.
+Notation "( x ∈.)" := (elem_of x) (only parsing) : stdpp_scope.
+Notation "(.∈ X )" := (λ x, elem_of x X) (only parsing) : stdpp_scope.
 Notation "x ∉ X" := (¬x ∈ X) (at level 80) : stdpp_scope.
 Notation "(∉)" := (λ x X, x ∉ X) (only parsing) : stdpp_scope.
-Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : stdpp_scope.
-Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : stdpp_scope.
+Notation "( x ∉.)" := (λ X, x ∉ X) (only parsing) : stdpp_scope.
+Notation "(.∉ X )" := (λ x, x ∉ X) (only parsing) : stdpp_scope.
 
 Infix "∈@{ B }" := (@elem_of _ B _) (at level 70, only parsing) : stdpp_scope.
 Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope.
@@ -1005,8 +1005,8 @@ Arguments omap {_ _ _ _} _ !_ / : assert.
 Instance: Params (@omap) 4 := {}.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
-Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
-Notation "(≫= f )" := (mbind f) (only parsing) : stdpp_scope.
+Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
+Notation "(.≫= f )" := (mbind f) (only parsing) : stdpp_scope.
 Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
 
 Notation "x ← y ; z" := (y ≫= (λ x : _, z))
@@ -1043,8 +1043,8 @@ Hint Mode Lookup - - ! : typeclass_instances.
 Instance: Params (@lookup) 4 := {}.
 Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
 Notation "(!!)" := lookup (only parsing) : stdpp_scope.
-Notation "( m !!)" := (λ i, m !! i) (only parsing) : stdpp_scope.
-Notation "(!! i )" := (lookup i) (only parsing) : stdpp_scope.
+Notation "( m !!.)" := (λ i, m !! i) (only parsing) : stdpp_scope.
+Notation "(.!! i )" := (lookup i) (only parsing) : stdpp_scope.
 Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The singleton map *)
@@ -1272,8 +1272,8 @@ Hint Mode SqSubsetEq ! : typeclass_instances.
 Instance: Params (@sqsubseteq) 2 := {}.
 Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
 Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
-Notation "( x ⊑)" := (sqsubseteq x) (only parsing) : stdpp_scope.
-Notation "(⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
+Notation "( x ⊑.)" := (sqsubseteq x) (only parsing) : stdpp_scope.
+Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
 
 Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
 Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
@@ -1287,16 +1287,16 @@ Hint Mode Meet ! : typeclass_instances.
 Instance: Params (@meet) 2 := {}.
 Infix "⊓" := meet (at level 40) : stdpp_scope.
 Notation "(⊓)" := meet (only parsing) : stdpp_scope.
-Notation "( x ⊓)" := (meet x) (only parsing) : stdpp_scope.
-Notation "(⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
+Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
+Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
 
 Class Join A := join: A → A → A.
 Hint Mode Join ! : typeclass_instances.
 Instance: Params (@join) 2 := {}.
 Infix "⊔" := join (at level 50) : stdpp_scope.
 Notation "(⊔)" := join (only parsing) : stdpp_scope.
-Notation "( x ⊔)" := (join x) (only parsing) : stdpp_scope.
-Notation "(⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
+Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
+Notation "(.⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
 
 Class Top A := top : A.
 Hint Mode Top ! : typeclass_instances.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index f22e042198d8875e5433ba519f1330cf1ed98484..5a5d2ca4a644198c67cd0575848bacca4cbf50db 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -121,7 +121,7 @@ Instance map_difference `{Merge M} {A} : Difference (M A) :=
 of the elements. Implemented by conversion to lists, so not very efficient. *)
 Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A),
     ∀ A, FinMapToList K A (M A)} {A B} (f : K → A → option B) (m : M A) : M B :=
-  list_to_map (omap (λ ix, (fst ix,) <$> curry f ix) (map_to_list m)).
+  list_to_map (omap (λ ix, (fst ix ,.) <$> curry f ix) (map_to_list m)).
 
 (* The zip operation on maps combines two maps key-wise. The keys of resulting
 map correspond to the keys that are in both maps. *)
@@ -507,7 +507,7 @@ Lemma insert_empty {A} i (x : A) : <[i:=x]>(∅ : M A) = {[i := x]}.
 Proof. done. Qed.
 Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m ≠ ∅.
 Proof.
-  intros Hi%(f_equal (!! i)). by rewrite lookup_insert, lookup_empty in Hi.
+  intros Hi%(f_equal (.!! i)). by rewrite lookup_insert, lookup_empty in Hi.
 Qed.
 
 Lemma insert_subseteq {A} (m : M A) i x : m !! i = None → m ⊆ <[i:=x]>m.
@@ -575,7 +575,7 @@ Lemma lookup_singleton_ne {A} i j (x : A) :
 Proof. by rewrite lookup_singleton_None. Qed.
 Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ≠ (∅ : M A).
 Proof.
-  intros Hix. apply (f_equal (!! i)) in Hix.
+  intros Hix. apply (f_equal (.!! i)) in Hix.
   by rewrite lookup_empty, lookup_singleton in Hix.
 Qed.
 Lemma insert_singleton {A} i (x y : A) : <[i:=y]>({[i := x]} : M A) = {[i := y]}.
@@ -1625,7 +1625,7 @@ Lemma lookup_union_None {A} (m1 m2 : M A) i :
 Proof. rewrite lookup_union.  destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
 Lemma map_positive_l {A} (m1 m2 : M A) : m1 ∪ m2 = ∅ → m1 = ∅.
 Proof.
-  intros Hm. apply map_empty. intros i. apply (f_equal (!! i)) in Hm.
+  intros Hm. apply map_empty. intros i. apply (f_equal (.!! i)) in Hm.
   rewrite lookup_empty, lookup_union_None in Hm; tauto.
 Qed.
 Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 ≠ ∅ → m1 ∪ m2 ≠ ∅.
diff --git a/theories/finite.v b/theories/finite.v
index 154142362811dbc21560e738336f4f561c56b1a4..94e3c298eda6ddcb099823facefa36a9356b5ec6 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -18,15 +18,15 @@ Definition card A `{Finite A} := length (enum A).
 
 Program Definition finite_countable `{Finite A} : Countable A := {|
   encode := λ x,
-    Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =) (enum A);
+    Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =.) (enum A);
   decode := λ p, enum A !! pred (Pos.to_nat p)
 |}.
 Arguments Pos.of_nat : simpl never.
 Next Obligation.
   intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
-  destruct (list_find_elem_of (x =) xs x) as [[i y] Hi]; auto.
+  destruct (list_find_elem_of (x =.) xs x) as [[i y] Hi]; auto.
   rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl.
-  destruct (list_find_Some (x =) xs i y); naive_solver.
+  destruct (list_find_Some (x =.) xs i y); naive_solver.
 Qed.
 Hint Immediate finite_countable : typeclass_instances.
 
@@ -38,7 +38,7 @@ Proof.
   destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
   rewrite Nat2Pos.id by done; simpl.
   destruct (list_find _ xs) as [[i y]|] eqn:?; simpl.
-  - destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some.
+  - destruct (list_find_Some (x =.) xs i y); eauto using lookup_lt_Some.
   - destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
 Qed.
 Lemma encode_decode A `{finA: Finite A} i :
@@ -48,8 +48,8 @@ Proof.
   unfold encode_nat, decode_nat, encode, decode, card; simpl.
   intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx].
   exists x. rewrite !Nat2Pos.id by done; simpl.
-  destruct (list_find_elem_of (x =) xs x) as [[j y] Hj]; auto.
-  destruct (list_find_Some (x =) xs j y) as [? ->]; auto.
+  destruct (list_find_elem_of (x =.) xs x) as [[j y] Hj]; auto.
+  destruct (list_find_Some (x =.) xs j y) as [? ->]; auto.
   rewrite Hj; csimpl; eauto using NoDup_lookup.
 Qed.
 Lemma find_Some `{finA: Finite A} P `{∀ x, Decision (P x)} (x : A) :
@@ -282,7 +282,7 @@ Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
 Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
 
 Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
-  {| enum := foldr (λ x, (pair x <$> enum B ++)) [] (enum A) |}.
+  {| enum := foldr (λ x, (pair x <$> enum B ++.)) [] (enum A) |}.
 Next Obligation.
   intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
   { constructor. }
@@ -312,7 +312,7 @@ Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n
   fix go n :=
   match n with
   | 0 => [[]↾eq_refl]
-  | S n => foldr (λ x, (sig_map (x ::) (λ _ H, f_equal S H) <$> (go n) ++)) [] l
+  | S n => foldr (λ x, (sig_map (x ::.) (λ _ H, f_equal S H) <$> (go n) ++.)) [] l
   end.
 
 Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
diff --git a/theories/gmap.v b/theories/gmap.v
index 2edcb42d67b878e4a8177be589d69a9915c064ae..d537f882a0ccdd8872bf9dde662234cf77af8373 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -73,7 +73,7 @@ Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f m1 m2,
     (bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))).
 Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
   let (m,_) := m in omap (λ ix : positive * A,
-    let (i,x) := ix in (,x) <$> decode i) (map_to_list m).
+    let (i,x) := ix in (., x) <$> decode i) (map_to_list m).
 
 (** * Instantiation of the finite map interface *)
 Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
@@ -139,12 +139,12 @@ Section curry_uncurry.
   (* FIXME: the type annotations `option (gmap K2 A)` are silly. Maybe these are
   a consequence of Coq bug #5735 *)
   Lemma lookup_gmap_curry (m : gmap K1 (gmap K2 A)) i j :
-    gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) ≫= (!! j).
+    gmap_curry m !! (i,j) = (m !! i : option (gmap K2 A)) ≫= (.!! j).
   Proof.
-    apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i ≫= (!! j))).
+    apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i ≫= (.!! j))).
     { by rewrite !lookup_empty. }
     clear m; intros i' m2 m m12 Hi' IH.
-    apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i ≫= (!! j))).
+    apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i ≫= (.!! j))).
     { rewrite IH. destruct (decide (i' = i)) as [->|].
       - rewrite lookup_insert, Hi'; simpl; by rewrite lookup_empty.
       - by rewrite lookup_insert_ne by done. }
@@ -156,9 +156,9 @@ Section curry_uncurry.
   Qed.
 
   Lemma lookup_gmap_uncurry (m : gmap (K1 * K2) A) i j :
-    (gmap_uncurry m !! i : option (gmap K2 A)) ≫= (!! j) = m !! (i, j).
+    (gmap_uncurry m !! i : option (gmap K2 A)) ≫= (.!! j) = m !! (i, j).
   Proof.
-    apply (map_fold_ind (λ mr m, mr !! i ≫= (!! j) = m !! (i, j))).
+    apply (map_fold_ind (λ mr m, mr !! i ≫= (.!! j) = m !! (i, j))).
     { by rewrite !lookup_empty. }
     clear m; intros [i' j'] x m12 mr Hij' IH.
     destruct (decide (i = i')) as [->|].
@@ -202,7 +202,7 @@ Section curry_uncurry.
     intros Hne. apply map_eq; intros i. destruct (m !! i) as [m2|] eqn:Hm.
     - destruct (gmap_uncurry (gmap_curry m) !! i) as [m2'|] eqn:Hcurry.
       + f_equal. apply map_eq. intros j.
-        trans ((gmap_uncurry (gmap_curry m) !! i : option (gmap _ _)) ≫= (!! j)).
+        trans ((gmap_uncurry (gmap_curry m) !! i : option (gmap _ _)) ≫= (.!! j)).
         { by rewrite Hcurry. }
         by rewrite lookup_gmap_uncurry, lookup_gmap_curry, Hm.
       + rewrite lookup_gmap_uncurry_None in Hcurry.
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index d243fd369566551b38434fb62fd5cf9a386cacf7..aab6bd727bba23195e83e269e3433a4a4eaa233c 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -218,12 +218,12 @@ Qed.
 Global Instance gmultiset_disj_union_right_id : RightId (=@{gmultiset A}) ∅ (⊎).
 Proof. intros X. by rewrite (comm_L (⊎)), (left_id_L _ _). Qed.
 
-Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ⊎).
+Global Instance gmultiset_disj_union_inj_1 X : Inj (=) (=) (X ⊎.).
 Proof.
   intros Y1 Y2. rewrite !gmultiset_eq. intros HX x; generalize (HX x).
   rewrite !multiplicity_disj_union. lia.
 Qed.
-Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (⊎ X).
+Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (.⊎ X).
 Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.
 
 Lemma gmultiset_disj_union_intersection_l X Y Z : X ⊎ (Y ∩ Z) = (X ⊎ Y) ∩ (X ⊎ Z).
diff --git a/theories/hashset.v b/theories/hashset.v
index 9494fe2ec5e3b0a1d11d0d73a8fc92bfbed07949..e0211a160cb7c71524c2979715c92cf2645be23e 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -129,7 +129,7 @@ Definition remove_dups_fast (l : list A) : list A :=
   | [x] => [x]
   | _ =>
      let n : Z := length l in
-     elements (foldr (λ x, ({[ x ]} ∪)) ∅ l :
+     elements (foldr (λ x, ({[ x ]} ∪.)) ∅ l :
        hashset (λ x, hash x `mod` (2 * n))%Z)
   end.
 Lemma elem_of_remove_dups_fast l x : x ∈ remove_dups_fast l ↔ x ∈ l.
diff --git a/theories/infinite.v b/theories/infinite.v
index 47c50e3bbd76f387da24e8ecd676460112c67db1..232304f6b55e3db2548bdc23ba19b4119450e174 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -35,7 +35,7 @@ Section search_infinite.
   Lemma search_infinite_R_wf xs : wf (R xs).
   Proof.
     revert xs. assert (help : ∀ xs n n',
-      Acc (R (filter (≠ f n') xs)) n → n' < n → Acc (R xs) n).
+      Acc (R (filter (.≠ f n') xs)) n → n' < n → Acc (R xs) n).
     { induction 1 as [n _ IH]. constructor; intros n2 [??]. apply IH; [|lia].
       split; [done|]. apply elem_of_list_filter; naive_solver lia. }
     intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH].
@@ -127,9 +127,9 @@ Instance sum_infinite_r {A} `{Infinite B} : Infinite (A + B) :=
   inj_infinite inr (maybe inr)  (λ _, eq_refl).
 
 Instance prod_infinite_l `{Infinite A, Inhabited B} : Infinite (A * B) :=
-  inj_infinite (,inhabitant) (Some ∘ fst) (λ _, eq_refl).
+  inj_infinite (., inhabitant) (Some ∘ fst) (λ _, eq_refl).
 Instance prod_infinite_r `{Inhabited A, Infinite B} : Infinite (A * B) :=
-  inj_infinite (inhabitant,) (Some ∘ snd) (λ _, eq_refl).
+  inj_infinite (inhabitant ,.) (Some ∘ snd) (λ _, eq_refl).
 
 (** Instance for lists *)
 Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
diff --git a/theories/list.v b/theories/list.v
index c53e23b65108710db0fd8ec870431b3104fba567..ec400bbbe313070f7d86c4780f3bff7dc6388d5a 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -33,20 +33,20 @@ Arguments Forall_cons {_} _ _ _ _ _ : assert.
 Remove Hints Permutation_cons : typeclass_instances.
 
 Notation "(::)" := cons (only parsing) : list_scope.
-Notation "( x ::)" := (cons x) (only parsing) : list_scope.
-Notation "(:: l )" := (λ x, cons x l) (only parsing) : list_scope.
+Notation "( x ::.)" := (cons x) (only parsing) : list_scope.
+Notation "(.:: l )" := (λ x, cons x l) (only parsing) : list_scope.
 Notation "(++)" := app (only parsing) : list_scope.
-Notation "( l ++)" := (app l) (only parsing) : list_scope.
-Notation "(++ k )" := (λ l, app l k) (only parsing) : list_scope.
+Notation "( l ++.)" := (app l) (only parsing) : list_scope.
+Notation "(.++ k )" := (λ l, app l k) (only parsing) : list_scope.
 
 Infix "≡ₚ" := Permutation (at level 70, no associativity) : stdpp_scope.
 Notation "(≡ₚ)" := Permutation (only parsing) : stdpp_scope.
-Notation "( x ≡ₚ)" := (Permutation x) (only parsing) : stdpp_scope.
-Notation "(≡ₚ x )" := (λ y, y ≡ₚ x) (only parsing) : stdpp_scope.
+Notation "( x ≡ₚ.)" := (Permutation x) (only parsing) : stdpp_scope.
+Notation "(.≡ₚ x )" := (λ y, y ≡ₚ x) (only parsing) : stdpp_scope.
 Notation "(≢ₚ)" := (λ x y, ¬x ≡ₚ y) (only parsing) : stdpp_scope.
 Notation "x ≢ₚ y":= (¬x ≡ₚ y) (at level 70, no associativity) : stdpp_scope.
-Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : stdpp_scope.
-Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : stdpp_scope.
+Notation "( x ≢ₚ.)" := (λ y, x ≢ₚ y) (only parsing) : stdpp_scope.
+Notation "(.≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : stdpp_scope.
 
 Infix "≡ₚ@{ A }" :=
   (@Permutation A) (at level 70, no associativity, only parsing) : stdpp_scope.
@@ -237,7 +237,7 @@ Fixpoint mask {A} (f : A → A) (βs : list bool) (l : list A) : list A :=
 (** The function [permutations l] yields all permutations of [l]. *)
 Fixpoint interleave {A} (x : A) (l : list A) : list (list A) :=
   match l with
-  | [] => [[x]]| y :: l => (x :: y :: l) :: ((y ::) <$> interleave x l)
+  | [] => [[x]]| y :: l => (x :: y :: l) :: ((y ::.) <$> interleave x l)
   end.
 Fixpoint permutations {A} (l : list A) : list (list A) :=
   match l with [] => [[]] | x :: l => permutations l ≫= interleave x end.
@@ -261,7 +261,7 @@ Section prefix_suffix_ops.
     | l1, [] => (l1, [], [])
     | x1 :: l1, x2 :: l2 =>
       if decide_rel (=) x1 x2
-      then prod_map id (x1 ::) (go l1 l2) else (x1 :: l1, x2 :: l2, [])
+      then prod_map id (x1 ::.) (go l1 l2) else (x1 :: l1, x2 :: l2, [])
     end.
   Definition max_suffix (l1 l2 : list A) : list A * list A * list A :=
     match max_prefix (reverse l1) (reverse l2) with
@@ -296,7 +296,7 @@ Hint Extern 0 (_ ⊆+ _) => reflexivity : core.
 Fixpoint list_remove `{EqDecision A} (x : A) (l : list A) : option (list A) :=
   match l with
   | [] => None
-  | y :: l => if decide (x = y) then Some l else (y ::) <$> list_remove x l
+  | y :: l => if decide (x = y) then Some l else (y ::.) <$> list_remove x l
   end.
 
 (** Removes all elements in the list [k] from the list [l]. The function returns
@@ -352,7 +352,7 @@ Section list_set.
     match l with
     | [] => []
     | x :: l => foldr (λ y,
-        match f x y with None => id | Some z => (z ::) end) (go l k) k
+        match f x y with None => id | Some z => (z ::.) end) (go l k) k
     end.
 End list_set.
 
@@ -442,9 +442,9 @@ Implicit Types l k : list A.
 
 Global Instance: Inj2 (=) (=) (=) (@cons A).
 Proof. by injection 1. Qed.
-Global Instance: ∀ k, Inj (=) (=) (k ++).
+Global Instance: ∀ k, Inj (=) (=) (k ++.).
 Proof. intros ???. apply app_inv_head. Qed.
-Global Instance: ∀ k, Inj (=) (=) (++ k).
+Global Instance: ∀ k, Inj (=) (=) (.++ k).
 Proof. intros ???. apply app_inv_tail. Qed.
 Global Instance: Assoc (=) (@app A).
 Proof. intros ???. apply app_assoc. Qed.
@@ -728,7 +728,7 @@ Lemma not_elem_of_app l1 l2 x : x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2.
 Proof. rewrite elem_of_app. tauto. Qed.
 Lemma elem_of_list_singleton x y : x ∈ [y] ↔ x = y.
 Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.
-Global Instance elem_of_list_permutation_proper x : Proper ((≡ₚ) ==> iff) (x ∈).
+Global Instance elem_of_list_permutation_proper x : Proper ((≡ₚ) ==> iff) (x ∈.).
 Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
 Lemma elem_of_list_split l x : x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2.
 Proof.
@@ -1370,7 +1370,7 @@ Proof.
   rewrite (Nat.mul_comm _ n) in Hlookup.
   unfold sublist_lookup in *; simplify_option_eq;
     [|by rewrite !lookup_ge_None_2 by auto].
-  apply (f_equal (!! i `mod` n)) in Hlookup.
+  apply (f_equal (.!! i `mod` n)) in Hlookup.
   by rewrite !lookup_take, !lookup_drop, <-!Nat.div_mod in Hlookup
     by (auto using Nat.mod_upper_bound with lia).
 Qed.
@@ -1611,15 +1611,15 @@ Proof.
   - by rewrite (right_id_L [] (++)).
   - rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
 Qed.
-Global Instance: ∀ x : A, Inj (≡ₚ) (≡ₚ) (x ::).
+Global Instance: ∀ x : A, Inj (≡ₚ) (≡ₚ) (x ::.).
 Proof. red. eauto using Permutation_cons_inv. Qed.
-Global Instance: ∀ k : list A, Inj (≡ₚ) (≡ₚ) (k ++).
+Global Instance: ∀ k : list A, Inj (≡ₚ) (≡ₚ) (k ++.).
 Proof.
   red. induction k as [|x k IH]; intros l1 l2; simpl; auto.
-  intros. by apply IH, (inj (x ::)).
+  intros. by apply IH, (inj (x ::.)).
 Qed.
-Global Instance: ∀ k : list A, Inj (≡ₚ) (≡ₚ) (++ k).
-Proof. intros k l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++)). Qed.
+Global Instance: ∀ k : list A, Inj (≡ₚ) (≡ₚ) (.++ k).
+Proof. intros k l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++.)). Qed.
 Lemma replicate_Permutation n x l : replicate n x ≡ₚ l → replicate n x = l.
 Proof.
   intros Hl. apply replicate_as_elem_of. split.
@@ -1646,7 +1646,7 @@ Proof.
   { apply elem_of_list_lookup. rewrite Hk, elem_of_cons; auto. }
   exists (take i k), (drop (S i) k). split.
   - by rewrite take_drop_middle.
-  - rewrite <-delete_take_drop. apply (inj (x ::)).
+  - rewrite <-delete_take_drop. apply (inj (x ::.)).
     by rewrite <-Hk, <-(delete_Permutation k) by done.
 Qed.
 
@@ -2488,7 +2488,7 @@ Section Forall_Exists.
   Qed.
   Lemma Forall_replicate n x : P x → Forall P (replicate n x).
   Proof. induction n; simpl; constructor; auto. Qed.
-  Lemma Forall_replicate_eq n (x : A) : Forall (x =) (replicate n x).
+  Lemma Forall_replicate_eq n (x : A) : Forall (x =.) (replicate n x).
   Proof using -(P). induction n; simpl; constructor; auto. Qed.
   Lemma Forall_take n l : Forall P l → Forall P (take n l).
   Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
@@ -2606,10 +2606,10 @@ Lemma existb_True (f : A → bool) xs : existsb f xs ↔ Exists f xs.
 Proof. split. induction xs; naive_solver. induction 1; naive_solver. Qed.
 
 Lemma replicate_as_Forall (x : A) n l :
-  replicate n x = l ↔ length l = n ∧ Forall (x =) l.
+  replicate n x = l ↔ length l = n ∧ Forall (x =.) l.
 Proof. rewrite replicate_as_elem_of, Forall_forall. naive_solver. Qed.
 Lemma replicate_as_Forall_2 (x : A) n l :
-  length l = n → Forall (x =) l → replicate n x = l.
+  length l = n → Forall (x =.) l → replicate n x = l.
 Proof. by rewrite replicate_as_Forall. Qed.
 End more_general_properties.
 
@@ -3392,14 +3392,14 @@ Section ret_join.
   Lemma elem_of_list_join (x : A) (ls : list (list A)) :
     x ∈ mjoin ls ↔ ∃ l : list A, x ∈ l ∧ l ∈ ls.
   Proof. by rewrite list_join_bind, elem_of_list_bind. Qed.
-  Lemma join_nil (ls : list (list A)) : mjoin ls = [] ↔ Forall (= []) ls.
+  Lemma join_nil (ls : list (list A)) : mjoin ls = [] ↔ Forall (.= []) ls.
   Proof.
     split; [|by induction 1 as [|[|??] ?]].
     by induction ls as [|[|??] ?]; constructor; auto.
   Qed.
-  Lemma join_nil_1 (ls : list (list A)) : mjoin ls = [] → Forall (= []) ls.
+  Lemma join_nil_1 (ls : list (list A)) : mjoin ls = [] → Forall (.= []) ls.
   Proof. by rewrite join_nil. Qed.
-  Lemma join_nil_2 (ls : list (list A)) : Forall (= []) ls → mjoin ls = [].
+  Lemma join_nil_2 (ls : list (list A)) : Forall (.= []) ls → mjoin ls = [].
   Proof. by rewrite join_nil. Qed.
   Lemma Forall_join (P : A → Prop) (ls: list (list A)) :
     Forall (Forall P) ls → Forall P (mjoin ls).
@@ -4008,7 +4008,7 @@ Section positives_flatten_unflatten.
       intros p1 p2 [|y ys] ?; simplify_eq/=; auto.
     rewrite !positives_flatten_cons, !(assoc _); intros Hl.
     assert (xs = ys) as <- by eauto; clear IH H; f_equal.
-    apply (inj (++ positives_flatten xs)) in Hl.
+    apply (inj (.++ positives_flatten xs)) in Hl.
     rewrite 2!Preverse_Pdup in Hl.
     apply (Pdup_suffix_eq _ _ p1 p2) in Hl.
     by apply (inj Preverse).
@@ -4018,7 +4018,7 @@ End positives_flatten_unflatten.
 (** * Relection over lists *)
 (** We define a simple data structure [rlist] to capture a syntactic
 representation of lists consisting of constants, applications and the nil list.
-Note that we represent [(x ::)] as [rapp (rnode [x])]. For now, we abstract
+Note that we represent [(x ::.)] as [rapp (rnode [x])]. For now, we abstract
 over the type of constants, but later we use [nat]s and a list representing
 a corresponding environment. *)
 Inductive rlist (A : Type) :=
@@ -4071,7 +4071,7 @@ End quote.
 Section eval.
   Context {A} (E : env A).
 
-  Lemma eval_alt t : eval E t = to_list t ≫= default [] ∘ (E !!).
+  Lemma eval_alt t : eval E t = to_list t ≫= default [] ∘ (E !!.).
   Proof.
     induction t; csimpl.
     - done.
diff --git a/theories/numbers.v b/theories/numbers.v
index 7ecce34d2558d5d10839a95079e11fe2eb1e4c71..0fcde178b41ce94425a4788b3db71b43e8156388 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -170,8 +170,8 @@ Fixpoint Papp (p1 p2 : positive) : positive :=
   end.
 Infix "++" := Papp : positive_scope.
 Notation "(++)" := Papp (only parsing) : positive_scope.
-Notation "( p ++)" := (Papp p) (only parsing) : positive_scope.
-Notation "(++ q )" := (λ p, Papp p q) (only parsing) : positive_scope.
+Notation "( p ++.)" := (Papp p) (only parsing) : positive_scope.
+Notation "(.++ q )" := (λ p, Papp p q) (only parsing) : positive_scope.
 
 Fixpoint Preverse_go (p1 p2 : positive) : positive :=
   match p2 with
@@ -187,7 +187,7 @@ Global Instance Papp_1_r : RightId (=) 1 (++).
 Proof. done. Qed.
 Global Instance Papp_assoc : Assoc (=) (++).
 Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
-Global Instance Papp_inj p : Inj (=) (=) (++ p).
+Global Instance Papp_inj p : Inj (=) (=) (.++ p).
 Proof. intros ???. induction p; simplify_eq; auto. Qed.
 
 Lemma Preverse_go_app p1 p2 p3 :
diff --git a/theories/pmap.v b/theories/pmap.v
index ff4b6b55ca64e3d016336f7582f3eca48b0592cc..088ebcb8a4106c468180f69fa966e95dee5090a8 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -224,14 +224,14 @@ Proof.
     apply IHl.
     { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
       + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
-        by apply (inj (++ _)) in Hi.
+        by apply (inj (.++ _)) in Hi.
       + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
     apply IHr; auto. intros i x Hi.
     apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
   - apply IHl.
     { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
       + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
-        by apply (inj (++ _)) in Hi.
+        by apply (inj (.++ _)) in Hi.
       + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
     apply IHr; auto. intros i x Hi.
     apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
diff --git a/theories/sets.v b/theories/sets.v
index b2ef0b20d7f359cc29cf6ecc5e7d58a5bf88573a..64b852b87a085d072474f1e09a546ad6f5cd4fc9 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -485,7 +485,7 @@ Section semi_set.
   Qed.
   Lemma union_list_mono Xs Ys : Xs ⊆* Ys → ⋃ Xs ⊆ ⋃ Ys.
   Proof. induction 1; simpl; auto using union_mono. Qed.
-  Lemma empty_union_list Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs.
+  Lemma empty_union_list Xs : ⋃ Xs ≡ ∅ ↔ Forall (.≡ ∅) Xs.
   Proof.
     split.
     - induction Xs; simpl; rewrite ?empty_union; intuition.
@@ -554,7 +554,7 @@ Section semi_set.
     Proof. unfold_leibniz. apply union_list_app. Qed.
     Lemma union_list_reverse_L Xs : ⋃ (reverse Xs) = ⋃ Xs.
     Proof. unfold_leibniz. apply union_list_reverse. Qed.
-    Lemma empty_union_list_L Xs : ⋃ Xs = ∅ ↔ Forall (= ∅) Xs.
+    Lemma empty_union_list_L Xs : ⋃ Xs = ∅ ↔ Forall (.= ∅) Xs.
     Proof. unfold_leibniz. by rewrite empty_union_list. Qed. 
   End leibniz.
 
@@ -567,7 +567,7 @@ Section semi_set.
 
     Lemma non_empty_union X Y : X ∪ Y ≢ ∅ ↔ X ≢ ∅ ∨ Y ≢ ∅.
     Proof. rewrite empty_union. destruct (decide (X ≡ ∅)); intuition. Qed.
-    Lemma non_empty_union_list Xs : ⋃ Xs ≢ ∅ → Exists (≢ ∅) Xs.
+    Lemma non_empty_union_list Xs : ⋃ Xs ≢ ∅ → Exists (.≢ ∅) Xs.
     Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.
 
     Context `{!LeibnizEquiv C}.
@@ -577,7 +577,7 @@ Section semi_set.
     Proof. unfold_leibniz. apply set_not_subset_inv. Qed.
     Lemma non_empty_union_L X Y : X ∪ Y ≠ ∅ ↔ X ≠ ∅ ∨ Y ≠ ∅.
     Proof. unfold_leibniz. apply non_empty_union. Qed.
-    Lemma non_empty_union_list_L Xs : ⋃ Xs ≠ ∅ → Exists (≠ ∅) Xs.
+    Lemma non_empty_union_list_L Xs : ⋃ Xs ≠ ∅ → Exists (.≠ ∅) Xs.
     Proof. unfold_leibniz. apply non_empty_union_list. Qed.
   End dec.
 End semi_set.
@@ -973,10 +973,10 @@ End set_monad.
 
 (** Finite sets *)
 Definition pred_finite {A} (P : A → Prop) := ∃ xs : list A, ∀ x, P x → x ∈ xs.
-Definition set_finite `{ElemOf A B} (X : B) := pred_finite (∈ X).
+Definition set_finite `{ElemOf A B} (X : B) := pred_finite (.∈ X).
 
 Definition pred_infinite {A} (P : A → Prop) := ∀ xs : list A, ∃ x, P x ∧ x ∉ xs.
-Definition set_infinite `{ElemOf A C} (X : C) := pred_infinite (∈ X).
+Definition set_infinite `{ElemOf A C} (X : C) := pred_infinite (.∈ X).
 
 Section pred_finite_infinite.
   Lemma pred_finite_impl {A} (P Q : A → Prop) :
diff --git a/theories/sorting.v b/theories/sorting.v
index 27cb04e9b4d0c4c8eca6b17da85f730ef87f66ac..4cd58672a5804daa23b83c6b941a47731d28eeae 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -85,7 +85,7 @@ Section sorted.
       assert (x2 ∈ x1 :: l1) as Hx2' by (by rewrite E; left).
       assert (x1 ∈ x2 :: l2) as Hx1' by (by rewrite <-E; left).
       inversion Hx1'; inversion Hx2'; simplify_eq; auto. }
-    f_equal. by apply IH, (inj (x2 ::)).
+    f_equal. by apply IH, (inj (x2 ::.)).
   Qed.
   Lemma Sorted_unique `{!Transitive R, !AntiSymm (=) R} l1 l2 :
     Sorted R l1 → Sorted R l2 → l1 ≡ₚ l2 → l1 = l2.
diff --git a/theories/vector.v b/theories/vector.v
index 4f9e7ddaa05f3e61c1b2c8723658f1e05b443030..9ca8ed4e658b7f7fa72092c5f1974ca440e92f47 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -21,15 +21,15 @@ Arguments vcons {_} _ {_} _.
 
 Infix ":::" := vcons (at level 60, right associativity) : vector_scope.
 Notation "(:::)" := vcons (only parsing) : vector_scope.
-Notation "( x :::)" := (vcons x) (only parsing) : vector_scope.
-Notation "(::: v )" := (λ x, vcons x v) (only parsing) : vector_scope.
+Notation "( x :::.)" := (vcons x) (only parsing) : vector_scope.
+Notation "(.::: v )" := (λ x, vcons x v) (only parsing) : vector_scope.
 Notation "[# ] " := vnil : vector_scope.
 Notation "[# x ] " := (vcons x vnil) : vector_scope.
 Notation "[# x ; .. ; y ] " := (vcons x .. (vcons y vnil) ..) : vector_scope.
 Infix "+++" := vapp (at level 60, right associativity) : vector_scope.
 Notation "(+++)" := vapp (only parsing) : vector_scope.
-Notation "( v +++)" := (vapp v) (only parsing) : vector_scope.
-Notation "(+++ w )" := (λ v, vapp v w) (only parsing) : vector_scope.
+Notation "( v +++.)" := (vapp v) (only parsing) : vector_scope.
+Notation "(.+++ w )" := (λ v, vapp v w) (only parsing) : vector_scope.
 
 (** Notice that we cannot define [Vector.nth] as an instance of our [Lookup]
 type class, as it has a dependent type. *)