diff --git a/information_theory/entropy_convex.v b/information_theory/entropy_convex.v
index 35197dab..0c8370ee 100644
--- a/information_theory/entropy_convex.v
+++ b/information_theory/entropy_convex.v
@@ -7,7 +7,7 @@ From mathcomp Require boolp.
 From mathcomp Require Import unstable mathcomp_extra reals.
 From mathcomp Require Import interval_inference set_interval.
 From mathcomp Require Import functions topology normedtype realfun derive exp.
-From mathcomp Require convex.
+From mathcomp Require Import -(notations)convex.
 Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln.
 Require Import derive_ext fdist jfdist_cond entropy convex.
 Require Import binary_entropy_function log_sum divergence.
@@ -244,7 +244,7 @@ have cnH2: {within `[x, y], continuous (- H2)}%classic.
 apply/RNconcave_function_at.
 rewrite /convex_function_at /=.
 rewrite -!mc_convRE.
-apply: (@analysis.convex.second_derivative_convex _ (fun z => - (H2 z))).
+apply: (@second_derivative_convex _ (fun z => - (H2 z))).
 - move=> z xzy.
   have/zxyoo01 z01: z \in `]x, y[%classic by rewrite inE.
   by rewrite DDnH2E// DDnH2_nonneg.
diff --git a/probability/convex.v b/probability/convex.v
index a1345b68..ea343fe8 100644
--- a/probability/convex.v
+++ b/probability/convex.v
@@ -4,6 +4,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg fingroup perm matrix interval.
 From mathcomp Require Import unstable mathcomp_extra boolp classical_sets.
 From mathcomp Require Import ssrnum archimedean ereal interval_inference.
+From mathcomp Require Import realfun.
 From mathcomp Require Import ring lra reals.
 Require Import ssr_ext ssralg_ext realType_ext realType_ln fdist.
 From mathcomp Require vector.