diff --git a/theories/base.v b/theories/base.v
index 4f9c20a6d8947a8d0a62a6b76841c77675b7c7dc..86d98c17b6e8d2ac44d9ab595aeebbb89637c321 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -505,12 +505,7 @@ Arguments id _ _ / : assert.
 Arguments compose _ _ _ _ _ _ / : assert.
 Arguments flip _ _ _ _ _ _ / : assert.
 Arguments const _ _ _ _ / : assert.
-Typeclasses Transparent id compose const.
-
-(** Make sure that [flip] is type class opaque, otherwise one gets loops due to
-instance involving [flip], e.g. [RelDecision R → RelDecision (flip R)] could be
-used indefinitely. *)
-Typeclasses Opaque flip.
+Typeclasses Transparent id compose flip const.
 
 Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' :=
   g ∘ h ∘ f.
diff --git a/theories/decidable.v b/theories/decidable.v
index 062dd1dc3ba0267eb21288ec996e23ec9fbb6a39..c78d72a6f01edf12d7d3fb1f47eeb2ea9fa7acdf 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -135,7 +135,7 @@ Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
   dexist (`x) p = x.
 Proof. apply dsig_eq; reflexivity. Qed.
 
-(** * Instances of [Decision] *)
+(** * Instances of Decision *)
 (** Instances of [Decision] for operators of propositional logic. *)
 Instance True_dec: Decision True := left I.
 Instance False_dec: Decision False := right (False_rect False).
@@ -192,7 +192,3 @@ Proof. destruct (decide Q); tauto. Qed.
 Program Definition inj_eq_dec `{EqDecision A} {B} (f : B → A)
   `{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
 Solve Obligations with firstorder congruence.
-
-(** * Instances of [RelDecision] *)
-Instance flip_dec {A} (R : relation A) `{!RelDecision R} :
-  RelDecision (flip R) := λ x y, decide_rel R y x.