From 88844f62611f5f47f9cf9f6da3cf166874144ffc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 28 Jun 2015 12:53:48 -0700 Subject: [PATCH] chore(src/library/user_recursors): add missing include --- src/library/user_recursors.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 {