lean2/src/library/CMakeLists.txt

add_library(library deep_copy.cpp expr_lt.cpp io_state_stream.cpp)
# kernel_bindings.cpp
# context_to_lambda.cpp placeholder.cpp
# fo_unify.cpp bin_op.cpp equality.cpp
# hop_match.cpp)

target_link_libraries(library ${LEAN_LIBS})
refactor(kernel): finish formatter interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-02-23 07:17:52 +00:00			`add_library(library deep_copy.cpp expr_lt.cpp io_state_stream.cpp)`
refactor(library): monotonic total order on terms Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-02-23 07:09:12 +00:00			`# kernel_bindings.cpp`
refactor(kernel): finish formatter interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-02-23 07:17:52 +00:00			`# context_to_lambda.cpp placeholder.cpp`
refactor(library): remove unnecessary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-02-23 07:18:51 +00:00			`# fo_unify.cpp bin_op.cpp equality.cpp`
refactor(library): deep_copy procedure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-02-23 06:53:34 +00:00			`# hop_match.cpp)`
refactor(kernel): move printer and formatter objects to the kernel The printer and formatter objects are not trusted code. We moved them to the kernel to be able to provide them as an argument to the trace objects. Another motivation is to eliminate the kernel_exception_formatter hack. With the formatter in the kernel, we can implement the pretty printer for kernel exceptions as a virtual method. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-10-01 01:16:13 +00:00
Rename exprlib to library. Name was misleading, it is more than a library for manipulating expressions. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-08-22 17:26:52 +00:00			`target_link_libraries(library ${LEAN_LIBS})`