From 210bf0910c6e2128193fb0fa7f3db7d9d867a18b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 5 Apr 2018 11:21:30 +0200
Subject: [PATCH] =?UTF-8?q?Notation=20`=E2=88=88@{A}`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base.v            | 3 +++
 theories/bset.v            | 2 +-
 theories/coPset.v          | 2 +-
 theories/collections.v     | 5 ++---
 theories/fin_collections.v | 2 +-
 theories/gmultiset.v       | 2 +-
 theories/infinite.v        | 2 +-
 theories/list.v            | 2 +-
 theories/mapset.v          | 2 +-
 9 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index d4005a4d..801af5bf 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -856,6 +856,9 @@ 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.
+
 Class Disjoint A := disjoint : A → A → Prop.
  Hint Mode Disjoint ! : typeclass_instances.
 Instance: Params (@disjoint) 2.
diff --git a/theories/bset.v b/theories/bset.v
index 1c17ee66..f0b7a050 100644
--- a/theories/bset.v
+++ b/theories/bset.v
@@ -29,7 +29,7 @@ Proof.
   - intros X Y x; unfold elem_of, bset_elem_of; simpl. 
     destruct (bset_car X x), (bset_car Y x); simpl; tauto.
 Qed.
-Instance bset_elem_of_dec {A} : RelDecision (@elem_of _ (bset A) _).
+Instance bset_elem_of_dec {A} : RelDecision (∈@{bset A}).
 Proof. refine (λ x X, cast_if (decide (bset_car X x))); done. Defined.
 
 Typeclasses Opaque bset_elem_of.
diff --git a/theories/coPset.v b/theories/coPset.v
index 5c027492..77b0d2b2 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -190,7 +190,7 @@ Proof.
   intros p; apply eq_bool_prop_intro, (HXY p).
 Qed.
 
-Instance coPset_elem_of_dec : RelDecision (@elem_of _ coPset _).
+Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
 Proof. solve_decision. Defined.
 Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
 Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
diff --git a/theories/collections.v b/theories/collections.v
index 93f3d435..cc4b9cc7 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -28,8 +28,7 @@ Section setoids_simple.
   Qed.
   Global Instance singleton_proper : Proper ((=) ==> (≡@{C})) singleton.
   Proof. apply _. Qed.
-  Global Instance elem_of_proper :
-    Proper ((=) ==> (≡) ==> iff) (@elem_of A C _) | 5.
+  Global Instance elem_of_proper : Proper ((=) ==> (≡) ==> iff) (∈@{C}) | 5.
   Proof. by intros x ? <- X Y. Qed.
   Global Instance disjoint_proper: Proper ((≡) ==> (≡) ==> iff) (@disjoint C _).
   Proof.
@@ -695,7 +694,7 @@ Section collection.
   End leibniz.
 
   Section dec.
-    Context `{!RelDecision (@elem_of A C _)}.
+    Context `{!RelDecision (∈@{C})}.
     Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
     Proof. rewrite elem_of_intersection. destruct (decide (x ∈ X)); tauto. Qed.
     Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y.
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index c2e6487e..0d9f16e8 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -23,7 +23,7 @@ Implicit Types X Y : C.
 Lemma fin_collection_finite X : set_finite X.
 Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
 
-Instance elem_of_dec_slow : RelDecision (@elem_of A C _) | 100.
+Instance elem_of_dec_slow : RelDecision (∈@{C}) | 100.
 Proof.
   refine (λ x X, cast_if (decide_rel (∈) x (elements X)));
     by rewrite <-(elem_of_elements _).
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 4cc990e2..ab6583c1 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -98,7 +98,7 @@ Proof.
       by split; auto with lia.
   - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. omega.
 Qed.
-Global Instance gmultiset_elem_of_dec : RelDecision (@elem_of _ (gmultiset A) _).
+Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
 Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
 
 (* Algebraic laws *)
diff --git a/theories/infinite.v b/theories/infinite.v
index 7b5c08f8..81863ebc 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -26,7 +26,7 @@ Qed.
 
 (** * Fresh elements *)
 Section Fresh.
-  Context `{FinCollection A C, Infinite A, !RelDecision (@elem_of A C _)}.
+  Context `{FinCollection A C, Infinite A, !RelDecision (∈@{C})}.
 
   Definition fresh_generic_body (s : C) (rec : ∀ s', s' ⊂ s → nat → A) (n : nat) : A :=
     let cand := inject n in
diff --git a/theories/list.v b/theories/list.v
index e5ac38d9..d5df07c7 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -311,7 +311,7 @@ Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈ l1 →
 
 Section list_set.
   Context `{dec : EqDecision A}.
-  Global Instance elem_of_list_dec : RelDecision (@elem_of A (list A) _).
+  Global Instance elem_of_list_dec : RelDecision (∈@{list A}).
   Proof.
    refine (
     fix go x l :=
diff --git a/theories/mapset.v b/theories/mapset.v
index b814d68f..fa5e02e5 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -78,7 +78,7 @@ Section deciders.
   Defined.
   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.
+  Global Instance mapset_elem_of_dec : RelDecision (∈@{mapset M}) | 1.
   Proof. refine (λ x X, cast_if (decide (mapset_car X !! x = Some ()))); done. Defined.
   Global Instance mapset_disjoint_dec : RelDecision (@disjoint (mapset M) _).
   Proof.
-- 
GitLab