diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 594b396d6..0a2d02aad 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -492,24 +492,24 @@ Qed.
 
 Lemma measurable_itv (i : interval R) : measurable [set` i].
 Proof.
-have moc (a b : R) : measurable `]a, b]%classic.
+have moc (a b : R) : measurable `]a, b].
   by apply: sub_sigma_algebra; apply: is_ocitv.
-have mopoo (x : R) : measurable `]x, +oo[%classic.
+have mopoo (x : R) : measurable `]x, +oo[.
   by rewrite itv_bnd_infty_bigcup; exact: bigcup_measurable.
-have mnooc (x : R) : measurable `]-oo, x]%classic.
+have mnooc (x : R) : measurable `]-oo, x].
   by rewrite -setCitvr; exact/measurableC.
-have ooE (a b : R) : `]a, b[%classic = `]a, b]%classic `\ b.
+have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b.
   case: (boolP (a < b)) => ab; last by rewrite !set_itv_ge ?set0D.
   by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF.
-have moo (a b : R) : measurable `]a, b[%classic.
+have moo (a b : R) : measurable `]a, b[.
   by rewrite ooE; exact: measurableD.
-have mcc (a b : R) : measurable `[a, b]%classic.
+have mcc (a b : R) : measurable `[a, b].
   case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge.
   by rewrite -setU1itv//; apply/measurableU.
-have mco (a b : R) : measurable `[a, b[%classic.
+have mco (a b : R) : measurable `[a, b[.
   case: (boolP (a < b)) => ab; last by rewrite set_itv_ge.
   by rewrite -setU1itv//; apply/measurableU.
-have oooE (b : R) : `]-oo, b[%classic = `]-oo, b]%classic `\ b.
+have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b.
   by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx.
 case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge.
 - by rewrite -setU1itv//; exact/measurableU.
diff --git a/theories/measure.v b/theories/measure.v
index 1dfdeecfa..3f60e5d0d 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -721,6 +721,8 @@ HB.mixin Record isSemiRingOfSets (d : measure_display) T := {
 #[short(type=semiRingOfSetsType)]
 HB.structure Definition SemiRingOfSets d := {T of isSemiRingOfSets d T}.
 
+Arguments measurable {d}%measure_display_scope {s} _%classical_set_scope.
+
 Canonical semiRingOfSets_eqType d (T : semiRingOfSetsType d) := EqType T ptclass.
 Canonical semiRingOfSets_choiceType d (T : semiRingOfSetsType d) :=
   ChoiceType T ptclass.