diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
index a2155ef0e..f9992483c 100644
--- a/reals/constructive_ereal.v
+++ b/reals/constructive_ereal.v
@@ -137,7 +137,7 @@ Definition er_map T T' (f : T -> T') (x : \bar T) : \bar T' :=
 Lemma er_map_idfun T (x : \bar T) : er_map idfun x = x.
 Proof. by case: x. Qed.
 
-Definition fine {R : zmodType} x : R := if x is EFin v then v else 0.
+Definition fine {R : zmodType} x : R := if x is EFin v then v else 0%R.
 
 Section EqEReal.
 Variable (R : eqType).
diff --git a/theories/normedtype.v b/theories/normedtype.v
index bf18d7bcd..ad227e6e1 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -244,11 +244,11 @@ Proof.
 apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]].
   exists (-%R @` A).
     exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//.
-    by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC.
+    by apply: reA; rewrite ?(@eqr_opp R)//= opprK addrC distrC.
   rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=.
   by rewrite opprK.
 exists e => //= x/=; rewrite -opprD normrN => axe xa.
-exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=.
+exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?(@eqr_oppLR R)//=.
 by rewrite opprK.
 Qed.
 
diff --git a/theories/showcase/summability.v b/theories/showcase/summability.v
index dae60a5b9..0a6c1df55 100644
--- a/theories/showcase/summability.v
+++ b/theories/showcase/summability.v
@@ -35,8 +35,9 @@ apply: filter_fromT_filter; first by exists fset0.
 by move=> A B /=; exists (A `|` B) => P /=; rewrite fsubUset => /andP[].
 Qed.
 
+Print Visibility.
 Definition partial_sum {I : choiceType} {R : zmodType}
-  (x : I -> R) (A : {fset I}) : R := \sum_(i : A) x (val i).
+  (x : I -> R) (A : {fset I}) : R := (\sum_(i : A) x (val i))%R.
 
 Definition sum (I : choiceType) {K : numDomainType} {R : normedModType K}
    (x : I -> R) : R := lim (partial_sum x @ totally).