diff --git a/theories/base.v b/theories/base.v
index 3900bc61734e1cf3c6cb20c5df4edf90e85f1a1d..aca6e5de38701cd1cf86369486ac93be3c8232dd 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 6fc4c39434f74ce3664e3601919e1f6dfb4a9599..1d939a5d3672a3713d39a66980a4f961c3eaefd3 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)
 }.