diff --git a/src/interval/interval.cpp b/src/interval/interval.cpp
index fdaf31a59b..985d22e4f8 100644
--- a/src/interval/interval.cpp
+++ b/src/interval/interval.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "interval_def.h"
 #include "mpq.h"
+#include "double.h"
 
 namespace lean {
 template class interval<mpq>;