From d9b128a783a81be63aae46867f84545a6aca66fc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Nov 2019 09:07:23 +0100
Subject: [PATCH] Remove `:>>` subclass instance declarations

There are not documented in
https://coq.inria.fr/refman/addendum/type-classes.html?highlight=class#coq:cmd.class,
and they don't have any advantage, so it's better to stop using them.
---
 theories/base.v        | 4 ++--
 theories/fin_map_dom.v | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 3900bc61..aca6e5de 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1161,7 +1161,7 @@ Class SemiSet A C `{ElemOf A C,
 }.
 Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
     Union C, Intersection C, Difference C} : Prop := {
-  set_semi_set :>> SemiSet A C;
+  set_semi_set :> SemiSet A C;
   elem_of_intersection (X Y : C) (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
   elem_of_difference (X Y : C) (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
 }.
@@ -1201,7 +1201,7 @@ Qed.
 anyway so as to avoid cycles in type class search. *)
 Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
     Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
-  fin_set_set :>> Set_ A C;
+  fin_set_set :> Set_ A C;
   elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X;
   NoDup_elements (X : C) : NoDup (elements X)
 }.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 6fc4c394..1d939a5d 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -11,8 +11,8 @@ Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
     OMap M, Merge M, ∀ A, FinMapToList K A (M A), EqDecision K,
     ElemOf K D, Empty D, Singleton K D,
     Union D, Intersection D, Difference D} := {
-  finmap_dom_map :>> FinMap K M;
-  finmap_dom_set :>> Set_ K D;
+  finmap_dom_map :> FinMap K M;
+  finmap_dom_set :> Set_ K D;
   elem_of_dom {A} (m : M A) i : i ∈ dom D m ↔ is_Some (m !! i)
 }.
 
-- 
GitLab