diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 4f4a146307fd4e54dec03748b8d6b2cc81e7a887..07603e81791ab8c06b05f4d480f997c1fe65bc5b 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -2255,7 +2255,7 @@ Qed.
 (** ** Properties on the [map_relation] relation *)
 Section map_relation.
   Context {A B} (R : K → A → B → Prop) (P : K → A → Prop) (Q : K → B → Prop).
-  Context `{!∀ i x y, Decision (R i x y),
+  Context `{!∀ i, RelDecision (R i),
     !∀ i x, Decision (P i x), !∀ i y, Decision (Q i y)}.
 
   (** The function [f] and lemma [map_relation_alt] are helpers to prove the
diff --git a/stdpp/fin_sets.v b/stdpp/fin_sets.v
index cc1725e3507ef05e30c071801e5b2acdf3845ff4..ee03dde9e5a49a4596286d0a84e05f99f2314384 100644
--- a/stdpp/fin_sets.v
+++ b/stdpp/fin_sets.v
@@ -345,7 +345,7 @@ Lemma set_fold_comm_acc {B} (f : A → B → B) (g : B → B) (b : B) X :
 Proof. intros. apply (set_fold_comm_acc_strong _); [solve_proper|auto]. Qed.
 
 (** * Minimal elements *)
-Lemma minimal_exists_elem_of R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) :
+Lemma minimal_exists_elem_of R `{!Transitive R, !RelDecision R} (X : C) :
   X ≢ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
 Proof.
   pattern X; apply set_ind; clear X.
@@ -361,13 +361,12 @@ Proof.
   exists x; split; [set_solver|].
   rewrite HX, (right_id _ (∪)). apply singleton_minimal.
 Qed.
-Lemma minimal_exists_elem_of_L R `{!LeibnizEquiv C, !Transitive R,
-    ∀ x y, Decision (R x y)} (X : C) :
+Lemma minimal_exists_elem_of_L R
+    `{!LeibnizEquiv C, !Transitive R, !RelDecision R} (X : C) :
   X ≠ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
 Proof. unfold_leibniz. apply (minimal_exists_elem_of R). Qed.
 
-Lemma minimal_exists R `{!Transitive R,
-    ∀ x y, Decision (R x y)} `{!Inhabited A} (X : C) :
+Lemma minimal_exists R `{!Transitive R, !RelDecision R, !Inhabited A} (X : C) :
   ∃ x, minimal R x X.
 Proof.
   destruct (set_choose_or_empty X) as [ (y & Ha) | Hne].
diff --git a/stdpp/sorting.v b/stdpp/sorting.v
index c5d4d95f04b4139094ae2dd6ebf20ca64bf90d42..be2059c2bcf39836bd4a76bf71d51baf4ab89d36 100644
--- a/stdpp/sorting.v
+++ b/stdpp/sorting.v
@@ -5,7 +5,7 @@ From stdpp Require Export orders list.
 From stdpp Require Import options.
 
 Section merge_sort.
-  Context {A} (R : relation A) `{∀ x y, Decision (R x y)}.
+  Context {A} (R : relation A) `{!RelDecision R}.
 
   Fixpoint list_merge (l1 : list A) : list A → list A :=
     fix list_merge_aux l2 :=
@@ -111,7 +111,7 @@ Section sorted.
     | y :: l => cast_if (decide (R x y))
     end; abstract first [by constructor | by inv 1].
   Defined.
-  Global Instance Sorted_dec `{∀ x y, Decision (R x y)} : ∀ l,
+  Global Instance Sorted_dec `{!RelDecision R} : ∀ l,
     Decision (Sorted R l).
   Proof.
    refine
@@ -121,7 +121,7 @@ Section sorted.
     | x :: l => cast_if_and (decide (HdRel R x l)) (go l)
     end); clear go; abstract first [by constructor | by inv 1].
   Defined.
-  Global Instance StronglySorted_dec `{∀ x y, Decision (R x y)} : ∀ l,
+  Global Instance StronglySorted_dec `{!RelDecision R} : ∀ l,
     Decision (StronglySorted R l).
   Proof.
    refine
@@ -172,7 +172,7 @@ Qed.
 
 (** ** Correctness of merge sort *)
 Section merge_sort_correct.
-  Context  {A} (R : relation A) `{∀ x y, Decision (R x y)}.
+  Context  {A} (R : relation A) `{!RelDecision R}.
 
   Lemma list_merge_nil_l l2 : list_merge R [] l2 = l2.
   Proof. by destruct l2. Qed.