diff --git a/theories/charge.v b/theories/charge.v
index e1f9965f94..9fae017ba9 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -91,7 +91,6 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-Import numFieldTopology.Exports.
 Import numFieldNormedType.Exports.
 
 Local Open Scope ring_scope.
diff --git a/theories/ftc.v b/theories/ftc.v
index 2d944d434e..9b3d9fc48a 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -24,7 +24,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-Import numFieldTopology.Exports.
 Import numFieldNormedType.Exports.
 
 Local Open Scope classical_set_scope.
@@ -39,7 +38,7 @@ Implicit Types (f : R -> R) (a : itv_bound R).
 Let FTC0 f a : mu.-integrable setT (EFin \o f) ->
   let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in
   forall x, a < BRight x -> lebesgue_pt f x ->
-    h^-1 *: (F (h + x) - F x) @[h --> (0:R)%R^'] --> f x.
+    h^-1 *: (F (h + x) - F x) @[h --> 0%R^'] --> f x.
 Proof.
 move=> intf F x ax fx.
 have locf : locally_integrable setT f.
@@ -191,7 +190,7 @@ Let FTC0_restrict f a x (u : R) : (x < u)%R ->
   mu.-integrable [set` Interval a (BRight u)] (EFin \o f) ->
   let F y := (\int[mu]_(t in [set` Interval a (BRight y)]) f t)%R in
   a < BRight x -> lebesgue_pt f x ->
-  h^-1 *: (F (h + x) - F x) @[h --> ((0:R)%R^')] --> f x.
+  h^-1 *: (F (h + x) - F x) @[h --> (0%R^')] --> f x.
 Proof.
 move=> xu + F ax fx.
 rewrite integrable_mkcond//= (restrict_EFin f) => intf.
@@ -354,7 +353,7 @@ Unshelve. all: by end_near. Qed.
 
 Lemma parameterized_integral_cvg_left a b (f : R -> R) : a < b ->
   mu.-integrable `[a, b] (EFin \o f) ->
-  int a x f @[x --> a] --> (0:R).
+  int a x f @[x --> a] --> 0.
 Proof.
 move=> ab intf; pose fab := f \_ `[a, b].
 have intfab : mu.-integrable `[a, b] (EFin \o fab).
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 28b581bd6a..e743cd0a71 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -82,7 +82,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-Import numFieldTopology.Exports.
 Import numFieldNormedType.Exports.
 From mathcomp Require Import mathcomp_extra.
 
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index bdd6263f30..193331cbad 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -61,7 +61,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
-Import numFieldTopology.Exports.
 Import numFieldNormedType.Exports.
 
 Local Open Scope classical_set_scope.