diff --git a/theories/base.v b/theories/base.v
index 86d98c17b6e8d2ac44d9ab595aeebbb89637c321..4f9c20a6d8947a8d0a62a6b76841c77675b7c7dc 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -505,7 +505,12 @@ Arguments id _ _ / : assert.
 Arguments compose _ _ _ _ _ _ / : assert.
 Arguments flip _ _ _ _ _ _ / : assert.
 Arguments const _ _ _ _ / : assert.
-Typeclasses Transparent id compose flip const.
+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.
 
 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 c78d72a6f01edf12d7d3fb1f47eeb2ea9fa7acdf..062dd1dc3ba0267eb21288ec996e23ec9fbb6a39 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,3 +192,7 @@ 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.