From 6aba4a3fe96dab179890ab9a7073cbea4238963e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 5 Apr 2018 11:12:16 +0200
Subject: [PATCH] =?UTF-8?q?Notations=20`=3D@{A}`=20and=20`=E2=89=A1@{A}`?=
 =?UTF-8?q?=20for=20being=20explicit=20about=20the=20type=20of=20(setoid)?=
 =?UTF-8?q?=20equality.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This followed from discussions in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/134
---
 theories/base.v        | 33 +++++++++++++------
 theories/coPset.v      |  2 +-
 theories/collections.v | 75 +++++++++++++++++++++---------------------
 theories/fin_maps.v    | 62 ++++++++++++++++------------------
 theories/gmultiset.v   | 10 +++---
 theories/list.v        | 47 +++++++++++++-------------
 theories/mapset.v      |  2 +-
 theories/option.v      | 26 +++++++--------
 theories/pmap.v        |  4 +--
 theories/pretty.v      |  4 +--
 theories/streams.v     |  8 ++---
 theories/tactics.v     |  2 +-
 12 files changed, 140 insertions(+), 135 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index c0733e1f..d4005a4d 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -159,10 +159,16 @@ 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.
 
+Infix "=@{ A }" := (@eq A)
+  (at level 70, only parsing, no associativity) : stdpp_scope.
+Notation "(=@{ A } )" := (@eq A) (only parsing) : stdpp_scope.
+Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope.
+Notation "X ≠@{ A } Y":= (¬X =@{ A } Y) (at level 70, no associativity) : stdpp_scope.
+
 Hint Extern 0 (_ = _) => reflexivity.
 Hint Extern 100 (_ ≠ _) => discriminate.
 
-Instance: @PreOrder A (=).
+Instance: ∀ A, PreOrder (=@{A}).
 Proof. split; repeat intro; congruence. Qed.
 
 (** ** Setoid equality *)
@@ -174,6 +180,9 @@ Class Equiv A := equiv: relation A.
 Hint Mode Equiv ! : typeclass_instances. *)
 
 Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
+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.
@@ -182,6 +191,10 @@ 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 "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope.
+Notation "(≢@{ A } )" := (λ X Y, ¬X ≡@{A} Y) (only parsing) : stdpp_scope.
+Notation "X ≢@{ A } Y":= (¬X ≡@{ A } Y) (at level 70, no associativity) : stdpp_scope.
+
 (** The type class [LeibnizEquiv] collects setoid equalities that coincide
 with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
 setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
@@ -189,22 +202,22 @@ reverse. *)
 Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x ≡ y → x = y.
 Hint Mode LeibnizEquiv ! - : typeclass_instances.
 
-Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@equiv A _)} (x y : A) :
+Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) :
   x ≡ y ↔ x = y.
 Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
 
 Ltac fold_leibniz := repeat
   match goal with
-  | H : context [ @equiv ?A _ _ _ ] |- _ =>
+  | H : context [ _ ≡@{?A} _ ] |- _ =>
     setoid_rewrite (leibniz_equiv_iff (A:=A)) in H
-  | |- context [ @equiv ?A _ _ _ ] =>
+  | |- context [ _ ≡@{?A} _ ] =>
     setoid_rewrite (leibniz_equiv_iff (A:=A))
   end.
 Ltac unfold_leibniz := repeat
   match goal with
-  | H : context [ @eq ?A _ _ ] |- _ =>
+  | H : context [ _ =@{?A} _ ] |- _ =>
     setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H
-  | |- context [ @eq ?A _ _ ] =>
+  | |- context [ _ =@{?A} _ ] =>
     setoid_rewrite <-(leibniz_equiv_iff (A:=A))
   end.
 
@@ -249,7 +262,7 @@ Class RelDecision {A B} (R : A → B → Prop) :=
   decide_rel x y :> Decision (R x y).
 Hint Mode RelDecision ! ! ! : typeclass_instances.
 Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
-Notation EqDecision A := (RelDecision (@eq A)).
+Notation EqDecision A := (RelDecision (=@{A})).
 
 (** ** Inhabited types *)
 (** This type class collects types that are inhabited. *)
@@ -411,9 +424,9 @@ Lemma exist_proper {A} (P Q : A → Prop) :
   (∀ x, P x ↔ Q x) → (∃ x, P x) ↔ (∃ x, Q x).
 Proof. firstorder. Qed.
 
-Instance: Comm (↔) (@eq A).
+Instance: Comm (↔) (=@{A}).
 Proof. red; intuition. Qed.
-Instance: Comm (↔) (λ x y, @eq A y x).
+Instance: Comm (↔) (λ x y, y =@{A} x).
 Proof. red; intuition. Qed.
 Instance: Comm (↔) (↔).
 Proof. red; intuition. Qed.
@@ -551,7 +564,7 @@ Proof. now intros -> ?. Qed.
 
 (** ** Unit *)
 Instance unit_equiv : Equiv unit := λ _ _, True.
-Instance unit_equivalence : Equivalence (@equiv unit _).
+Instance unit_equivalence : Equivalence (≡@{unit}).
 Proof. repeat split. Qed.
 Instance unit_leibniz : LeibnizEquiv unit.
 Proof. intros [] []; reflexivity. Qed.
diff --git a/theories/coPset.v b/theories/coPset.v
index 6110295d..5c027492 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -192,7 +192,7 @@ Qed.
 
 Instance coPset_elem_of_dec : RelDecision (@elem_of _ coPset _).
 Proof. solve_decision. Defined.
-Instance coPset_equiv_dec : RelDecision (@equiv coPset _).
+Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
 Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
 Instance mapset_disjoint_dec : RelDecision (@disjoint coPset _).
 Proof.
diff --git a/theories/collections.v b/theories/collections.v
index a650917f..93f3d435 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -19,14 +19,14 @@ Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint.
 Section setoids_simple.
   Context `{SimpleCollection A C}.
 
-  Global Instance collection_equivalence: @Equivalence C (≡).
+  Global Instance collection_equivalence : Equivalence (≡@{C}).
   Proof.
     split.
     - done.
     - intros X Y ? x. by symmetry.
     - intros X Y Z ?? x; by trans (x ∈ Y).
   Qed.
-  Global Instance singleton_proper : Proper ((=) ==> (≡)) (singleton (B:=C)).
+  Global Instance singleton_proper : Proper ((=) ==> (≡@{C})) singleton.
   Proof. apply _. Qed.
   Global Instance elem_of_proper :
     Proper ((=) ==> (≡) ==> iff) (@elem_of A C _) | 5.
@@ -35,11 +35,11 @@ Section setoids_simple.
   Proof.
     intros X1 X2 HX Y1 Y2 HY; apply forall_proper; intros x. by rewrite HX, HY.
   Qed.
-  Global Instance union_proper : Proper ((≡) ==> (≡) ==> (≡)) (@union C _).
+  Global Instance union_proper : Proper ((≡) ==> (≡) ==> (≡@{C})) union.
   Proof. intros X1 X2 HX Y1 Y2 HY x. rewrite !elem_of_union. f_equiv; auto. Qed.
-  Global Instance union_list_proper: Proper ((≡) ==> (≡)) (union_list (A:=C)).
+  Global Instance union_list_proper: Proper ((≡) ==> (≡@{C})) union_list.
   Proof. by induction 1; simpl; try apply union_proper. Qed.
-  Global Instance subseteq_proper : Proper ((≡) ==> (≡) ==> iff) ((⊆) : relation C).
+  Global Instance subseteq_proper : Proper ((≡@{C}) ==> (≡@{C}) ==> iff) (⊆).
   Proof.
     intros X1 X2 HX Y1 Y2 HY. apply forall_proper; intros x. by rewrite HX, HY.
   Qed.
@@ -50,12 +50,12 @@ Section setoids.
 
   (** * Setoids *)
   Global Instance intersection_proper :
-    Proper ((≡) ==> (≡) ==> (≡)) (@intersection C _).
+    Proper ((≡) ==> (≡) ==> (≡@{C})) intersection.
   Proof.
     intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_intersection, HX, HY.
   Qed.
   Global Instance difference_proper :
-     Proper ((≡) ==> (≡) ==> (≡)) (@difference C _).
+     Proper ((≡) ==> (≡) ==> (≡@{C})) difference.
   Proof.
     intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_difference, HX, HY.
   Qed.
@@ -357,15 +357,15 @@ Section simple_collection.
   Lemma union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∪ Y1 ⊆ X2 ∪ Y2.
   Proof. set_solver. Qed.
 
-  Global Instance union_idemp : IdemP ((≡) : relation C) (∪).
+  Global Instance union_idemp : IdemP (≡@{C}) (∪).
   Proof. intros X. set_solver. Qed.
-  Global Instance union_empty_l : LeftId ((≡) : relation C) ∅ (∪).
+  Global Instance union_empty_l : LeftId (≡@{C}) ∅ (∪).
   Proof. intros X. set_solver. Qed.
-  Global Instance union_empty_r : RightId ((≡) : relation C) ∅ (∪).
+  Global Instance union_empty_r : RightId (≡@{C}) ∅ (∪).
   Proof. intros X. set_solver. Qed.
-  Global Instance union_comm : Comm ((≡) : relation C) (∪).
+  Global Instance union_comm : Comm (≡@{C}) (∪).
   Proof. intros X Y. set_solver. Qed.
-  Global Instance union_assoc : Assoc ((≡) : relation C) (∪).
+  Global Instance union_assoc : Assoc (≡@{C}) (∪).
   Proof. intros X Y Z. set_solver. Qed.
 
   Lemma empty_union X Y : X ∪ Y ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅.
@@ -480,15 +480,15 @@ Section simple_collection.
     Proof. unfold_leibniz. apply subseteq_union_2. Qed.
 
     (** Union *)
-    Global Instance union_idemp_L : IdemP (@eq C) (∪).
+    Global Instance union_idemp_L : IdemP (=@{C}) (∪).
     Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
-    Global Instance union_empty_l_L : LeftId (@eq C) ∅ (∪).
+    Global Instance union_empty_l_L : LeftId (=@{C}) ∅ (∪).
     Proof. intros ?. unfold_leibniz. apply (left_id _ _). Qed.
-    Global Instance union_empty_r_L : RightId (@eq C) ∅ (∪).
+    Global Instance union_empty_r_L : RightId (=@{C}) ∅ (∪).
     Proof. intros ?. unfold_leibniz. apply (right_id _ _). Qed.
-    Global Instance union_comm_L : Comm (@eq C) (∪).
+    Global Instance union_comm_L : Comm (=@{C}) (∪).
     Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
-    Global Instance union_assoc_L : Assoc (@eq C) (∪).
+    Global Instance union_assoc_L : Assoc (=@{C}) (∪).
     Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.
 
     Lemma empty_union_L X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅.
@@ -527,7 +527,7 @@ Section simple_collection.
   End leibniz.
 
   Section dec.
-    Context `{!RelDecision (@equiv C _)}.
+    Context `{!RelDecision (≡@{C})}.
     Lemma collection_subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y.
     Proof. destruct (decide (X ≡ Y)); [by right|left;set_solver]. Qed.
     Lemma collection_not_subset_inv X Y : X ⊄ Y → X ⊈ Y ∨ X ≡ Y.
@@ -580,15 +580,15 @@ Section collection.
     X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∩ Y1 ⊆ X2 ∩ Y2.
   Proof. set_solver. Qed.
 
-  Global Instance intersection_idemp : IdemP ((≡) : relation C) (∩).
+  Global Instance intersection_idemp : IdemP (≡@{C}) (∩).
   Proof. intros X; set_solver. Qed.
-  Global Instance intersection_comm : Comm ((≡) : relation C) (∩).
+  Global Instance intersection_comm : Comm (≡@{C}) (∩).
   Proof. intros X Y; set_solver. Qed.
-  Global Instance intersection_assoc : Assoc ((≡) : relation C) (∩).
+  Global Instance intersection_assoc : Assoc (≡@{C}) (∩).
   Proof. intros X Y Z; set_solver. Qed.
-  Global Instance intersection_empty_l : LeftAbsorb ((≡) : relation C) ∅ (∩).
+  Global Instance intersection_empty_l : LeftAbsorb (≡@{C}) ∅ (∩).
   Proof. intros X; set_solver. Qed.
-  Global Instance intersection_empty_r: RightAbsorb ((≡) : relation C) ∅ (∩).
+  Global Instance intersection_empty_r: RightAbsorb (≡@{C}) ∅ (∩).
   Proof. intros X; set_solver. Qed.
 
   Lemma intersection_singletons x : ({[x]} : C) ∩ {[x]} ≡ {[x]}.
@@ -647,15 +647,15 @@ Section collection.
     Lemma subseteq_intersection_2_L X Y : X ∩ Y = X → X ⊆ Y.
     Proof. unfold_leibniz. apply subseteq_intersection_2. Qed.
 
-    Global Instance intersection_idemp_L : IdemP ((=) : relation C) (∩).
+    Global Instance intersection_idemp_L : IdemP (=@{C}) (∩).
     Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
-    Global Instance intersection_comm_L : Comm ((=) : relation C) (∩).
+    Global Instance intersection_comm_L : Comm (=@{C}) (∩).
     Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
-    Global Instance intersection_assoc_L : Assoc ((=) : relation C) (∩).
+    Global Instance intersection_assoc_L : Assoc (=@{C}) (∩).
     Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.
-    Global Instance intersection_empty_l_L: LeftAbsorb ((=) : relation C) ∅ (∩).
+    Global Instance intersection_empty_l_L: LeftAbsorb (=@{C}) ∅ (∩).
     Proof. intros ?. unfold_leibniz. apply (left_absorb _ _). Qed.
-    Global Instance intersection_empty_r_L: RightAbsorb ((=) : relation C) ∅ (∩).
+    Global Instance intersection_empty_r_L: RightAbsorb (=@{C}) ∅ (∩).
     Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed.
 
     Lemma intersection_singletons_L x : {[x]} ∩ {[x]} = ({[x]} : C).
@@ -776,17 +776,17 @@ Section of_option_list.
     SetUnfold (x ∈ l) P → SetUnfold (x ∈ of_list (C:=C) l) P.
   Proof. constructor. by rewrite elem_of_of_list, (set_unfold (x ∈ l) P). Qed.
 
-  Lemma of_list_nil : of_list (C:=C) [] = ∅.
+  Lemma of_list_nil : of_list [] =@{C} ∅.
   Proof. done. Qed.
-  Lemma of_list_cons x l : of_list (C:=C) (x :: l) = {[ x ]} ∪ of_list l.
+  Lemma of_list_cons x l : of_list (x :: l) =@{C} {[ x ]} ∪ of_list l.
   Proof. done. Qed.
-  Lemma of_list_app l1 l2 : of_list (C:=C) (l1 ++ l2) ≡ of_list l1 ∪ of_list l2.
+  Lemma of_list_app l1 l2 : of_list (l1 ++ l2) ≡@{C} of_list l1 ∪ of_list l2.
   Proof. set_solver. Qed.
   Global Instance of_list_perm : Proper ((≡ₚ) ==> (≡)) (of_list (C:=C)).
   Proof. induction 1; set_solver. Qed.
 
   Context `{!LeibnizEquiv C}.
-  Lemma of_list_app_L l1 l2 : of_list (C:=C) (l1 ++ l2) = of_list l1 ∪ of_list l2.
+  Lemma of_list_app_L l1 l2 : of_list (l1 ++ l2) =@{C} of_list l1 ∪ of_list l2.
   Proof. set_solver. Qed.
   Global Instance of_list_perm_L : Proper ((≡ₚ) ==> (=)) (of_list (C:=C)).
   Proof. induction 1; set_solver. Qed.
@@ -887,10 +887,9 @@ Section fresh.
   Context `{FreshSpec A C}.
   Implicit Types X Y : C.
 
-  Global Instance fresh_proper: Proper ((≡) ==> (=)) (fresh (C:=C)).
+  Global Instance fresh_proper: Proper ((≡@{C}) ==> (=)) fresh.
   Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
-  Global Instance fresh_list_proper n:
-    Proper ((≡) ==> (=)) (fresh_list (C:=C) n).
+  Global Instance fresh_list_proper n : Proper ((≡@{C}) ==> (=)) (fresh_list n).
   Proof. induction n as [|n IH]; intros ?? E; by setoid_subst. Qed.
 
   Lemma exist_fresh X : ∃ x, x ∉ X.
@@ -1058,13 +1057,13 @@ Section seq_set.
   Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed.
 
   Lemma seq_set_S_union start len :
-    seq_set start (C:=C) (S len) ≡ {[ start + len ]} ∪ seq_set start len.
+    seq_set start (S len) ≡@{C} {[ start + len ]} ∪ seq_set start len.
   Proof.
     intros x. rewrite elem_of_union, elem_of_singleton, !elem_of_seq_set. omega.
   Qed.
 
   Lemma seq_set_S_union_L `{!LeibnizEquiv C} start len :
-    seq_set start (C:=C) (S len) = {[ start + len ]} ∪ seq_set start len.
+    seq_set start (S len) =@{C} {[ start + len ]} ∪ seq_set start len.
   Proof. unfold_leibniz. apply seq_set_S_union. Qed.
 End seq_set.
 
@@ -1078,7 +1077,7 @@ Section minimal.
   Context `{SimpleCollection A C} {R : relation A}.
   Implicit Types X Y : C.
 
-  Global Instance minimal_proper x : Proper (@equiv C _ ==> iff) (minimal R x).
+  Global Instance minimal_proper x : Proper ((≡@{C}) ==> iff) (minimal R x).
   Proof. intros X X' y; unfold minimal; set_solver. Qed.
 
   Lemma minimal_anti_symm_1 `{!AntiSymm (=) R} X x y :
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 21bea185..abbad8d9 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -147,38 +147,34 @@ Section setoid.
     m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
   Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
 
-  Global Instance map_equivalence :
-    Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (M A)).
+  Global Instance map_equivalence : Equivalence (≡@{A}) → Equivalence (≡@{M A}).
   Proof.
     split.
     - by intros m i.
     - by intros m1 m2 ? i.
     - by intros m1 m2 m3 ?? i; trans (m2 !! i).
   Qed.
-  Global Instance lookup_proper (i : K) :
-    Proper ((≡) ==> (≡)) (lookup (M:=M A) i).
+  Global Instance lookup_proper (i : K) : Proper ((≡@{M A}) ==> (≡)) (lookup i).
   Proof. by intros m1 m2 Hm. Qed.
   Global Instance partial_alter_proper :
-    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (partial_alter (M:=M A)).
+    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡@{M A})) partial_alter.
   Proof.
     by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
       rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne by done;
       try apply Hf; apply lookup_proper.
   Qed.
   Global Instance insert_proper (i : K) :
-    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=M A) i).
+    Proper ((≡) ==> (≡) ==> (≡@{M A})) (insert i).
   Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
-  Global Instance singleton_proper k :
-    Proper ((≡) ==> (≡)) (singletonM k : A → M A).
+  Global Instance singleton_proper k : Proper ((≡) ==> (≡@{M A})) (singletonM k).
   Proof.
     intros ???; apply insert_proper; [done|].
     intros ?. rewrite lookup_empty; constructor.
   Qed.
-  Global Instance delete_proper (i : K) :
-    Proper ((≡) ==> (≡)) (delete (M:=M A) i).
+  Global Instance delete_proper (i : K) : Proper ((≡) ==> (≡@{M A})) (delete i).
   Proof. by apply partial_alter_proper; [constructor|]. Qed.
   Global Instance alter_proper :
-    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (alter (A:=A) (M:=M A)).
+    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡@{M A})) alter.
   Proof.
     intros ?? Hf; apply partial_alter_proper.
     by destruct 1; constructor; apply Hf.
@@ -186,12 +182,12 @@ Section setoid.
   Lemma merge_ext `{Equiv B, Equiv C} (f g : option A → option B → option C)
       `{!DiagNone f, !DiagNone g} :
     ((≡) ==> (≡) ==> (≡))%signature f g →
-    ((≡) ==> (≡) ==> (≡))%signature (merge (M:=M) f) (merge g).
+    ((≡) ==> (≡) ==> (≡@{M _}))%signature (merge f) (merge g).
   Proof.
     by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge by done; apply Hf.
   Qed.
   Global Instance union_with_proper :
-    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡)) (union_with (M:=M A)).
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡@{M A})) union_with.
   Proof.
     intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
     by do 2 destruct 1; first [apply Hf | constructor].
@@ -205,7 +201,7 @@ Section setoid.
     - intros ?. rewrite lookup_empty; constructor.
   Qed.
   Global Instance map_fmap_proper `{Equiv B} (f : A → B) :
-    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap (M:=M) f).
+    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡@{M _})) (fmap f).
   Proof.
     intros ? m m' ? k; rewrite !lookup_fmap. by apply option_fmap_proper.
   Qed.
@@ -921,13 +917,13 @@ Section map_of_to_collection.
   Proof. unfold map_to_collection; simpl. by rewrite map_to_list_empty. Qed.
   Lemma map_to_collection_insert (f : K → A → B)(m : M A) i x :
     m !! i = None →
-    map_to_collection (C:=C) f (<[i:=x]>m) ≡ {[f i x]} ∪ map_to_collection f m.
+    map_to_collection f (<[i:=x]>m) ≡@{C} {[f i x]} ∪ map_to_collection f m.
   Proof.
     intros. unfold map_to_collection; simpl. by rewrite map_to_list_insert.
   Qed.
   Lemma map_to_collection_insert_L `{!LeibnizEquiv C} (f : K → A → B) (m : M A) i x :
     m !! i = None →
-    map_to_collection (C:=C) f (<[i:=x]>m) = {[f i x]} ∪ map_to_collection f m.
+    map_to_collection f (<[i:=x]>m) =@{C} {[f i x]} ∪ map_to_collection f m.
   Proof. unfold_leibniz. apply map_to_collection_insert. Qed.
 End map_of_to_collection.
 
@@ -1166,19 +1162,19 @@ Lemma merge_comm m1 m2 :
   (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) →
   merge f m1 m2 = merge f m2 m1.
 Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-Global Instance merge_comm' : Comm (=) f → Comm (=) (merge (M:=M) f).
+Global Instance merge_comm' : Comm (=) f → Comm (=@{M _}) (merge f).
 Proof. intros ???. apply merge_comm. intros. by apply (comm f). Qed.
 Lemma merge_assoc m1 m2 m3 :
   (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) =
         f (f (m1 !! i) (m2 !! i)) (m3 !! i)) →
   merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
 Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-Global Instance merge_assoc' : Assoc (=) f → Assoc (=) (merge (M:=M) f).
+Global Instance merge_assoc' : Assoc (=) f → Assoc (=@{M _}) (merge f).
 Proof. intros ????. apply merge_assoc. intros. by apply (assoc_L f). Qed.
 Lemma merge_idemp m1 :
   (∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) → merge f m1 m1 = m1.
 Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-Global Instance merge_idemp' : IdemP (=) f → IdemP (=) (merge (M:=M) f).
+Global Instance merge_idemp' : IdemP (=) f → IdemP (=@{M _}) (merge f).
 Proof. intros ??. apply merge_idemp. intros. by apply (idemp f). Qed.
 End merge.
 
@@ -1433,9 +1429,9 @@ Proof.
   rewrite lookup_union_with.
   destruct (m1 !! i), (m2 !! i); compute; naive_solver.
 Qed.
-Global Instance: LeftId (@eq (M A)) ∅ (union_with f).
+Global Instance: LeftId (=@{M A}) ∅ (union_with f).
 Proof. unfold union_with, map_union_with. apply _. Qed.
-Global Instance: RightId (@eq (M A)) ∅ (union_with f).
+Global Instance: RightId (=@{M A}) ∅ (union_with f).
 Proof. unfold union_with, map_union_with. apply _. Qed.
 Lemma union_with_comm m1 m2 :
   (∀ i x y, m1 !! i = Some x → m2 !! i = Some y → f x y = f y x) →
@@ -1444,7 +1440,7 @@ Proof.
   intros. apply (merge_comm _). intros i.
   destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
 Qed.
-Global Instance: Comm (=) f → Comm (@eq (M A)) (union_with f).
+Global Instance: Comm (=) f → Comm (=@{M A}) (union_with f).
 Proof. intros ???. apply union_with_comm. eauto. Qed.
 Lemma union_with_idemp m :
   (∀ i x, m !! i = Some x → f x x = Some x) → union_with f m m = m.
@@ -1502,15 +1498,15 @@ Qed.
 End union_with.
 
 (** ** Properties of the [union] operation *)
-Global Instance: LeftId (@eq (M A)) ∅ (∪) := _.
-Global Instance: RightId (@eq (M A)) ∅ (∪) := _.
-Global Instance: Assoc (@eq (M A)) (∪).
+Global Instance: LeftId (=@{M A}) ∅ (∪) := _.
+Global Instance: RightId (=@{M A}) ∅ (∪) := _.
+Global Instance: Assoc (=@{M A}) (∪).
 Proof.
   intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with.
   apply (merge_assoc _). intros i.
   by destruct (m1 !! i), (m2 !! i), (m3 !! i).
 Qed.
-Global Instance: IdemP (@eq (M A)) (∪).
+Global Instance: IdemP (=@{M A}) (∪).
 Proof. intros A ?. by apply union_with_idemp. Qed.
 Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x :
   (m1 ∪ m2) !! i = Some x ↔
@@ -1766,9 +1762,9 @@ Proof. intro. by rewrite map_disjoint_of_list_zip_r. Qed.
 Section intersection_with.
 Context {A} (f : A → A → option A).
 Implicit Type (m: M A).
-Global Instance : LeftAbsorb (@eq (M A)) ∅ (intersection_with f).
+Global Instance : LeftAbsorb (=@{M A}) ∅ (intersection_with f).
 Proof. unfold intersection_with, map_intersection_with. apply _. Qed.
-Global Instance: RightAbsorb (@eq (M A)) ∅ (intersection_with f).
+Global Instance: RightAbsorb (=@{M A}) ∅ (intersection_with f).
 Proof. unfold intersection_with, map_intersection_with. apply _. Qed.
 Lemma lookup_intersection_with m1 m2 i :
   intersection_with f m1 m2 !! i = intersection_with f (m1 !! i) (m2 !! i).
@@ -1787,7 +1783,7 @@ Proof.
   intros. apply (merge_comm _). intros i.
   destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
 Qed.
-Global Instance: Comm (=) f → Comm (@eq (M A)) (intersection_with f).
+Global Instance: Comm (=) f → Comm (=@{M A}) (intersection_with f).
 Proof. intros ???. apply intersection_with_comm. eauto. Qed.
 Lemma intersection_with_idemp m :
   (∀ i x, m !! i = Some x → f x x = Some x) → intersection_with f m m = m.
@@ -1817,16 +1813,16 @@ Proof. by intros; apply (partial_alter_merge _). Qed.
 End intersection_with.
 
 (** ** Properties of the [intersection] operation *)
-Global Instance: LeftAbsorb (@eq (M A)) ∅ (∩) := _.
-Global Instance: RightAbsorb (@eq (M A)) ∅ (∩) := _.
-Global Instance: Assoc (@eq (M A)) (∩).
+Global Instance: LeftAbsorb (=@{M A}) ∅ (∩) := _.
+Global Instance: RightAbsorb (=@{M A}) ∅ (∩) := _.
+Global Instance: Assoc (=@{M A}) (∩).
 Proof.
   intros A m1 m2 m3.
   unfold intersection, map_intersection, intersection_with, map_intersection_with.
   apply (merge_assoc _). intros i.
   by destruct (m1 !! i), (m2 !! i), (m3 !! i).
 Qed.
-Global Instance: IdemP (@eq (M A)) (∩).
+Global Instance: IdemP (=@{M A}) (∩).
 Proof. intros A ?. by apply intersection_with_idemp. Qed.
 
 Lemma lookup_intersection_Some {A} (m1 m2 : M A) i x :
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index a3ed60e8..4cc990e2 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -102,20 +102,20 @@ Global Instance gmultiset_elem_of_dec : RelDecision (@elem_of _ (gmultiset A) _)
 Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
 
 (* Algebraic laws *)
-Global Instance gmultiset_comm : Comm (@eq (gmultiset A)) (∪).
+Global Instance gmultiset_comm : Comm (=@{gmultiset A}) (∪).
 Proof.
   intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; omega.
 Qed.
-Global Instance gmultiset_assoc : Assoc (@eq (gmultiset A)) (∪).
+Global Instance gmultiset_assoc : Assoc (=@{gmultiset A}) (∪).
 Proof.
   intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; omega.
 Qed.
-Global Instance gmultiset_left_id : LeftId (@eq (gmultiset A)) ∅ (∪).
+Global Instance gmultiset_left_id : LeftId (=@{gmultiset A}) ∅ (∪).
 Proof.
   intros X. apply gmultiset_eq; intros x.
   by rewrite multiplicity_union, multiplicity_empty.
 Qed.
-Global Instance gmultiset_right_id : RightId (@eq (gmultiset A)) ∅ (∪).
+Global Instance gmultiset_right_id : RightId (=@{gmultiset A}) ∅ (∪).
 Proof. intros X. by rewrite (comm_L (∪)), (left_id_L _ _). Qed.
 
 Global Instance gmultiset_union_inj_1 X : Inj (=) (=) (X ∪).
@@ -126,7 +126,7 @@ Qed.
 Global Instance gmultiset_union_inj_2 X : Inj (=) (=) (∪ X).
 Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.
 
-Lemma gmultiset_non_empty_singleton x : {[ x ]} ≠ (∅ : gmultiset A).
+Lemma gmultiset_non_empty_singleton x : {[ x ]} ≠@{gmultiset A} ∅.
 Proof.
   rewrite gmultiset_eq. intros Hx; generalize (Hx x).
   by rewrite multiplicity_singleton, multiplicity_empty.
diff --git a/theories/list.v b/theories/list.v
index ace7fc83..e5ac38d9 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -358,7 +358,7 @@ Tactic Notation "discriminate_list" hyp(H) :=
   apply (f_equal length) in H;
   repeat (csimpl in H || rewrite app_length in H); exfalso; lia.
 Tactic Notation "discriminate_list" :=
-  match goal with H : @eq (list _) _ _ |- _ => discriminate_list H end.
+  match goal with H : _ =@{list _} _ |- _ => discriminate_list H end.
 
 (** The tactic [simplify_list_eq] simplifies hypotheses involving
 equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies
@@ -830,7 +830,7 @@ Section find.
 End find.
 
 (** ** Properties of the [reverse] function *)
-Lemma reverse_nil : reverse [] = @nil A.
+Lemma reverse_nil : reverse [] =@{list A} [].
 Proof. done. Qed.
 Lemma reverse_singleton x : reverse [x] = [x].
 Proof. done. Qed.
@@ -883,7 +883,7 @@ Lemma take_drop_middle l i x :
 Proof.
   revert i x. induction l; intros [|?] ??; simplify_eq/=; f_equal; auto.
 Qed.
-Lemma take_nil n : take n (@nil A) = [].
+Lemma take_nil n : take n [] =@{list A} [].
 Proof. by destruct n. Qed.
 Lemma take_app l k : take (length l) (l ++ k) = l.
 Proof. induction l; f_equal/=; auto. Qed.
@@ -935,7 +935,7 @@ Qed.
 (** ** Properties of the [drop] function *)
 Lemma drop_0 l : drop 0 l = l.
 Proof. done. Qed.
-Lemma drop_nil n : drop n (@nil A) = [].
+Lemma drop_nil n : drop n [] =@{list A} [].
 Proof. by destruct n. Qed.
 Lemma drop_length l n : length (drop n l) = length l - n.
 Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
@@ -1323,7 +1323,7 @@ Proof.
 Qed.
 
 (** ** Properties of the [mask] function *)
-Lemma mask_nil f βs : mask f βs (@nil A) = [].
+Lemma mask_nil f βs : mask f βs [] =@{list A} [].
 Proof. by destruct βs. Qed.
 Lemma mask_length f βs l : length (mask f βs l) = length l.
 Proof. revert βs. induction l; intros [|??]; f_equal/=; auto. Qed.
@@ -2826,7 +2826,7 @@ Section setoid.
   Qed.
 
   Global Instance list_equivalence :
-    Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (list A)).
+    Equivalence (≡@{A}) → Equivalence (≡@{list A}).
   Proof.
     split.
     - intros l. by apply equiv_Forall2.
@@ -2836,51 +2836,50 @@ Section setoid.
   Global Instance list_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (list A).
   Proof. induction 1; f_equal; fold_leibniz; auto. Qed.
 
-  Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A).
+  Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡@{list A})) cons.
   Proof. by constructor. Qed.
-  Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@app A).
+  Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡@{list A})) app.
   Proof. induction 1; intros ???; simpl; try constructor; auto. Qed.
-  Global Instance length_proper : Proper ((≡) ==> (=)) (@length A).
+  Global Instance length_proper : Proper ((≡@{list A}) ==> (=)) length.
   Proof. induction 1; f_equal/=; auto. Qed.
-  Global Instance tail_proper : Proper ((≡) ==> (≡)) (@tail A).
+  Global Instance tail_proper : Proper ((≡@{list A}) ==> (≡)) tail.
   Proof. destruct 1; try constructor; auto. Qed.
-  Global Instance take_proper n : Proper ((≡) ==> (≡)) (@take A n).
+  Global Instance take_proper n : Proper ((≡@{list A}) ==> (≡)) (take n).
   Proof. induction n; destruct 1; constructor; auto. Qed.
-  Global Instance drop_proper n : Proper ((≡) ==> (≡)) (@drop A n).
+  Global Instance drop_proper n : Proper ((≡@{list A}) ==> (≡)) (drop n).
   Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
-  Global Instance list_lookup_proper i :
-    Proper ((≡) ==> (≡)) (lookup (M:=list A) i).
+  Global Instance list_lookup_proper i : Proper ((≡@{list A}) ==> (≡)) (lookup i).
   Proof. induction i; destruct 1; simpl; try constructor; auto. Qed.
   Global Instance list_alter_proper f i :
-    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
+    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡@{list A})) (alter f i).
   Proof. intros. induction i; destruct 1; constructor; eauto. Qed.
   Global Instance list_insert_proper i :
-    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list A) i).
+    Proper ((≡) ==> (≡) ==> (≡@{list A})) (insert i).
   Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed.
   Global Instance list_inserts_proper i :
-    Proper ((≡) ==> (≡) ==> (≡)) (@list_inserts A i).
+    Proper ((≡) ==> (≡) ==> (≡@{list A})) (list_inserts i).
   Proof.
     intros k1 k2 Hk; revert i.
     induction Hk; intros ????; simpl; try f_equiv; naive_solver.
   Qed.
   Global Instance list_delete_proper i :
-    Proper ((≡) ==> (≡)) (delete (M:=list A) i).
+    Proper ((≡) ==> (≡@{list A})) (delete i).
   Proof. induction i; destruct 1; try constructor; eauto. Qed.
-  Global Instance option_list_proper : Proper ((≡) ==> (≡)) (@option_list A).
+  Global Instance option_list_proper : Proper ((≡) ==> (≡@{list A})) option_list.
   Proof. destruct 1; repeat constructor; auto. Qed.
   Global Instance list_filter_proper P `{∀ x, Decision (P x)} :
-    Proper ((≡) ==> iff) P → Proper ((≡) ==> (≡)) (filter (B:=list A) P).
+    Proper ((≡) ==> iff) P → Proper ((≡) ==> (≡@{list A})) (filter P).
   Proof. intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed.
-  Global Instance replicate_proper n : Proper ((≡) ==> (≡)) (@replicate A n).
+  Global Instance replicate_proper n : Proper ((≡@{A}) ==> (≡)) (replicate n).
   Proof. induction n; constructor; auto. Qed.
-  Global Instance reverse_proper : Proper ((≡) ==> (≡)) (@reverse A).
+  Global Instance reverse_proper : Proper ((≡) ==> (≡@{list A})) reverse.
   Proof.
     induction 1; rewrite ?reverse_cons; simpl; [constructor|].
     apply app_proper; repeat constructor; auto.
   Qed.
   Global Instance last_proper : Proper ((≡) ==> (≡)) (@last A).
   Proof. induction 1 as [|????? []]; simpl; repeat constructor; auto. Qed.
-  Global Instance resize_proper n : Proper ((≡) ==> (≡) ==> (≡)) (@resize A n).
+  Global Instance resize_proper n : Proper ((≡) ==> (≡) ==> (≡@{list A})) (resize n).
   Proof.
     induction n; destruct 2; simpl; repeat (constructor || f_equiv); auto.
   Qed.
@@ -3646,7 +3645,7 @@ Ltac solve_length :=
   simplify_eq/=;
   repeat (rewrite fmap_length || rewrite app_length);
   repeat match goal with
-  | H : @eq (list _) _ _ |- _ => apply (f_equal length) in H
+  | H : _ =@{list _} _ |- _ => apply (f_equal length) in H
   | H : Forall2 _ _ _ |- _ => apply Forall2_length in H
   | H : context[length (_ <$> _)] |- _ => rewrite fmap_length in H
   end; done || congruence.
diff --git a/theories/mapset.v b/theories/mapset.v
index 6e9f72cb..b814d68f 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -76,7 +76,7 @@ Section deciders.
     match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
     abstract congruence.
   Defined.
-  Global Instance mapset_equiv_dec : RelDecision (@equiv (mapset M)_) | 1.
+  Global Instance mapset_equiv_dec : RelDecision (≡@{mapset M}) | 1.
   Proof. refine (λ X1 X2, cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined.
   Global Instance mapset_elem_of_dec : RelDecision (@elem_of _ (mapset M) _) | 1.
   Proof. refine (λ x X, cast_if (decide (mapset_car X !! x = Some ()))); done. Defined.
diff --git a/theories/option.v b/theories/option.v
index f539f4bf..fa3fbd61 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -122,11 +122,11 @@ Section setoids.
   Proof. done. Qed.
 
   Global Instance option_equivalence :
-    Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (option A)).
+    Equivalence (≡@{A}) → Equivalence (≡@{option A}).
   Proof. apply _. Qed.
-  Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A).
+  Global Instance Some_proper : Proper ((≡) ==> (≡@{option A})) Some.
   Proof. by constructor. Qed.
-  Global Instance Some_equiv_inj : Inj (≡) (≡) (@Some A).
+  Global Instance Some_equiv_inj : Inj (≡) (≡@{option A}) Some.
   Proof. by inversion_clear 1. Qed.
   Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
   Proof. intros x y; destruct 1; f_equal; by apply leibniz_equiv. Qed.
@@ -141,11 +141,11 @@ Section setoids.
   Proof. destruct 1; naive_solver. Qed.
   Lemma equiv_Some_inv_l' my x : Some x ≡ my → ∃ x', Some x' = my ∧ x ≡ x'.
   Proof. intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed.
-  Lemma equiv_Some_inv_r' `{!Equivalence ((≡) : relation A)} mx y :
+  Lemma equiv_Some_inv_r' `{!Equivalence (≡@{A})} mx y :
     mx ≡ Some y → ∃ y', mx = Some y' ∧ y ≡ y'.
   Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed.
 
-  Global Instance is_Some_proper : Proper ((≡) ==> iff) (@is_Some A).
+  Global Instance is_Some_proper : Proper ((≡@{option A}) ==> iff) is_Some.
   Proof. inversion_clear 1; split; eauto. Qed.
   Global Instance from_option_proper {B} (R : relation B) (f : A → B) :
     Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
@@ -188,8 +188,7 @@ Lemma fmap_Some_1 {A B} (f : A → B) mx y :
 Proof. apply fmap_Some. Qed.
 Lemma fmap_Some_2 {A B} (f : A → B) mx x : mx = Some x → f <$> mx = Some (f x).
 Proof. intros. apply fmap_Some; eauto. Qed.
-Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)}
-      (f : A → B) mx y :
+Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence (≡@{B})} (f : A → B) mx y :
   f <$> mx ≡ Some y ↔ ∃ x, mx = Some x ∧ y ≡ f x.
 Proof.
   destruct mx; simpl; split.
@@ -198,8 +197,7 @@ Proof.
   - intros ?%symmetry%equiv_None. done.
   - intros (? & ? & ?). done.
 Qed.
-Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)}
-      (f : A → B) mx y :
+Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence (≡@{B})} (f : A → B) mx y :
   f <$> mx ≡ Some y → ∃ x, mx = Some x ∧ y ≡ f x.
 Proof. by rewrite fmap_Some_equiv. Qed.
 Lemma fmap_None {A B} (f : A → B) mx : f <$> mx = None ↔ mx = None.
@@ -237,13 +235,13 @@ Lemma bind_with_Some {A} (mx : option A) : mx ≫= Some = mx.
 Proof. by destruct mx. Qed.
 
 Instance option_fmap_proper `{Equiv A, Equiv B} :
-  Proper (((≡) ==> (≡)) ==> (≡) ==> (≡)) (fmap (M:=option) (A:=A) (B:=B)).
+  Proper (((≡) ==> (≡)) ==> (≡@{option A}) ==> (≡@{option B})) fmap.
 Proof. destruct 2; constructor; auto. Qed.
 Instance option_mbind_proper `{Equiv A, Equiv B} :
-  Proper (((≡) ==> (≡)) ==> (≡) ==> (≡)) (mbind (M:=option) (A:=A) (B:=B)).
+  Proper (((≡) ==> (≡)) ==> (≡@{option A}) ==> (≡@{option B})) mbind.
 Proof. destruct 2; simpl; try constructor; auto. Qed.
 Instance option_mjoin_proper `{Equiv A} :
-  Proper ((≡) ==> (≡)) (mjoin (M:=option) (A:=A)).
+  Proper ((≡) ==> (≡@{option (option A)})) mjoin.
 Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
 
 (** ** Inverses of constructors *)
@@ -312,14 +310,14 @@ Section union_intersection_difference.
   Global Instance union_with_right_id : RightId (=) None (union_with f).
   Proof. by intros [?|]. Qed.
   Global Instance union_with_comm :
-    Comm (=) f → Comm (=) (union_with (M:=option A) f).
+    Comm (=) f → Comm (=@{option A}) (union_with f).
   Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
   Global Instance intersection_with_left_ab : LeftAbsorb (=) None (intersection_with f).
   Proof. by intros [?|]. Qed.
   Global Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f).
   Proof. by intros [?|]. Qed.
   Global Instance difference_with_comm :
-    Comm (=) f → Comm (=) (intersection_with (M:=option A) f).
+    Comm (=) f → Comm (=@{option A}) (intersection_with f).
   Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
   Global Instance difference_with_right_id : RightId (=) None (difference_with f).
   Proof. by intros [?|]. Qed.
diff --git a/theories/pmap.v b/theories/pmap.v
index 05c9b94c..0eba03ef 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -13,8 +13,8 @@ From stdpp Require Export fin_maps.
 Set Default Proof Using "Type".
 
 Local Open Scope positive_scope.
-Local Hint Extern 0 (@eq positive _ _) => congruence.
-Local Hint Extern 0 (¬@eq positive _ _) => congruence.
+Local Hint Extern 0 (_ =@{positive} _) => congruence.
+Local Hint Extern 0 (_ ≠@{positive} _) => congruence.
 
 (** * The tree data structure *)
 (** The data type [Pmap_raw] specifies radix-2 search trees. These trees do
diff --git a/theories/pretty.v b/theories/pretty.v
index a1e85a46..a26e574b 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -40,7 +40,7 @@ Qed.
 Instance pretty_N : Pretty N := λ x, pretty_N_go x ""%string.
 Lemma pretty_N_unfold x : pretty x = pretty_N_go x "".
 Proof. done. Qed.
-Instance pretty_N_inj : Inj (@eq N) (=) pretty.
+Instance pretty_N_inj : Inj (=@{N}) (=) pretty.
 Proof.
   assert (∀ x y, x < 10 → y < 10 →
     pretty_N_char x =  pretty_N_char y → x = y)%N.
@@ -71,6 +71,6 @@ Instance pretty_Z : Pretty Z := λ x,
   | Z0 => "" | Zpos x => pretty (Npos x) | Zneg x => "-" +:+ pretty (Npos x)
   end%string.
 Instance pretty_nat : Pretty nat := λ x, pretty (N.of_nat x).
-Instance pretty_nat_inj : Inj (@eq nat) (=) pretty.
+Instance pretty_nat_inj : Inj (=@{nat}) (=) pretty.
 Proof. apply _. Qed.
 
diff --git a/theories/streams.v b/theories/streams.v
index 747141eb..0a1be8b6 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -38,7 +38,7 @@ Implicit Types s t : stream A.
 
 Lemma scons_equiv s1 s2 : shead s1 = shead s2 → stail s1 ≡ stail s2 → s1 ≡ s2.
 Proof. by constructor. Qed.
-Global Instance equal_equivalence : Equivalence (@equiv (stream A) _).
+Global Instance equal_equivalence : Equivalence (≡@{stream A}).
 Proof.
   split.
   - now cofix; intros [??]; constructor.
@@ -47,10 +47,10 @@ Proof.
 Qed.
 Global Instance scons_proper x : Proper ((≡) ==> (≡)) (scons x).
 Proof. by constructor. Qed.
-Global Instance shead_proper : Proper ((≡) ==> (=)) (@shead A).
+Global Instance shead_proper : Proper ((≡) ==> (=@{A})) shead.
 Proof. by intros ?? [??]. Qed.
-Global Instance stail_proper : Proper ((≡) ==> (≡)) (@stail A).
+Global Instance stail_proper : Proper ((≡) ==> (≡@{stream A})) stail.
 Proof. by intros ?? [??]. Qed.
-Global Instance slookup_proper : Proper ((≡) ==> eq) (@slookup A i).
+Global Instance slookup_proper : Proper ((≡@{stream A}) ==> (=)) (slookup i).
 Proof. by induction i as [|i IH]; intros s1 s2 Hs; simpl; rewrite Hs. Qed.
 End stream_properties.
diff --git a/theories/tactics.v b/theories/tactics.v
index 84922876..4b42a8f6 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -241,7 +241,7 @@ Tactic Notation "simplify_eq" := repeat
     assert (y = x) by congruence; clear H2
   | H1 : ?o = Some ?x, H2 : ?o = None |- _ => congruence
   | H : @existT ?A _ _ _ = existT _ _ |- _ =>
-     apply (Eqdep_dec.inj_pair2_eq_dec _ (decide_rel (@eq A))) in H
+     apply (Eqdep_dec.inj_pair2_eq_dec _ (decide_rel (=@{A}))) in H
   end.
 Tactic Notation "simplify_eq" "/=" :=
   repeat (progress csimpl in * || simplify_eq).
-- 
GitLab