chore(src/library/user_recursors): add missing include
This commit is contained in:
parent
2f75768243
commit
88844f6261
1 changed files with 1 additions and 1 deletions
|
@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
Author: Leonardo de Moura
|
Author: Leonardo de Moura
|
||||||
*/
|
*/
|
||||||
#pragma once
|
#pragma once
|
||||||
|
#include "kernel/environment.h"
|
||||||
namespace lean {
|
namespace lean {
|
||||||
/** \brief Information for a user defined recursor */
|
/** \brief Information for a user defined recursor */
|
||||||
class recursor_info {
|
class recursor_info {
|
||||||
|
|
Loading…
Reference in a new issue