Merge branch 'ci/robbert/no_forward_instances' into 'master'

Remove `:>>` subclass instance declarations

See merge request !104

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)
 }.

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)
 }.