diff --git a/theories/exp.v b/theories/exp.v
index c7316c04f..b21b553f9 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import mathcomp_extra.
-Require Import reals ereal nsatz_realtype.
+Require Import reals ereal.
 Require Import signed topology normedtype landau sequences derive realfun.
 Require Import itv convex.