Move src/interval to src/util/interval

This commit is contained in:
Soonho Kong 2013-09-17 14:10:53 -07:00
parent df054477eb
commit 27d5ae13d7
9 changed files with 7 additions and 8 deletions

View file

@ -85,7 +85,7 @@ add_subdirectory(util/numerics)
set(LEAN_LIBS ${LEAN_LIBS} numerics)
add_subdirectory(util/sexpr)
set(LEAN_LIBS ${LEAN_LIBS} sexpr)
add_subdirectory(interval)
add_subdirectory(util/interval)
set(LEAN_LIBS ${LEAN_LIBS} interval)
add_subdirectory(kernel)
set(LEAN_LIBS ${LEAN_LIBS} kernel)

View file

@ -7,7 +7,7 @@ Author: Soonho Kong
#include "util/test.h"
#include "util/trace.h"
#include "util/numerics/double.h"
#include "interval/interval_def.h"
#include "util/interval/interval_def.h"
#include "tests/interval/check.h"
using namespace lean;

View file

@ -7,7 +7,7 @@ Author: Soonho Kong
#include "util/test.h"
#include "util/trace.h"
#include "util/numerics/float.h"
#include "interval/interval_def.h"
#include "util/interval/interval_def.h"
#include "tests/interval/check.h"
using namespace lean;

View file

@ -11,7 +11,7 @@ Author: Leonardo de Moura
#include "util/numerics/double.h"
#include "util/numerics/mpq.h"
#include "util/numerics/mpfp.h"
#include "interval/interval_def.h"
#include "util/interval/interval_def.h"
using namespace lean;

View file

@ -7,7 +7,7 @@ Author: Soonho Kong
#include "util/test.h"
#include "util/trace.h"
#include "util/numerics/mpfp.h"
#include "interval/interval_def.h"
#include "util/interval/interval_def.h"
#include "tests/interval/check.h"
using namespace lean;

View file

@ -1,3 +1,2 @@
add_library(interval interval.cpp)
target_link_libraries(interval ${LEAN_LIBS})

View file

@ -6,7 +6,7 @@ Author: Leonardo de Moura
*/
#include "util/numerics/mpq.h"
#include "util/numerics/double.h"
#include "interval/interval_def.h"
#include "util/interval/interval_def.h"
namespace lean {
template class interval<mpq>;

View file

@ -12,7 +12,7 @@ Author: Leonardo de Moura
#include <algorithm>
#include "util/trace.h"
#include "util/numerics/mpz.h"
#include "interval/interval.h"
#include "util/interval/interval.h"
namespace lean {