diff --git a/src/library/user_recursors.h b/src/library/user_recursors.h
index 81a3834fd6..6f5fc49f7f 100644
--- a/src/library/user_recursors.h
+++ b/src/library/user_recursors.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-
+#include "kernel/environment.h"
 namespace lean {
 /** \brief Information for a user defined recursor */
 class recursor_info {